extracted/cminor_semantics.ml

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open Extralib
  12
  13 open Lists
  14
  15 open Identifiers
  16
  17 open Integers
  18
  19 open AST
  20
  21 open Division
  22
  23 open Exp
  24
  25 open Arithmetic
  26
  27 open Extranat
  28
  29 open Vector
  30
  31 open FoldStuff
  32
  33 open BitVector
  34
  35 open Z
  36
  37 open BitVectorZ
  38
  39 open Pointers
  40
  41 open ErrorMessages
  42
  43 open Option
  44
  45 open Setoids
  46
  47 open Monad
  48
  49 open Positive
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Div_and_mod
  56
  57 open Jmeq
  58
  59 open Russell
  60
  61 open Util
  62
  63 open Bool
  64
  65 open Relations
  66
  67 open Nat
  68
  69 open List
  70
  71 open Hints_declaration
  72
  73 open Core_notation
  74
  75 open Pts
  76
  77 open Logic
  78
  79 open Types
  80
  81 open Coqlib
  82
  83 open Values
  84
  85 open Events
  86
  87 open FrontEndVal
  88
  89 open Hide
  90
  91 open ByteValues
  92
  93 open GenMem
  94
  95 open FrontEndMem
  96
  97 open IOMonad
  98
  99 open IO
 100
 101 open Extra_bool
 102
 103 open Globalenvs
 104
 105 open SmallstepExec
 106
 107 open FrontEndOps
 108
 109 open Cminor_syntax
 110
 111 type env = Values.val0 Identifiers.identifier_map
 112
 113 type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t
 114
 115 type cont =
 116 | Kend
 117 | Kseq of Cminor_syntax.stmt * cont
 118 | Kblock of cont
 119
 120 (** val cont_rect_Type4 :
 121     'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 122     -> cont -> 'a1 **)
 123 let rec cont_rect_Type4 h_Kend h_Kseq h_Kblock = function
 124 | Kend -> h_Kend
 125 | Kseq (x_23729, x_23728) ->
 126   h_Kseq x_23729 x_23728 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23728)
 127 | Kblock x_23730 ->
 128   h_Kblock x_23730 (cont_rect_Type4 h_Kend h_Kseq h_Kblock x_23730)
 129
 130 (** val cont_rect_Type3 :
 131     'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 132     -> cont -> 'a1 **)
 133 let rec cont_rect_Type3 h_Kend h_Kseq h_Kblock = function
 134 | Kend -> h_Kend
 135 | Kseq (x_23743, x_23742) ->
 136   h_Kseq x_23743 x_23742 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23742)
 137 | Kblock x_23744 ->
 138   h_Kblock x_23744 (cont_rect_Type3 h_Kend h_Kseq h_Kblock x_23744)
 139
 140 (** val cont_rect_Type2 :
 141     'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 142     -> cont -> 'a1 **)
 143 let rec cont_rect_Type2 h_Kend h_Kseq h_Kblock = function
 144 | Kend -> h_Kend
 145 | Kseq (x_23750, x_23749) ->
 146   h_Kseq x_23750 x_23749 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23749)
 147 | Kblock x_23751 ->
 148   h_Kblock x_23751 (cont_rect_Type2 h_Kend h_Kseq h_Kblock x_23751)
 149
 150 (** val cont_rect_Type1 :
 151     'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 152     -> cont -> 'a1 **)
 153 let rec cont_rect_Type1 h_Kend h_Kseq h_Kblock = function
 154 | Kend -> h_Kend
 155 | Kseq (x_23757, x_23756) ->
 156   h_Kseq x_23757 x_23756 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23756)
 157 | Kblock x_23758 ->
 158   h_Kblock x_23758 (cont_rect_Type1 h_Kend h_Kseq h_Kblock x_23758)
 159
 160 (** val cont_rect_Type0 :
 161     'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
 162     -> cont -> 'a1 **)
 163 let rec cont_rect_Type0 h_Kend h_Kseq h_Kblock = function
 164 | Kend -> h_Kend
 165 | Kseq (x_23764, x_23763) ->
 166   h_Kseq x_23764 x_23763 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23763)
 167 | Kblock x_23765 ->
 168   h_Kblock x_23765 (cont_rect_Type0 h_Kend h_Kseq h_Kblock x_23765)
 169
 170 (** val cont_inv_rect_Type4 :
 171     cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
 172     -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 173 let cont_inv_rect_Type4 hterm h1 h2 h3 =
 174   let hcut = cont_rect_Type4 h1 h2 h3 hterm in hcut __
 175
 176 (** val cont_inv_rect_Type3 :
 177     cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
 178     -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 179 let cont_inv_rect_Type3 hterm h1 h2 h3 =
 180   let hcut = cont_rect_Type3 h1 h2 h3 hterm in hcut __
 181
 182 (** val cont_inv_rect_Type2 :
 183     cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
 184     -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 185 let cont_inv_rect_Type2 hterm h1 h2 h3 =
 186   let hcut = cont_rect_Type2 h1 h2 h3 hterm in hcut __
 187
 188 (** val cont_inv_rect_Type1 :
 189     cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
 190     -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 191 let cont_inv_rect_Type1 hterm h1 h2 h3 =
 192   let hcut = cont_rect_Type1 h1 h2 h3 hterm in hcut __
 193
 194 (** val cont_inv_rect_Type0 :
 195     cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __
 196     -> 'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 197 let cont_inv_rect_Type0 hterm h1 h2 h3 =
 198   let hcut = cont_rect_Type0 h1 h2 h3 hterm in hcut __
 199
 200 (** val cont_discr : cont -> cont -> __ **)
 201 let cont_discr x y =
 202   Logic.eq_rect_Type2 x
 203     (match x with
 204      | Kend -> Obj.magic (fun _ dH -> dH)
 205      | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 206      | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
 207
 208 (** val cont_jmdiscr : cont -> cont -> __ **)
 209 let cont_jmdiscr x y =
 210   Logic.eq_rect_Type2 x
 211     (match x with
 212      | Kend -> Obj.magic (fun _ dH -> dH)
 213      | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
 214      | Kblock a0 -> Obj.magic (fun _ dH -> dH __)) y
 215
 216 type stack =
 217 | SStop
 218 | Scall of (AST.ident, AST.typ) Types.prod Types.option
 219    * Cminor_syntax.internal_function * Pointers.block * env * cont *
 220    stack
 221
 222 (** val stack_rect_Type4 :
 223     'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 224     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 225     cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
 226 let rec stack_rect_Type4 h_SStop h_Scall = function
 227 | SStop -> h_SStop
 228 | Scall (dest, f, x_23824, en, k, x_23820) ->
 229   h_Scall dest f x_23824 en __ __ k __ x_23820
 230     (stack_rect_Type4 h_SStop h_Scall x_23820)
 231
 232 (** val stack_rect_Type3 :
 233     'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 234     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 235     cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
 236 let rec stack_rect_Type3 h_SStop h_Scall = function
 237 | SStop -> h_SStop
 238 | Scall (dest, f, x_23840, en, k, x_23836) ->
 239   h_Scall dest f x_23840 en __ __ k __ x_23836
 240     (stack_rect_Type3 h_SStop h_Scall x_23836)
 241
 242 (** val stack_rect_Type2 :
 243     'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 244     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 245     cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
 246 let rec stack_rect_Type2 h_SStop h_Scall = function
 247 | SStop -> h_SStop
 248 | Scall (dest, f, x_23848, en, k, x_23844) ->
 249   h_Scall dest f x_23848 en __ __ k __ x_23844
 250     (stack_rect_Type2 h_SStop h_Scall x_23844)
 251
 252 (** val stack_rect_Type1 :
 253     'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 254     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 255     cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
 256 let rec stack_rect_Type1 h_SStop h_Scall = function
 257 | SStop -> h_SStop
 258 | Scall (dest, f, x_23856, en, k, x_23852) ->
 259   h_Scall dest f x_23856 en __ __ k __ x_23852
 260     (stack_rect_Type1 h_SStop h_Scall x_23852)
 261
 262 (** val stack_rect_Type0 :
 263     'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
 264     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 265     cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1 **)
 266 let rec stack_rect_Type0 h_SStop h_Scall = function
 267 | SStop -> h_SStop
 268 | Scall (dest, f, x_23864, en, k, x_23860) ->
 269   h_Scall dest f x_23864 en __ __ k __ x_23860
 270     (stack_rect_Type0 h_SStop h_Scall x_23860)
 271
 272 (** val stack_inv_rect_Type4 :
 273     stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 274     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 275     cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 276 let stack_inv_rect_Type4 hterm h1 h2 =
 277   let hcut = stack_rect_Type4 h1 h2 hterm in hcut __
 278
 279 (** val stack_inv_rect_Type3 :
 280     stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 281     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 282     cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 283 let stack_inv_rect_Type3 hterm h1 h2 =
 284   let hcut = stack_rect_Type3 h1 h2 hterm in hcut __
 285
 286 (** val stack_inv_rect_Type2 :
 287     stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 288     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 289     cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 290 let stack_inv_rect_Type2 hterm h1 h2 =
 291   let hcut = stack_rect_Type2 h1 h2 hterm in hcut __
 292
 293 (** val stack_inv_rect_Type1 :
 294     stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 295     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 296     cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 297 let stack_inv_rect_Type1 hterm h1 h2 =
 298   let hcut = stack_rect_Type1 h1 h2 hterm in hcut __
 299
 300 (** val stack_inv_rect_Type0 :
 301     stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
 302     Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
 303     cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
 304 let stack_inv_rect_Type0 hterm h1 h2 =
 305   let hcut = stack_rect_Type0 h1 h2 hterm in hcut __
 306
 307 (** val stack_jmdiscr : stack -> stack -> __ **)
 308 let stack_jmdiscr x y =
 309   Logic.eq_rect_Type2 x
 310     (match x with
 311      | SStop -> Obj.magic (fun _ dH -> dH)
 312      | Scall (a0, a1, a2, a3, a6, a8) ->
 313        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __)) y
 314
 315 type state =
 316 | State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
 317    * GenMem.mem * Pointers.block * cont * stack
 318 | Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
 319    * Values.val0 List.list * GenMem.mem * stack
 320 | Returnstate of Values.val0 Types.option * GenMem.mem * stack
 321 | Finalstate of Integers.int
 322
 323 (** val state_rect_Type4 :
 324     (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 325     -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 326     (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 327     List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 328     GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 329 let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
 330 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
 331 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
 332 | Returnstate (v, m, st) -> h_Returnstate v m st
 333 | Finalstate r -> h_Finalstate r
 334
 335 (** val state_rect_Type5 :
 336     (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 337     -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 338     (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 339     List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 340     GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 341 let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
 342 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
 343 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
 344 | Returnstate (v, m, st) -> h_Returnstate v m st
 345 | Finalstate r -> h_Finalstate r
 346
 347 (** val state_rect_Type3 :
 348     (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 349     -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 350     (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 351     List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 352     GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 353 let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
 354 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
 355 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
 356 | Returnstate (v, m, st) -> h_Returnstate v m st
 357 | Finalstate r -> h_Finalstate r
 358
 359 (** val state_rect_Type2 :
 360     (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 361     -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 362     (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 363     List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 364     GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 365 let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
 366 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
 367 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
 368 | Returnstate (v, m, st) -> h_Returnstate v m st
 369 | Finalstate r -> h_Finalstate r
 370
 371 (** val state_rect_Type1 :
 372     (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 373     -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 374     (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 375     List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 376     GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 377 let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
 378 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
 379 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
 380 | Returnstate (v, m, st) -> h_Returnstate v m st
 381 | Finalstate r -> h_Finalstate r
 382
 383 (** val state_rect_Type0 :
 384     (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
 385     -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
 386     (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
 387     List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
 388     GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1 **)
 389 let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
 390 | State (f, s, en, m, sp, k, st) -> h_State f s en __ __ m sp k __ st
 391 | Callstate (id, fd, args, m, st) -> h_Callstate id fd args m st
 392 | Returnstate (v, m, st) -> h_Returnstate v m st
 393 | Finalstate r -> h_Finalstate r
 394
 395 (** val state_inv_rect_Type4 :
 396     state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 397     __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 398     'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 399     Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
 400     (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
 401     (Integers.int -> __ -> 'a1) -> 'a1 **)
 402 let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
 403   let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
 404
 405 (** val state_inv_rect_Type3 :
 406     state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 407     __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 408     'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 409     Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
 410     (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
 411     (Integers.int -> __ -> 'a1) -> 'a1 **)
 412 let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
 413   let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
 414
 415 (** val state_inv_rect_Type2 :
 416     state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 417     __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 418     'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 419     Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
 420     (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
 421     (Integers.int -> __ -> 'a1) -> 'a1 **)
 422 let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
 423   let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
 424
 425 (** val state_inv_rect_Type1 :
 426     state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 427     __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 428     'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 429     Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
 430     (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
 431     (Integers.int -> __ -> 'a1) -> 'a1 **)
 432 let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
 433   let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
 434
 435 (** val state_inv_rect_Type0 :
 436     state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
 437     __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
 438     'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
 439     Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) ->
 440     (Values.val0 Types.option -> GenMem.mem -> stack -> __ -> 'a1) ->
 441     (Integers.int -> __ -> 'a1) -> 'a1 **)
 442 let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
 443   let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
 444
 445 (** val state_jmdiscr : state -> state -> __ **)
 446 let state_jmdiscr x y =
 447   Logic.eq_rect_Type2 x
 448     (match x with
 449      | State (a0, a1, a2, a5, a6, a7, a9) ->
 450        Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)
 451      | Callstate (a0, a1, a2, a3, a4) ->
 452        Obj.magic (fun _ dH -> dH __ __ __ __ __)
 453      | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
 454      | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
 455
 456 (** val eval_expr :
 457     genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
 458     GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res **)
 459 let rec eval_expr ge ty0 e en sp m =
 460   (match e with
 461    | Cminor_syntax.Id (x, i) ->
 462      (fun _ ->
 463        let r = Identifiers.lookup_present PreIdentifiers.SymbolTag en i in
 464        Errors.OK { Types.fst = Events.e0; Types.snd = r })
 465    | Cminor_syntax.Cst (x, c) ->
 466      (fun _ ->
 467        Obj.magic
 468          (Monad.m_bind0 (Monad.max_def Errors.res0)
 469            (Obj.magic
 470              (Errors.opt_to_res (Errors.msg ErrorMessages.FailedConstant)
 471                (FrontEndOps.eval_constant x (Globalenvs.find_symbol ge) sp c)))
 472            (fun r ->
 473            Obj.magic (Errors.OK { Types.fst = Events.e0; Types.snd = r }))))
 474    | Cminor_syntax.Op1 (ty, ty', op, e') ->
 475      (fun _ ->
 476        Obj.magic
 477          (Monad.m_bind2 (Monad.max_def Errors.res0)
 478            (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr v ->
 479            Monad.m_bind0 (Monad.max_def Errors.res0)
 480              (Obj.magic
 481                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 482                  (FrontEndOps.eval_unop ty ty' op v))) (fun r ->
 483              Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
 484    | Cminor_syntax.Op2 (ty1, ty2, ty', op, e1, e2) ->
 485      (fun _ ->
 486        Obj.magic
 487          (Monad.m_bind2 (Monad.max_def Errors.res0)
 488            (Obj.magic (eval_expr ge ty1 e1 en sp m)) (fun tr1 v1 ->
 489            Monad.m_bind2 (Monad.max_def Errors.res0)
 490              (Obj.magic (eval_expr ge ty2 e2 en sp m)) (fun tr2 v2 ->
 491              Monad.m_bind0 (Monad.max_def Errors.res0)
 492                (Obj.magic
 493                  (Errors.opt_to_res (Errors.msg ErrorMessages.FailedOp)
 494                    (FrontEndOps.eval_binop m ty1 ty2 ty' op v1 v2)))
 495                (fun r ->
 496                Obj.magic (Errors.OK { Types.fst = (Events.eapp tr1 tr2);
 497                  Types.snd = r }))))))
 498    | Cminor_syntax.Mem (ty, e0) ->
 499      (fun _ ->
 500        Obj.magic
 501          (Monad.m_bind2 (Monad.max_def Errors.res0)
 502            (Obj.magic (eval_expr ge AST.ASTptr e0 en sp m)) (fun tr v ->
 503            Monad.m_bind0 (Monad.max_def Errors.res0)
 504              (Obj.magic
 505                (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad)
 506                  (FrontEndMem.loadv ty m v))) (fun r ->
 507              Obj.magic (Errors.OK { Types.fst = tr; Types.snd = r })))))
 508    | Cminor_syntax.Cond (sz, sg, ty, e', e1, e2) ->
 509      (fun _ ->
 510        Obj.magic
 511          (Monad.m_bind2 (Monad.max_def Errors.res0)
 512            (Obj.magic (eval_expr ge (AST.ASTint (sz, sg)) e' en sp m))
 513            (fun tr v ->
 514            Monad.m_bind0 (Monad.max_def Errors.res0)
 515              (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
 516              Monad.m_bind2 (Monad.max_def Errors.res0)
 517                (Obj.magic
 518                  (eval_expr ge ty
 519                    (match b with
 520                     | Bool.True -> e1
 521                     | Bool.False -> e2) en sp m)) (fun tr' r ->
 522                Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
 523                  Types.snd = r }))))))
 524    | Cminor_syntax.Ecost (ty, l, e') ->
 525      (fun _ ->
 526        Obj.magic
 527          (Monad.m_bind2 (Monad.max_def Errors.res0)
 528            (Obj.magic (eval_expr ge ty e' en sp m)) (fun tr r ->
 529            Obj.magic (Errors.OK { Types.fst =
 530              (Events.eapp (Events.echarge l) tr); Types.snd = r }))))) __
 531
 532 (** val k_exit :
 533     Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
 534     Types.sig0 Errors.res **)
 535 let rec k_exit n k f en =
 536   (match k with
 537    | Kend -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.BadState))
 538    | Kseq (x, k') -> (fun _ -> k_exit n k' f en)
 539    | Kblock k' ->
 540      (fun _ ->
 541        match n with
 542        | Nat.O -> Errors.OK k'
 543        | Nat.S m -> k_exit m k' f en)) __
 544
 545 (** val find_case :
 546     AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1
 547     -> 'a1 **)
 548 let rec find_case sz i cs default =
 549   match cs with
 550   | List.Nil -> default
 551   | List.Cons (h, t) ->
 552     let { Types.fst = hi; Types.snd = a } = h in
 553     (match BitVector.eq_bv (AST.bitsize_of_intsize sz) i hi with
 554      | Bool.True -> a
 555      | Bool.False -> find_case sz i t default)
 556
 557 (** val find_label :
 558     PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
 559     Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
 560     Types.prod Types.sig0 Types.option **)
 561 let rec find_label l s k f en =
 562   (match s with
 563    | Cminor_syntax.St_skip -> (fun _ -> Types.None)
 564    | Cminor_syntax.St_assign (x, x0, x1) -> (fun _ -> Types.None)
 565    | Cminor_syntax.St_store (x, x0, x1) -> (fun _ -> Types.None)
 566    | Cminor_syntax.St_call (x, x0, x1) -> (fun _ -> Types.None)
 567    | Cminor_syntax.St_seq (s1, s2) ->
 568      (fun _ ->
 569        match find_label l s1 (Kseq (s2, k)) f en with
 570        | Types.None -> find_label l s2 k f en
 571        | Types.Some sk -> Types.Some sk)
 572    | Cminor_syntax.St_ifthenelse (x, x0, x1, s1, s2) ->
 573      (fun _ ->
 574        match find_label l s1 k f en with
 575        | Types.None -> find_label l s2 k f en
 576        | Types.Some sk -> Types.Some sk)
 577    | Cminor_syntax.St_return x -> (fun _ -> Types.None)
 578    | Cminor_syntax.St_label (l', s') ->
 579      (fun _ ->
 580        match Identifiers.identifier_eq PreIdentifiers.Label l l' with
 581        | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
 582        | Types.Inr _ -> find_label l s' k f en)
 583    | Cminor_syntax.St_goto x -> (fun _ -> Types.None)
 584    | Cminor_syntax.St_cost (x, s') -> (fun _ -> find_label l s' k f en)) __
 585
 586 (** val find_label_always :
 587     PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
 588     Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
 589     Types.prod Types.sig0 **)
 590 let find_label_always l s k f en =
 591   (match find_label l s k f en with
 592    | Types.None -> (fun _ -> assert false (* absurd case *))
 593    | Types.Some sk -> (fun _ -> sk)) __
 594
 595 (** val bind_params :
 596     Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
 597     Types.sig0 Errors.res **)
 598 let rec bind_params vs ids =
 599   match vs with
 600   | List.Nil ->
 601     (match ids with
 602      | List.Nil -> Errors.OK (Identifiers.empty_map PreIdentifiers.SymbolTag)
 603      | List.Cons (x, x0) ->
 604        Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters))
 605   | List.Cons (v, vt) ->
 606     (match ids with
 607      | List.Nil ->
 608        Errors.Error (Errors.msg ErrorMessages.WrongNumberOfParameters)
 609      | List.Cons (idh, idt) ->
 610        let { Types.fst = id; Types.snd = ty } = idh in
 611        Obj.magic
 612          (Monad.m_bind0 (Monad.max_def Errors.res0)
 613            (Obj.magic (bind_params vt idt)) (fun en ->
 614            Obj.magic (Errors.OK
 615              (Identifiers.add PreIdentifiers.SymbolTag (Types.pi1 en)
 616                idh.Types.fst v)))))
 617
 618 (** val init_locals :
 619     env -> (AST.ident, AST.typ) Types.prod List.list -> env **)
 620 let init_locals =
 621   List.foldr (fun idty en ->
 622     Identifiers.add PreIdentifiers.SymbolTag en idty.Types.fst Values.Vundef)
 623
 624 (** val trace_map_inv :
 625     ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
 626     -> (Events.trace, 'a2 List.list) Types.prod Errors.res **)
 627 let rec trace_map_inv f l =
 628   (match l with
 629    | List.Nil ->
 630      (fun _ -> Errors.OK { Types.fst = Events.e0; Types.snd = List.Nil })
 631    | List.Cons (h, t) ->
 632      (fun _ ->
 633        Obj.magic
 634          (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic f h __)
 635            (fun tr h' ->
 636            Monad.m_bind2 (Monad.max_def Errors.res0)
 637              (Obj.magic (trace_map_inv f t)) (fun tr' t' ->
 638              Obj.magic (Errors.OK { Types.fst = (Events.eapp tr tr');
 639                Types.snd = (List.Cons (h', t')) })))))) __
 640
 641 (** val eval_step :
 642     genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
 643     IOMonad.iO **)
 644 let eval_step ge = function
 645 | State (f, s, en, m, sp, k, st0) ->
 646   IOMonad.err_to_io
 647     ((match s with
 648       | Cminor_syntax.St_skip ->
 649         (fun _ ->
 650           (match k with
 651            | Kend ->
 652              (fun _ ->
 653                Obj.magic
 654                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 655                    Events.e0; Types.snd = (Returnstate (Types.None,
 656                    (GenMem.free m sp), st0)) }))
 657            | Kseq (s', k') ->
 658              (fun _ ->
 659                Obj.magic
 660                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 661                    Events.e0; Types.snd = (State (f, s', en, m, sp, k',
 662                    st0)) }))
 663            | Kblock k' ->
 664              (fun _ ->
 665                Obj.magic
 666                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 667                    Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
 668                    en, m, sp, k', st0)) }))) __)
 669       | Cminor_syntax.St_assign (x, id, e) ->
 670         (fun _ ->
 671           Obj.magic
 672             (Monad.m_bind2 (Monad.max_def Errors.res0)
 673               (Obj.magic (eval_expr ge x e en sp m)) (fun tr v ->
 674               let en' =
 675                 Identifiers.update_present PreIdentifiers.SymbolTag en id v
 676               in
 677               Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
 678                 Types.snd = (State (f, Cminor_syntax.St_skip, en', m, sp, k,
 679                 st0)) })))
 680       | Cminor_syntax.St_store (ty, edst, e) ->
 681         (fun _ ->
 682           Obj.magic
 683             (Monad.m_bind2 (Monad.max_def Errors.res0)
 684               (Obj.magic (eval_expr ge AST.ASTptr edst en sp m))
 685               (fun tr vdst ->
 686               Monad.m_bind2 (Monad.max_def Errors.res0)
 687                 (Obj.magic (eval_expr ge ty e en sp m)) (fun tr' v ->
 688                 Monad.m_bind0 (Monad.max_def Errors.res0)
 689                   (Obj.magic
 690                     (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore)
 691                       (FrontEndMem.storev ty m vdst v))) (fun m' ->
 692                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 693                     (Events.eapp tr tr'); Types.snd = (State (f,
 694                     Cminor_syntax.St_skip, en, m', sp, k, st0)) })))))
 695       | Cminor_syntax.St_call (dst, ef, args) ->
 696         (fun _ ->
 697           Obj.magic
 698             (Monad.m_bind2 (Monad.max_def Errors.res0)
 699               (Obj.magic (eval_expr ge AST.ASTptr ef en sp m)) (fun tr vf ->
 700               Monad.m_bind2 (Monad.max_def Errors.res0)
 701                 (Obj.magic
 702                   (Errors.opt_to_res
 703                     (Errors.msg ErrorMessages.BadFunctionValue)
 704                     (Globalenvs.find_funct_id ge vf))) (fun fd id ->
 705                 Monad.m_bind2 (Monad.max_def Errors.res0)
 706                   (Obj.magic
 707                     (trace_map_inv (fun e ->
 708                       let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
 709                       (fun _ -> eval_expr ge ty e0 en sp m)) args))
 710                   (fun tr' vargs ->
 711                   Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 712                     (Events.eapp tr tr'); Types.snd = (Callstate (id, fd,
 713                     vargs, m, (Scall (dst, f, sp, en, k, st0)))) })))))
 714       | Cminor_syntax.St_seq (s1, s2) ->
 715         (fun _ ->
 716           Obj.magic
 717             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 718               Events.e0; Types.snd = (State (f, s1, en, m, sp, (Kseq (s2,
 719               k)), st0)) }))
 720       | Cminor_syntax.St_ifthenelse (x, x0, e, strue, sfalse) ->
 721         (fun _ ->
 722           Obj.magic
 723             (Monad.m_bind2 (Monad.max_def Errors.res0)
 724               (Obj.magic (eval_expr ge (AST.ASTint (x, x0)) e en sp m))
 725               (fun tr v ->
 726               Monad.m_bind0 (Monad.max_def Errors.res0)
 727                 (Obj.magic (Values.eval_bool_of_val v)) (fun b ->
 728                 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
 729                   Types.snd = (State (f,
 730                   (match b with
 731                    | Bool.True -> strue
 732                    | Bool.False -> sfalse), en, m, sp, k, st0)) }))))
 733       | Cminor_syntax.St_return eo ->
 734         (match eo with
 735          | Types.None ->
 736            (fun _ ->
 737              Obj.magic
 738                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 739                  Events.e0; Types.snd = (Returnstate (Types.None,
 740                  (GenMem.free m sp), st0)) }))
 741          | Types.Some e ->
 742            let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
 743            (fun _ ->
 744            Obj.magic
 745              (Monad.m_bind2 (Monad.max_def Errors.res0)
 746                (Obj.magic (eval_expr ge ty e0 en sp m)) (fun tr v ->
 747                Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = tr;
 748                  Types.snd = (Returnstate ((Types.Some v),
 749                  (GenMem.free m sp), st0)) }))))
 750       | Cminor_syntax.St_label (l, s') ->
 751         (fun _ ->
 752           Obj.magic
 753             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 754               Events.e0; Types.snd = (State (f, s', en, m, sp, k, st0)) }))
 755       | Cminor_syntax.St_goto l ->
 756         (fun _ ->
 757           let sk = find_label_always l f.Cminor_syntax.f_body Kend f en in
 758           Obj.magic
 759             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 760               Events.e0; Types.snd = (State (f, sk.Types.fst, en, m, sp,
 761               sk.Types.snd, st0)) }))
 762       | Cminor_syntax.St_cost (l, s') ->
 763         (fun _ ->
 764           Obj.magic
 765             (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 766               (Events.echarge l); Types.snd = (State (f, s', en, m, sp, k,
 767               st0)) }))) __)
 768 | Callstate (x, fd, args, m, st0) ->
 769   (match fd with
 770    | AST.Internal f ->
 771      IOMonad.err_to_io
 772        (let { Types.fst = m'; Types.snd = sp } =
 773           GenMem.alloc m (Z.z_of_nat Nat.O)
 774             (Z.z_of_nat f.Cminor_syntax.f_stacksize)
 775         in
 776        Obj.magic
 777          (Monad.m_bind0 (Monad.max_def Errors.res0)
 778            (Obj.magic (bind_params args f.Cminor_syntax.f_params)) (fun en ->
 779            Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 780              Events.e0; Types.snd = (State (f, f.Cminor_syntax.f_body,
 781              (init_locals (Types.pi1 en) f.Cminor_syntax.f_vars), m', sp,
 782              Kend, st0)) })))
 783    | AST.External fn ->
 784      Obj.magic
 785        (Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
 786          (Obj.magic
 787            (IOMonad.err_to_io
 788              (IO.check_eventval_list args fn.AST.ef_sig.AST.sig_args)))
 789          (fun evargs ->
 790          Monad.m_bind0 (Monad.max_def IOMonad.iOMonad)
 791            (Obj.magic
 792              (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig)))
 793            (fun evres ->
 794            let res =
 795              match fn.AST.ef_sig.AST.sig_res with
 796              | Types.None -> Types.None
 797              | Types.Some x0 ->
 798                Types.Some (IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres)
 799            in
 800            Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { Types.fst =
 801              (Events.eextcall fn.AST.ef_id evargs
 802                (IO.mk_eventval (AST.proj_sig_res fn.AST.ef_sig) evres));
 803              Types.snd = (Returnstate (res, m, st0)) }))))
 804 | Returnstate (result, m, st0) ->
 805   IOMonad.err_to_io
 806     (match st0 with
 807      | SStop ->
 808        (match result with
 809         | Types.None ->
 810           Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
 811         | Types.Some v ->
 812           (match v with
 813            | Values.Vundef ->
 814              Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
 815            | Values.Vint (sz, r) ->
 816              (match sz with
 817               | AST.I8 ->
 818                 (fun x -> Errors.Error
 819                   (Errors.msg ErrorMessages.ReturnMismatch))
 820               | AST.I16 ->
 821                 (fun x -> Errors.Error
 822                   (Errors.msg ErrorMessages.ReturnMismatch))
 823               | AST.I32 ->
 824                 (fun r0 ->
 825                   Obj.magic
 826                     (Monad.m_return0 (Monad.max_def Errors.res0)
 827                       { Types.fst = Events.e0; Types.snd = (Finalstate r0) })))
 828                r
 829            | Values.Vnull ->
 830              Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
 831            | Values.Vptr x ->
 832              Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)))
 833      | Scall (dst, f, sp, en, k, st') ->
 834        (match result with
 835         | Types.None ->
 836           (match dst with
 837            | Types.None ->
 838              Obj.magic
 839                (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 840                  Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip, en,
 841                  m, sp, k, st')) })
 842            | Types.Some x ->
 843              Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
 844         | Types.Some v ->
 845           (match dst with
 846            | Types.None ->
 847              (fun _ -> Errors.Error
 848                (Errors.msg ErrorMessages.ReturnMismatch))
 849            | Types.Some idty ->
 850              (fun _ ->
 851                Obj.magic
 852                  (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
 853                    Events.e0; Types.snd = (State (f, Cminor_syntax.St_skip,
 854                    (Identifiers.update_present PreIdentifiers.SymbolTag en
 855                      idty.Types.fst v), m, sp, k, st')) }))) __))
 856 | Finalstate r ->
 857   IOMonad.err_to_io (Errors.Error (Errors.msg ErrorMessages.BadState))
 858
 859 (** val is_final : state -> Integers.int Types.option **)
 860 let is_final = function
 861 | State (x, x0, x1, x4, x5, x6, x8) -> Types.None
 862 | Callstate (x, x0, x1, x2, x3) -> Types.None
 863 | Returnstate (x, x0, x1) -> Types.None
 864 | Finalstate r -> Types.Some r
 865
 866 (** val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system **)
 867 let cminor_exec =
 868   { SmallstepExec.is_final = (fun x -> Obj.magic is_final);
 869     SmallstepExec.step = (Obj.magic eval_step) }
 870
 871 (** val make_global : Cminor_syntax.cminor_program -> genv **)
 872 let make_global p =
 873   Globalenvs.globalenv (fun x -> x) p
 874
 875 (** val make_initial_state :
 876     Cminor_syntax.cminor_program -> state Errors.res **)
 877 let make_initial_state p =
 878   let ge = make_global p in
 879   Obj.magic
 880     (Monad.m_bind0 (Monad.max_def Errors.res0)
 881       (Obj.magic (Globalenvs.init_mem (fun x -> x) p)) (fun m ->
 882       Monad.m_bind0 (Monad.max_def Errors.res0)
 883         (Obj.magic
 884           (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
 885             (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
 886         Monad.m_bind0 (Monad.max_def Errors.res0)
 887           (Obj.magic
 888             (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
 889               (Globalenvs.find_funct_ptr ge b))) (fun f ->
 890           Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
 891             SStop)))))))
 892
 893 (** val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
 894 let cminor_fullexec =
 895   { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
 896     (Obj.magic make_global); SmallstepExec.make_initial_state =
 897     (Obj.magic make_initial_state) }
 898
 899 (** val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv **)
 900 let make_noinit_global p =
 901   Globalenvs.globalenv (fun x -> List.Cons ((AST.Init_space x), List.Nil)) p
 902
 903 (** val make_initial_noinit_state :
 904     Cminor_syntax.cminor_noinit_program -> state Errors.res **)
 905 let make_initial_noinit_state p =
 906   let ge = make_noinit_global p in
 907   Obj.magic
 908     (Monad.m_bind0 (Monad.max_def Errors.res0)
 909       (Obj.magic
 910         (Globalenvs.init_mem (fun x -> List.Cons ((AST.Init_space x),
 911           List.Nil)) p)) (fun m ->
 912       Monad.m_bind0 (Monad.max_def Errors.res0)
 913         (Obj.magic
 914           (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
 915             (Globalenvs.find_symbol ge p.AST.prog_main))) (fun b ->
 916         Monad.m_bind0 (Monad.max_def Errors.res0)
 917           (Obj.magic
 918             (Errors.opt_to_res (Errors.msg ErrorMessages.MainMissing)
 919               (Globalenvs.find_funct_ptr ge b))) (fun f ->
 920           Obj.magic (Errors.OK (Callstate (p.AST.prog_main, f, List.Nil, m,
 921             SStop)))))))
 922
 923 (** val cminor_noinit_fullexec :
 924     (IO.io_out, IO.io_in) SmallstepExec.fullexec **)
 925 let cminor_noinit_fullexec =
 926   { SmallstepExec.es1 = cminor_exec; SmallstepExec.make_global =
 927     (Obj.magic make_noinit_global); SmallstepExec.make_initial_state =
 928     (Obj.magic make_initial_noinit_state) }
 929