Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/rTLabs_traces.mli

    r2743 r2773  
    1111open StructuredTraces
    1212
     13open BitVectorTrie
     14
    1315open Graphs
    1416
     
    2224
    2325open SmallstepExec
    24 
    25 open BitVectorTrie
    2626
    2727open CostLabel
     
    139139type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
    140140and ('o, 'i) __flat_trace =
    141 | Ft_stop of RTLabs_semantics.state0
    142 | Ft_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     141| Ft_stop of RTLabs_semantics.state
     142| Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    143143   * ('o, 'i) flat_trace
    144144
    145145val flat_trace_inv_rect_Type4 :
    146   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    147   -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    148   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    149   -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
     146  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     147  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
     148  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
     149  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
    150150
    151151val flat_trace_inv_rect_Type3 :
    152   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    153   -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    154   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    155   -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
     152  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     153  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
     154  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
     155  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
    156156
    157157val flat_trace_inv_rect_Type2 :
    158   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    159   -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    160   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    161   -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
     158  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     159  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
     160  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
     161  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
    162162
    163163val flat_trace_inv_rect_Type1 :
    164   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    165   -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    166   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    167   -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
     164  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     165  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
     166  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
     167  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
    168168
    169169val flat_trace_inv_rect_Type0 :
    170   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    171   -> (RTLabs_semantics.state0 -> __ -> __ -> __ -> 'a3) ->
    172   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 -> __
    173   -> ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
     170  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     171  (RTLabs_semantics.state -> __ -> __ -> __ -> 'a3) ->
     172  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state -> __ ->
     173  ('a1, 'a2) flat_trace -> __ -> __ -> 'a3) -> 'a3
    174174
    175175val flat_trace_discr :
    176   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    177   -> ('a1, 'a2) flat_trace -> __
     176  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     177  ('a1, 'a2) flat_trace -> __
    178178
    179179val flat_trace_jmdiscr :
    180   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> ('a1, 'a2) flat_trace
    181   -> ('a1, 'a2) flat_trace -> __
     180  RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
     181  ('a1, 'a2) flat_trace -> __
    182182
    183183val make_flat_trace :
    184   __ -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace
     184  __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace
    185185
    186186val make_whole_flat_trace : __ -> __ -> (IO.io_out, IO.io_in) flat_trace
    187187
    188188type will_return =
    189 | Wr_step of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     189| Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    190190   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
    191 | Wr_call of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     191| Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    192192   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
    193 | Wr_ret of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     193| Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    194194   * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
    195 | Wr_base of RTLabs_semantics.state0 * Events.trace * RTLabs_semantics.state0
     195| Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
    196196   * (IO.io_out, IO.io_in) flat_trace
    197197
    198198val will_return_rect_Type4 :
    199   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    200   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    201   flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
    202   -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     199  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     200  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     201  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
     202  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    203203  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    204   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     204  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
    205205  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    206   'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    207   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    208   'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     206  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     207  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     208  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    209209  flat_trace -> will_return -> 'a1
    210210
    211211val will_return_rect_Type3 :
    212   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    213   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    214   flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
    215   -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     212  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     213  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     214  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
     215  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    216216  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    217   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     217  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
    218218  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    219   'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    220   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    221   'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     219  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     220  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     221  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    222222  flat_trace -> will_return -> 'a1
    223223
    224224val will_return_rect_Type2 :
    225   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    226   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    227   flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
    228   -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     225  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     226  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     227  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
     228  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    229229  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    230   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     230  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
    231231  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    232   'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    233   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    234   'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     232  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     233  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     234  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    235235  flat_trace -> will_return -> 'a1
    236236
    237237val will_return_rect_Type1 :
    238   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    239   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    240   flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
    241   -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     238  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     239  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     240  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
     241  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    242242  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    243   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     243  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
    244244  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    245   'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    246   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    247   'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     245  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     246  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     247  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    248248  flat_trace -> will_return -> 'a1
    249249
    250250val will_return_rect_Type0 :
    251   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    252   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    253   flat_trace -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state0
    254   -> Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     251  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     252  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     253  -> __ -> will_return -> 'a1 -> 'a1) -> (RTLabs_semantics.state ->
     254  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    255255  IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
    256   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
     256  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
    257257  Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
    258   'a1 -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    259   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    260   'a1) -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in)
     258  'a1 -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     259  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     260  'a1) -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out, IO.io_in)
    261261  flat_trace -> will_return -> 'a1
    262262
    263263val will_return_inv_rect_Type4 :
    264   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    265   IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
    266   Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     264  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     265  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
     266  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    267267  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
    268   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
    269   -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
     268  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
     269  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    270270  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    271   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    272   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
     271  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     272  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     273  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
     274  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     275  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     276  __ -> __ -> __ -> __ -> 'a1) -> 'a1
     277
     278val will_return_inv_rect_Type3 :
     279  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     280  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
     281  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
     282  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
     283  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
     284  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    273285  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    274   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    275   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     286  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     287  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     288  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
     289  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     290  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    276291  __ -> __ -> __ -> __ -> 'a1) -> 'a1
    277292
    278 val will_return_inv_rect_Type3 :
    279   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    280   IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
    281   Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     293val will_return_inv_rect_Type2 :
     294  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     295  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
     296  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    282297  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
    283   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
    284   -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
     298  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
     299  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    285300  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    286   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    287   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
     301  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     302  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     303  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
     304  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     305  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     306  __ -> __ -> __ -> __ -> 'a1) -> 'a1
     307
     308val will_return_inv_rect_Type1 :
     309  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     310  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
     311  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
     312  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
     313  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
     314  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    288315  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    289   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    290   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     316  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     317  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     318  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
     319  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     320  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    291321  __ -> __ -> __ -> __ -> 'a1) -> 'a1
    292322
    293 val will_return_inv_rect_Type2 :
    294   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    295   IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
    296   Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
     323val will_return_inv_rect_Type0 :
     324  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     325  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state ->
     326  Events.trace -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out,
    297327  IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
    298   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
    299   -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
     328  -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
     329  -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    300330  flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    301   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    302   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    303   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    304   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    305   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
     331  __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     332  RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace
     333  -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ -> __ -> __ ->
     334  __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace ->
     335  RTLabs_semantics.state -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    306336  __ -> __ -> __ -> __ -> 'a1) -> 'a1
    307337
    308 val will_return_inv_rect_Type1 :
    309   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    310   IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
    311   Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
    312   IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
    313   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
    314   -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    315   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    316   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    317   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    318   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    319   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    320   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    321   __ -> __ -> __ -> __ -> 'a1) -> 'a1
    322 
    323 val will_return_inv_rect_Type0 :
    324   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    325   IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0 ->
    326   Events.trace -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out,
    327   IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
    328   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace
    329   -> RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    330   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    331   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    332   RTLabs_semantics.state0 -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
    333   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
    334   __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state0 -> Events.trace ->
    335   RTLabs_semantics.state0 -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ ->
    336   __ -> __ -> __ -> __ -> 'a1) -> 'a1
    337 
    338338val will_return_jmdiscr :
    339   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
     339  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
    340340  IO.io_in) flat_trace -> will_return -> will_return -> __
    341341
    342342val will_return_length :
    343   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
     343  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
    344344  IO.io_in) flat_trace -> will_return -> Nat.nat
    345345
    346346val will_return_end :
    347   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    348   IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state0,
    349   (IO.io_out, IO.io_in) flat_trace) Types.dPair
     347  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     348  IO.io_in) flat_trace -> will_return -> (RTLabs_semantics.state, (IO.io_out,
     349  IO.io_in) flat_trace) Types.dPair
    350350
    351351val will_return_call :
    352   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> Events.trace
    353   -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
     352  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
     353  -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
    354354  will_return -> will_return Types.sig0
    355355
    356356val will_return_return :
    357   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> Events.trace
    358   -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace ->
     357  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
     358  -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
    359359  will_return -> __
    360360
    361361val will_return_notfn :
    362   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> Events.trace
    363   -> RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace -> (__, __)
     362  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
     363  -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> (__, __)
    364364  Types.sum -> will_return -> will_return Types.sig0
    365365
    366366val will_return_prepend :
    367   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
    368   IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state0
    369   -> (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return
     367  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
     368  IO.io_in) flat_trace -> will_return -> Nat.nat -> RTLabs_semantics.state ->
     369  (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return
    370370
    371371val nat_jmdiscr : Nat.nat -> Nat.nat -> __
    372372
    373373val will_return_remove_call :
    374   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
     374  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
    375375  IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
    376   RTLabs_semantics.state0 -> (IO.io_out, IO.io_in) flat_trace -> will_return
     376  RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return
    377377
    378378val will_return_lower :
    379   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state0 -> (IO.io_out,
     379  RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
    380380  IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return
    381381
     
    612612  StructuredTraces.trace_label_return trace_result
    613613
    614 val actual_successor : RTLabs_semantics.state0 -> Graphs.label Types.option
     614val actual_successor : RTLabs_semantics.state -> Graphs.label Types.option
    615615
    616616val steps_for_statement : RTLabs_syntax.statement -> Nat.nat
     
    683683
    684684val init_state_is :
    685   RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 -> (Pointers.block,
     685  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> (Pointers.block,
    686686  __) Types.dPair
    687687
    688688val ras_state_initial :
    689   RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state0 ->
     689  RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
    690690  RTLabs_abstract.rTLabs_ext_state
    691691
    692692val deprop_execute :
    693   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
     693  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
    694694  -> Events.trace Types.sig0
    695695
     
    699699
    700700type ('o, 'i) partial_flat_trace =
    701 | Pft_base of RTLabs_semantics.state0 * Events.trace
    702    * RTLabs_semantics.state0
    703 | Pft_step of RTLabs_semantics.state0 * Events.trace
    704    * RTLabs_semantics.state0 * RTLabs_semantics.state0
    705    * ('o, 'i) partial_flat_trace
     701| Pft_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
     702| Pft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
     703   * RTLabs_semantics.state * ('o, 'i) partial_flat_trace
    706704
    707705val partial_flat_trace_rect_Type4 :
    708   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    709   RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    710   Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
    711   ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
    712   RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
     706  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     707  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     708  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     709  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     710  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
    713711
    714712val partial_flat_trace_rect_Type3 :
    715   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    716   RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    717   Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
    718   ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
    719   RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
     713  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     714  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     715  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     716  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     717  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
    720718
    721719val partial_flat_trace_rect_Type2 :
    722   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    723   RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    724   Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
    725   ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
    726   RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
     720  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     721  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     722  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     723  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     724  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
    727725
    728726val partial_flat_trace_rect_Type1 :
    729   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    730   RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    731   Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
    732   ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
    733   RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
     727  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     728  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     729  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     730  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     731  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
    734732
    735733val partial_flat_trace_rect_Type0 :
    736   RTLabs_semantics.genv -> (RTLabs_semantics.state0 -> Events.trace ->
    737   RTLabs_semantics.state0 -> __ -> 'a3) -> (RTLabs_semantics.state0 ->
    738   Events.trace -> RTLabs_semantics.state0 -> RTLabs_semantics.state0 -> __ ->
    739   ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state0 ->
    740   RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> 'a3
     734  RTLabs_semantics.genv -> (RTLabs_semantics.state -> Events.trace ->
     735  RTLabs_semantics.state -> __ -> 'a3) -> (RTLabs_semantics.state ->
     736  Events.trace -> RTLabs_semantics.state -> RTLabs_semantics.state -> __ ->
     737  ('a1, 'a2) partial_flat_trace -> 'a3 -> 'a3) -> RTLabs_semantics.state ->
     738  RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> 'a3
    741739
    742740val partial_flat_trace_inv_rect_Type4 :
    743   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
    744   -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
    745   Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
    746   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    747   RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
     741  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     742  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
     743  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     744  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     745  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
    748746  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
    749747
    750748val partial_flat_trace_inv_rect_Type3 :
    751   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
    752   -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
    753   Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
    754   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    755   RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
     749  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     750  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
     751  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     752  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     753  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
    756754  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
    757755
    758756val partial_flat_trace_inv_rect_Type2 :
    759   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
    760   -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
    761   Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
    762   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    763   RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
     757  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     758  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
     759  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     760  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     761  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
    764762  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
    765763
    766764val partial_flat_trace_inv_rect_Type1 :
    767   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
    768   -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
    769   Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
    770   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    771   RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
     765  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     766  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
     767  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     768  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     769  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
    772770  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
    773771
    774772val partial_flat_trace_inv_rect_Type0 :
    775   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
    776   -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state0 ->
    777   Events.trace -> RTLabs_semantics.state0 -> __ -> __ -> __ -> __ -> 'a3) ->
    778   (RTLabs_semantics.state0 -> Events.trace -> RTLabs_semantics.state0 ->
    779   RTLabs_semantics.state0 -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
     773  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     774  -> ('a1, 'a2) partial_flat_trace -> (RTLabs_semantics.state -> Events.trace
     775  -> RTLabs_semantics.state -> __ -> __ -> __ -> __ -> 'a3) ->
     776  (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
     777  RTLabs_semantics.state -> __ -> ('a1, 'a2) partial_flat_trace -> (__ -> __
    780778  -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
    781779
    782780val partial_flat_trace_jmdiscr :
    783   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
     781  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
    784782  -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __
    785783
    786784val append_partial_flat_trace :
    787   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
    788   -> RTLabs_semantics.state0 -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
     785  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
     786  -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
    789787  partial_flat_trace -> ('a1, 'a2) partial_flat_trace
    790788
    791789val partial_to_flat_trace :
    792   RTLabs_semantics.genv -> RTLabs_semantics.state0 -> RTLabs_semantics.state0
     790  RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
    793791  -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
    794792  flat_trace
     
    824822
    825823val add_partial_flat_trace :
    826   RTLabs_semantics.genv -> RTLabs_semantics.state0 ->
     824  RTLabs_semantics.genv -> RTLabs_semantics.state ->
    827825  RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
    828826  partial_flat_trace -> StructuredTraces.trace_label_diverges -> (IO.io_out,
Note: See TracChangeset for help on using the changeset viewer.