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/rTLabs_semantics.mli

    r2649 r2730  
    7373open Identifiers
    7474
     75open Exp
     76
    7577open Arithmetic
    7678
     
    9395open Globalenvs
    9496
     97open BitVectorTrie
     98
    9599open CostLabel
    96100
     
    102106
    103107open SmallstepExec
    104 
    105 open BitVectorTrie
    106108
    107109open Graphs
     
    193195type state0 =
    194196| State of frame * frame List.list * GenMem.mem1
    195 | Callstate of RTLabs_syntax.internal_function AST.fundef
     197| Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
    196198   * Values.val0 List.list * Registers.register Types.option
    197199   * frame List.list * GenMem.mem1
     
    201203
    202204val state_rect_Type4 :
    203   (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
    204   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     205  (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
     206  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    205207  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    206208  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
     
    208210
    209211val state_rect_Type5 :
    210   (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
    211   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     212  (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
     213  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    212214  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    213215  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
     
    215217
    216218val state_rect_Type3 :
    217   (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
    218   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     219  (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
     220  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    219221  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    220222  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
     
    222224
    223225val state_rect_Type2 :
    224   (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
    225   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     226  (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
     227  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    226228  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    227229  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
     
    229231
    230232val state_rect_Type1 :
    231   (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
    232   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     233  (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
     234  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    233235  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    234236  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
     
    236238
    237239val state_rect_Type0 :
    238   (frame -> frame List.list -> GenMem.mem1 -> 'a1) ->
    239   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     240  (frame -> frame List.list -> GenMem.mem1 -> 'a1) -> (AST.ident ->
     241  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    240242  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> 'a1)
    241243  -> (Values.val0 Types.option -> Registers.register Types.option -> frame
     
    244246val state_inv_rect_Type4 :
    245247  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    246   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    247   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    248   'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
    249   frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
    250   -> 'a1
     248  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     249  List.list -> Registers.register Types.option -> frame List.list ->
     250  GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
     251  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
     252  'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    251253
    252254val state_inv_rect_Type3 :
    253255  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    254   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    255   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    256   'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
    257   frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
    258   -> 'a1
     256  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     257  List.list -> Registers.register Types.option -> frame List.list ->
     258  GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
     259  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
     260  'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    259261
    260262val state_inv_rect_Type2 :
    261263  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    262   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    263   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    264   'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
    265   frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
    266   -> 'a1
     264  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     265  List.list -> Registers.register Types.option -> frame List.list ->
     266  GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
     267  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
     268  'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    267269
    268270val state_inv_rect_Type1 :
    269271  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    270   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    271   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    272   'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
    273   frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
    274   -> 'a1
     272  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     273  List.list -> Registers.register Types.option -> frame List.list ->
     274  GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
     275  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
     276  'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    275277
    276278val state_inv_rect_Type0 :
    277279  state0 -> (frame -> frame List.list -> GenMem.mem1 -> __ -> 'a1) ->
    278   (RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
    279   Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
    280   'a1) -> (Values.val0 Types.option -> Registers.register Types.option ->
    281   frame List.list -> GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1)
    282   -> 'a1
    283 
    284 val state_discr : state0 -> state0 -> __
     280  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
     281  List.list -> Registers.register Types.option -> frame List.list ->
     282  GenMem.mem1 -> __ -> 'a1) -> (Values.val0 Types.option ->
     283  Registers.register Types.option -> frame List.list -> GenMem.mem1 -> __ ->
     284  'a1) -> (Integers.int -> __ -> 'a1) -> 'a1
    285285
    286286val state_jmdiscr : state0 -> state0 -> __
     
    327327  'a3) -> 'a3
    328328
     329val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2
     330
    329331val func_block_of_exec :
    330   genv -> state0 -> Events.trace -> RTLabs_syntax.internal_function
    331   AST.fundef -> Values.val0 List.list -> Registers.register Types.option ->
    332   frame List.list -> GenMem.mem1 -> Pointers.block Types.sig0
    333 
     332  genv -> state0 -> Events.trace -> AST.ident ->
     333  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
     334  Registers.register Types.option -> frame List.list -> GenMem.mem1 ->
     335  Pointers.block Types.sig0
     336
Note: See TracChangeset for help on using the changeset viewer.