Changeset 2730 for extracted/csem.mli


Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/csem.mli

    r2717 r2730  
    317317type state0 =
    318318| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
    319 | Callstate of Values.val0 * Csyntax.clight_fundef * Values.val0 List.list
     319| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
    320320   * cont * GenMem.mem1
    321321| Returnstate of Values.val0 * cont * GenMem.mem1
     
    324324val state_rect_Type4 :
    325325  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    326   'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     326  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    327327  cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    328328  -> (Integers.int -> 'a1) -> state0 -> 'a1
     
    330330val state_rect_Type5 :
    331331  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    332   'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     332  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    333333  cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    334334  -> (Integers.int -> 'a1) -> state0 -> 'a1
     
    336336val state_rect_Type3 :
    337337  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    338   'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     338  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    339339  cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    340340  -> (Integers.int -> 'a1) -> state0 -> 'a1
     
    342342val state_rect_Type2 :
    343343  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    344   'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     344  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    345345  cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    346346  -> (Integers.int -> 'a1) -> state0 -> 'a1
     
    348348val state_rect_Type1 :
    349349  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    350   'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     350  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    351351  cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    352352  -> (Integers.int -> 'a1) -> state0 -> 'a1
     
    354354val state_rect_Type0 :
    355355  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
    356   'a1) -> (Values.val0 -> Csyntax.clight_fundef -> Values.val0 List.list ->
     356  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
    357357  cont -> GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1)
    358358  -> (Integers.int -> 'a1) -> state0 -> 'a1
     
    360360val state_inv_rect_Type4 :
    361361  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    362   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     362  GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    363363  Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    364364  -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     
    366366val state_inv_rect_Type3 :
    367367  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    368   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     368  GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    369369  Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    370370  -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     
    372372val state_inv_rect_Type2 :
    373373  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    374   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     374  GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    375375  Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    376376  -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     
    378378val state_inv_rect_Type1 :
    379379  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    380   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     380  GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    381381  Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    382382  -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
     
    384384val state_inv_rect_Type0 :
    385385  state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
    386   GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> Csyntax.clight_fundef ->
     386  GenMem.mem1 -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
    387387  Values.val0 List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0
    388388  -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
Note: See TracChangeset for help on using the changeset viewer.