open Preamble

open CostLabel

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Coqlib

open Values

open Events

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

open IOMonad

open IO

open Extra_bool

open Globalenvs

open SmallstepExec

open FrontEndOps

open Cminor_syntax

type env = Values.val0 Identifiers.identifier_map

type genv = Cminor_syntax.internal_function AST.fundef Globalenvs.genv_t

type cont =
| Kend
| Kseq of Cminor_syntax.stmt * cont
| Kblock of cont

val cont_rect_Type4 :
  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
  -> cont -> 'a1

val cont_rect_Type3 :
  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
  -> cont -> 'a1

val cont_rect_Type2 :
  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
  -> cont -> 'a1

val cont_rect_Type1 :
  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
  -> cont -> 'a1

val cont_rect_Type0 :
  'a1 -> (Cminor_syntax.stmt -> cont -> 'a1 -> 'a1) -> (cont -> 'a1 -> 'a1)
  -> cont -> 'a1

val cont_inv_rect_Type4 :
  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type3 :
  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type2 :
  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type1 :
  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type0 :
  cont -> (__ -> 'a1) -> (Cminor_syntax.stmt -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_discr : cont -> cont -> __

val cont_jmdiscr : cont -> cont -> __

type stack =
| SStop
| Scall of (AST.ident, AST.typ) Types.prod Types.option
   * Cminor_syntax.internal_function * Pointers.block * env * cont * 
   stack

val stack_rect_Type4 :
  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1

val stack_rect_Type3 :
  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1

val stack_rect_Type2 :
  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1

val stack_rect_Type1 :
  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1

val stack_rect_Type0 :
  'a1 -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> 'a1 -> 'a1) -> stack -> 'a1

val stack_inv_rect_Type4 :
  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val stack_inv_rect_Type3 :
  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val stack_inv_rect_Type2 :
  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val stack_inv_rect_Type1 :
  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val stack_inv_rect_Type0 :
  stack -> (__ -> 'a1) -> ((AST.ident, AST.typ) Types.prod Types.option ->
  Cminor_syntax.internal_function -> Pointers.block -> env -> __ -> __ ->
  cont -> __ -> stack -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val stack_jmdiscr : stack -> stack -> __

type state =
| State of Cminor_syntax.internal_function * Cminor_syntax.stmt * env
   * GenMem.mem * Pointers.block * cont * stack
| Callstate of AST.ident * Cminor_syntax.internal_function AST.fundef
   * Values.val0 List.list * GenMem.mem * stack
| Returnstate of Values.val0 Types.option * GenMem.mem * stack
| Finalstate of Integers.int

val state_rect_Type4 :
  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type5 :
  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type3 :
  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type2 :
  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type1 :
  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type0 :
  (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env -> __ -> __
  -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> 'a1) ->
  (AST.ident -> Cminor_syntax.internal_function AST.fundef -> Values.val0
  List.list -> GenMem.mem -> stack -> 'a1) -> (Values.val0 Types.option ->
  GenMem.mem -> stack -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_inv_rect_Type4 :
  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
  'a1) -> 'a1

val state_inv_rect_Type3 :
  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
  'a1) -> 'a1

val state_inv_rect_Type2 :
  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
  'a1) -> 'a1

val state_inv_rect_Type1 :
  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
  'a1) -> 'a1

val state_inv_rect_Type0 :
  state -> (Cminor_syntax.internal_function -> Cminor_syntax.stmt -> env ->
  __ -> __ -> GenMem.mem -> Pointers.block -> cont -> __ -> stack -> __ ->
  'a1) -> (AST.ident -> Cminor_syntax.internal_function AST.fundef ->
  Values.val0 List.list -> GenMem.mem -> stack -> __ -> 'a1) -> (Values.val0
  Types.option -> GenMem.mem -> stack -> __ -> 'a1) -> (Integers.int -> __ ->
  'a1) -> 'a1

val state_jmdiscr : state -> state -> __

val eval_expr :
  genv -> AST.typ -> Cminor_syntax.expr -> env -> Pointers.block ->
  GenMem.mem -> (Events.trace, Values.val0) Types.prod Errors.res

val k_exit :
  Nat.nat -> cont -> Cminor_syntax.internal_function -> env -> cont
  Types.sig0 Errors.res

val find_case :
  AST.intsize -> AST.bvint -> (AST.bvint, 'a1) Types.prod List.list -> 'a1 ->
  'a1

val find_label :
  PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
  Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
  Types.prod Types.sig0 Types.option

val find_label_always :
  PreIdentifiers.identifier -> Cminor_syntax.stmt -> cont ->
  Cminor_syntax.internal_function -> env -> (Cminor_syntax.stmt, cont)
  Types.prod Types.sig0

val bind_params :
  Values.val0 List.list -> (AST.ident, AST.typ) Types.prod List.list -> env
  Types.sig0 Errors.res

val init_locals : env -> (AST.ident, AST.typ) Types.prod List.list -> env

val trace_map_inv :
  ('a1 -> __ -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list
  -> (Events.trace, 'a2 List.list) Types.prod Errors.res

val eval_step :
  genv -> state -> (IO.io_out, IO.io_in, (Events.trace, state) Types.prod)
  IOMonad.iO

val is_final : state -> Integers.int Types.option

val cminor_exec : (IO.io_out, IO.io_in) SmallstepExec.trans_system

val make_global : Cminor_syntax.cminor_program -> genv

val make_initial_state : Cminor_syntax.cminor_program -> state Errors.res

val cminor_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec

val make_noinit_global : Cminor_syntax.cminor_noinit_program -> genv

val make_initial_noinit_state :
  Cminor_syntax.cminor_noinit_program -> state Errors.res

val cminor_noinit_fullexec : (IO.io_out, IO.io_in) SmallstepExec.fullexec