extracted/rTLabs_traces.mli

   1 open Preamble
   2
   3 open Deqsets_extra
   4
   5 open CostSpec
   6
   7 open Sets
   8
   9 open Listb
  10
  11 open StructuredTraces
  12
  13 open BitVectorTrie
  14
  15 open Graphs
  16
  17 open Order
  18
  19 open Registers
  20
  21 open FrontEndOps
  22
  23 open RTLabs_syntax
  24
  25 open SmallstepExec
  26
  27 open CostLabel
  28
  29 open Events
  30
  31 open IOMonad
  32
  33 open IO
  34
  35 open Extra_bool
  36
  37 open Coqlib
  38
  39 open Values
  40
  41 open FrontEndVal
  42
  43 open Hide
  44
  45 open ByteValues
  46
  47 open Division
  48
  49 open Z
  50
  51 open BitVectorZ
  52
  53 open Pointers
  54
  55 open GenMem
  56
  57 open FrontEndMem
  58
  59 open Proper
  60
  61 open PositiveMap
  62
  63 open Deqsets
  64
  65 open Extralib
  66
  67 open Lists
  68
  69 open Identifiers
  70
  71 open Exp
  72
  73 open Arithmetic
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Util
  80
  81 open FoldStuff
  82
  83 open BitVector
  84
  85 open Extranat
  86
  87 open Integers
  88
  89 open AST
  90
  91 open Globalenvs
  92
  93 open ErrorMessages
  94
  95 open Option
  96
  97 open Setoids
  98
  99 open Monad
 100
 101 open Jmeq
 102
 103 open Russell
 104
 105 open Positive
 106
 107 open PreIdentifiers
 108
 109 open Errors
 110
 111 open Bool
 112
 113 open Relations
 114
 115 open Nat
 116
 117 open Hints_declaration
 118
 119 open Core_notation
 120
 121 open Pts
 122
 123 open Logic
 124
 125 open Types
 126
 127 open List
 128
 129 open RTLabs_semantics
 130
 131 open RTLabs_abstract
 132
 133 open CostMisc
 134
 135 open Executions
 136
 137 open Listb_extra
 138
 139 type ('o, 'i) flat_trace = ('o, 'i) __flat_trace Lazy.t
 140 and ('o, 'i) __flat_trace =
 141 | Ft_stop of RTLabs_semantics.state
 142 | Ft_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 143    * ('o, 'i) flat_trace
 144
 145 val flat_trace_inv_rect_Type4 :
 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
 150
 151 val flat_trace_inv_rect_Type3 :
 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
 156
 157 val flat_trace_inv_rect_Type2 :
 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
 162
 163 val flat_trace_inv_rect_Type1 :
 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
 168
 169 val flat_trace_inv_rect_Type0 :
 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
 174
 175 val flat_trace_discr :
 176   RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
 177   ('a1, 'a2) flat_trace -> __
 178
 179 val flat_trace_jmdiscr :
 180   RTLabs_semantics.genv -> RTLabs_semantics.state -> ('a1, 'a2) flat_trace ->
 181   ('a1, 'a2) flat_trace -> __
 182
 183 val make_flat_trace :
 184   __ -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace
 185
 186 val make_whole_flat_trace : __ -> __ -> (IO.io_out, IO.io_in) flat_trace
 187
 188 type will_return =
 189 | Wr_step of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 190    * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
 191 | Wr_call of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 192    * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
 193 | Wr_ret of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 194    * Nat.nat * (IO.io_out, IO.io_in) flat_trace * will_return
 195 | Wr_base of RTLabs_semantics.state * Events.trace * RTLabs_semantics.state
 196    * (IO.io_out, IO.io_in) flat_trace
 197
 198 val will_return_rect_Type4 :
 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,
 203   IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 204   (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 205   Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 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)
 209   flat_trace -> will_return -> 'a1
 210
 211 val will_return_rect_Type3 :
 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,
 216   IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 217   (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 218   Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 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)
 222   flat_trace -> will_return -> 'a1
 223
 224 val will_return_rect_Type2 :
 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,
 229   IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 230   (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 231   Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 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)
 235   flat_trace -> will_return -> 'a1
 236
 237 val will_return_rect_Type1 :
 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,
 242   IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 243   (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 244   Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 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)
 248   flat_trace -> will_return -> 'a1
 249
 250 val will_return_rect_Type0 :
 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,
 255   IO.io_in) flat_trace -> __ -> will_return -> 'a1 -> 'a1) ->
 256   (RTLabs_semantics.state -> Events.trace -> RTLabs_semantics.state ->
 257   Nat.nat -> __ -> (IO.io_out, IO.io_in) flat_trace -> __ -> will_return ->
 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)
 261   flat_trace -> will_return -> 'a1
 262
 263 val will_return_inv_rect_Type4 :
 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,
 267   IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
 268   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
 269   -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 270   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
 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
 278 val 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)
 285   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
 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 -> __ ->
 291   __ -> __ -> __ -> __ -> 'a1) -> 'a1
 292
 293 val 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,
 297   IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
 298   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
 299   -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 300   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
 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
 308 val 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)
 315   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
 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 -> __ ->
 321   __ -> __ -> __ -> __ -> 'a1) -> 'a1
 322
 323 val 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,
 327   IO.io_in) flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1)
 328   -> __ -> __ -> __ -> __ -> 'a1) -> (RTLabs_semantics.state -> Events.trace
 329   -> RTLabs_semantics.state -> Nat.nat -> __ -> (IO.io_out, IO.io_in)
 330   flat_trace -> __ -> will_return -> (__ -> __ -> __ -> __ -> 'a1) -> __ ->
 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 -> __ ->
 336   __ -> __ -> __ -> __ -> 'a1) -> 'a1
 337
 338 val will_return_jmdiscr :
 339   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 340   IO.io_in) flat_trace -> will_return -> will_return -> __
 341
 342 val will_return_length :
 343   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 344   IO.io_in) flat_trace -> will_return -> Nat.nat
 345
 346 val will_return_end :
 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
 350
 351 val will_return_call :
 352   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
 353   -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
 354   will_return -> will_return Types.sig0
 355
 356 val will_return_return :
 357   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
 358   -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace ->
 359   will_return -> __
 360
 361 val will_return_notfn :
 362   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> Events.trace
 363   -> RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> (__, __)
 364   Types.sum -> will_return -> will_return Types.sig0
 365
 366 val will_return_prepend :
 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
 370
 371 val nat_jmdiscr : Nat.nat -> Nat.nat -> __
 372
 373 val will_return_remove_call :
 374   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 375   IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return ->
 376   RTLabs_semantics.state -> (IO.io_out, IO.io_in) flat_trace -> will_return
 377
 378 val will_return_lower :
 379   RTLabs_semantics.genv -> Nat.nat -> RTLabs_semantics.state -> (IO.io_out,
 380   IO.io_in) flat_trace -> will_return -> Nat.nat -> will_return
 381
 382 val list_jmdiscr : 'a1 List.list -> 'a1 List.list -> __
 383
 384 type 't trace_result = { new_state : RTLabs_abstract.rTLabs_ext_state;
 385                          remainder : (IO.io_out, IO.io_in) flat_trace;
 386                          new_trace : 't; terminates : __ }
 387
 388 val trace_result_rect_Type4 :
 389   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 390   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 391   will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 392   IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
 393   -> 'a2
 394
 395 val trace_result_rect_Type5 :
 396   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 397   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 398   will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 399   IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
 400   -> 'a2
 401
 402 val trace_result_rect_Type3 :
 403   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 404   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 405   will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 406   IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
 407   -> 'a2
 408
 409 val trace_result_rect_Type2 :
 410   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 411   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 412   will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 413   IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
 414   -> 'a2
 415
 416 val trace_result_rect_Type1 :
 417   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 418   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 419   will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 420   IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
 421   -> 'a2
 422
 423 val trace_result_rect_Type0 :
 424   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 425   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 426   will_return -> Nat.nat -> (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 427   IO.io_in) flat_trace -> __ -> 'a1 -> __ -> __ -> 'a2) -> 'a1 trace_result
 428   -> 'a2
 429
 430 val new_state :
 431   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 432   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 433   will_return -> Nat.nat -> 'a1 trace_result ->
 434   RTLabs_abstract.rTLabs_ext_state
 435
 436 val remainder :
 437   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 438   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 439   will_return -> Nat.nat -> 'a1 trace_result -> (IO.io_out, IO.io_in)
 440   flat_trace
 441
 442 val new_trace :
 443   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 444   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 445   will_return -> Nat.nat -> 'a1 trace_result -> 'a1
 446
 447 val terminates :
 448   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 449   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 450   will_return -> Nat.nat -> 'a1 trace_result -> __
 451
 452 val trace_result_inv_rect_Type4 :
 453   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 454   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 455   will_return -> Nat.nat -> 'a1 trace_result ->
 456   (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
 457   -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
 458
 459 val trace_result_inv_rect_Type3 :
 460   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 461   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 462   will_return -> Nat.nat -> 'a1 trace_result ->
 463   (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
 464   -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
 465
 466 val trace_result_inv_rect_Type2 :
 467   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 468   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 469   will_return -> Nat.nat -> 'a1 trace_result ->
 470   (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
 471   -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
 472
 473 val trace_result_inv_rect_Type1 :
 474   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 475   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 476   will_return -> Nat.nat -> 'a1 trace_result ->
 477   (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
 478   -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
 479
 480 val trace_result_inv_rect_Type0 :
 481   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 482   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 483   will_return -> Nat.nat -> 'a1 trace_result ->
 484   (RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace -> __
 485   -> 'a1 -> __ -> __ -> __ -> 'a2) -> 'a2
 486
 487 val trace_result_jmdiscr :
 488   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 489   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 490   will_return -> Nat.nat -> 'a1 trace_result -> 'a1 trace_result -> __
 491
 492 type 't sub_trace_result = { ends : StructuredTraces.trace_ends_with_ret;
 493                              trace_res : 't trace_result }
 494
 495 val sub_trace_result_rect_Type4 :
 496   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 497   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 498   (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
 499   sub_trace_result -> 'a2
 500
 501 val sub_trace_result_rect_Type5 :
 502   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 503   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 504   (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
 505   sub_trace_result -> 'a2
 506
 507 val sub_trace_result_rect_Type3 :
 508   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 509   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 510   (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
 511   sub_trace_result -> 'a2
 512
 513 val sub_trace_result_rect_Type2 :
 514   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 515   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 516   (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
 517   sub_trace_result -> 'a2
 518
 519 val sub_trace_result_rect_Type1 :
 520   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 521   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 522   (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
 523   sub_trace_result -> 'a2
 524
 525 val sub_trace_result_rect_Type0 :
 526   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 527   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 528   (StructuredTraces.trace_ends_with_ret -> 'a1 trace_result -> 'a2) -> 'a1
 529   sub_trace_result -> 'a2
 530
 531 val ends :
 532   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 533   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 534   sub_trace_result -> StructuredTraces.trace_ends_with_ret
 535
 536 val trace_res :
 537   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 538   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 539   sub_trace_result -> 'a1 trace_result
 540
 541 val sub_trace_result_inv_rect_Type4 :
 542   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 543   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 544   sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
 545   trace_result -> __ -> 'a2) -> 'a2
 546
 547 val sub_trace_result_inv_rect_Type3 :
 548   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 549   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 550   sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
 551   trace_result -> __ -> 'a2) -> 'a2
 552
 553 val sub_trace_result_inv_rect_Type2 :
 554   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 555   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 556   sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
 557   trace_result -> __ -> 'a2) -> 'a2
 558
 559 val sub_trace_result_inv_rect_Type1 :
 560   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 561   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 562   sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
 563   trace_result -> __ -> 'a2) -> 'a2
 564
 565 val sub_trace_result_inv_rect_Type0 :
 566   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 567   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 568   sub_trace_result -> (StructuredTraces.trace_ends_with_ret -> 'a1
 569   trace_result -> __ -> 'a2) -> 'a2
 570
 571 val sub_trace_result_discr :
 572   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 573   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 574   sub_trace_result -> 'a1 sub_trace_result -> __
 575
 576 val sub_trace_result_jmdiscr :
 577   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 578   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat -> 'a1
 579   sub_trace_result -> 'a1 sub_trace_result -> __
 580
 581 val replace_trace :
 582   RTLabs_semantics.genv -> Nat.nat -> StructuredTraces.trace_ends_with_ret ->
 583   RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
 584   (IO.io_out, IO.io_in) flat_trace -> (IO.io_out, IO.io_in) flat_trace ->
 585   will_return -> will_return -> Nat.nat -> Nat.nat -> 'a1 trace_result -> 'a2
 586   -> 'a2 trace_result
 587
 588 val replace_sub_trace :
 589   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 590   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in) flat_trace ->
 591   (IO.io_out, IO.io_in) flat_trace -> will_return -> will_return -> Nat.nat
 592   -> Nat.nat -> 'a1 sub_trace_result -> 'a2 -> 'a2 sub_trace_result
 593
 594 val make_any_label :
 595   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 596   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 597   StructuredTraces.trace_any_label sub_trace_result
 598
 599 val make_label_label :
 600   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 601   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 602   StructuredTraces.trace_label_label sub_trace_result
 603
 604 val make_label_return :
 605   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 606   (IO.io_out, IO.io_in) flat_trace -> will_return -> Nat.nat ->
 607   StructuredTraces.trace_label_return trace_result
 608
 609 val make_label_return' :
 610   RTLabs_semantics.genv -> Nat.nat -> RTLabs_abstract.rTLabs_ext_state ->
 611   (IO.io_out, IO.io_in) flat_trace -> will_return ->
 612   StructuredTraces.trace_label_return trace_result
 613
 614 val actual_successor : RTLabs_semantics.state -> Graphs.label Types.option
 615
 616 val steps_for_statement : RTLabs_syntax.statement -> Nat.nat
 617
 618 type remainder_ok =
 619 | Mk_remainder_ok
 620
 621 val remainder_ok_rect_Type4 :
 622   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 623   IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
 624   'a1
 625
 626 val remainder_ok_rect_Type5 :
 627   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 628   IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
 629   'a1
 630
 631 val remainder_ok_rect_Type3 :
 632   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 633   IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
 634   'a1
 635
 636 val remainder_ok_rect_Type2 :
 637   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 638   IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
 639   'a1
 640
 641 val remainder_ok_rect_Type1 :
 642   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 643   IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
 644   'a1
 645
 646 val remainder_ok_rect_Type0 :
 647   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 648   IO.io_in) flat_trace -> (__ -> __ -> __ -> __ -> 'a1) -> remainder_ok ->
 649   'a1
 650
 651 val remainder_ok_inv_rect_Type4 :
 652   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 653   IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
 654   -> 'a1
 655
 656 val remainder_ok_inv_rect_Type3 :
 657   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 658   IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
 659   -> 'a1
 660
 661 val remainder_ok_inv_rect_Type2 :
 662   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 663   IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
 664   -> 'a1
 665
 666 val remainder_ok_inv_rect_Type1 :
 667   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 668   IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
 669   -> 'a1
 670
 671 val remainder_ok_inv_rect_Type0 :
 672   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 673   IO.io_in) flat_trace -> remainder_ok -> (__ -> __ -> __ -> __ -> __ -> 'a1)
 674   -> 'a1
 675
 676 val remainder_ok_discr :
 677   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 678   IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __
 679
 680 val remainder_ok_jmdiscr :
 681   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state -> (IO.io_out,
 682   IO.io_in) flat_trace -> remainder_ok -> remainder_ok -> __
 683
 684 val init_state_is :
 685   RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state -> (Pointers.block,
 686   __) Types.dPair
 687
 688 val ras_state_initial :
 689   RTLabs_syntax.rTLabs_program -> RTLabs_semantics.state ->
 690   RTLabs_abstract.rTLabs_ext_state
 691
 692 val deprop_execute :
 693   RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
 694   -> Events.trace Types.sig0
 695
 696 val deprop_as_execute :
 697   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
 698   RTLabs_abstract.rTLabs_ext_state -> Events.trace Types.sig0
 699
 700 type ('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
 704
 705 val partial_flat_trace_rect_Type4 :
 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
 711
 712 val partial_flat_trace_rect_Type3 :
 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
 718
 719 val partial_flat_trace_rect_Type2 :
 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
 725
 726 val partial_flat_trace_rect_Type1 :
 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
 732
 733 val partial_flat_trace_rect_Type0 :
 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
 739
 740 val partial_flat_trace_inv_rect_Type4 :
 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 -> (__ -> __
 746   -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
 747
 748 val partial_flat_trace_inv_rect_Type3 :
 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 -> (__ -> __
 754   -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
 755
 756 val partial_flat_trace_inv_rect_Type2 :
 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 -> (__ -> __
 762   -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
 763
 764 val partial_flat_trace_inv_rect_Type1 :
 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 -> (__ -> __
 770   -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
 771
 772 val partial_flat_trace_inv_rect_Type0 :
 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 -> (__ -> __
 778   -> __ -> 'a3) -> __ -> __ -> __ -> 'a3) -> 'a3
 779
 780 val partial_flat_trace_jmdiscr :
 781   RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
 782   -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) partial_flat_trace -> __
 783
 784 val append_partial_flat_trace :
 785   RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
 786   -> RTLabs_semantics.state -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2)
 787   partial_flat_trace -> ('a1, 'a2) partial_flat_trace
 788
 789 val partial_to_flat_trace :
 790   RTLabs_semantics.genv -> RTLabs_semantics.state -> RTLabs_semantics.state
 791   -> ('a1, 'a2) partial_flat_trace -> ('a1, 'a2) flat_trace -> ('a1, 'a2)
 792   flat_trace
 793
 794 val flat_trace_of_any_label :
 795   RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
 796   RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
 797   StructuredTraces.trace_any_label -> (IO.io_out, IO.io_in)
 798   partial_flat_trace
 799
 800 val flat_trace_of_label_label :
 801   RTLabs_semantics.genv -> StructuredTraces.trace_ends_with_ret ->
 802   RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
 803   StructuredTraces.trace_label_label -> (IO.io_out, IO.io_in)
 804   partial_flat_trace
 805
 806 val flat_trace_of_label_return :
 807   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
 808   RTLabs_abstract.rTLabs_ext_state -> StructuredTraces.trace_label_return ->
 809   (IO.io_out, IO.io_in) partial_flat_trace
 810
 811 val flat_trace_of_any_call :
 812   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
 813   RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
 814   Events.trace -> StructuredTraces.trace_any_call -> (IO.io_out, IO.io_in)
 815   partial_flat_trace
 816
 817 val flat_trace_of_label_call :
 818   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
 819   RTLabs_abstract.rTLabs_ext_state -> RTLabs_abstract.rTLabs_ext_state ->
 820   Events.trace -> StructuredTraces.trace_label_call -> (IO.io_out, IO.io_in)
 821   partial_flat_trace
 822
 823 val add_partial_flat_trace :
 824   RTLabs_semantics.genv -> RTLabs_semantics.state ->
 825   RTLabs_abstract.rTLabs_ext_state -> (IO.io_out, IO.io_in)
 826   partial_flat_trace -> StructuredTraces.trace_label_diverges -> (IO.io_out,
 827   IO.io_in) flat_trace
 828
 829 val flat_trace_of_label_diverges :
 830   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
 831   StructuredTraces.trace_label_diverges -> (IO.io_out, IO.io_in) flat_trace
 832
 833 val flat_trace_of_whole_program :
 834   RTLabs_semantics.genv -> RTLabs_abstract.rTLabs_ext_state ->
 835   StructuredTraces.trace_whole_program -> (IO.io_out, IO.io_in) flat_trace
 836
 837 val state_fn : RTLabs_semantics.genv -> __ -> Pointers.block Types.option
 838
 839 val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __
 840