open Preamble

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Errors

open Extra_bool

open Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open Globalenvs

open CostLabel

open Events

open IOMonad

open IO

open SmallstepExec

open BitVectorTrie

open Graphs

open Order

open Registers

open FrontEndOps

open RTLabs_syntax

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

type frame = { func : RTLabs_syntax.internal_function;
               locals : Values.val0 Registers.register_env;
               next : Graphs.label; sp : Pointers.block;
               retdst : Registers.register Types.option }

val frame_rect_Type4 :
  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
  'a1) -> frame -> 'a1

val frame_rect_Type5 :
  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
  'a1) -> frame -> 'a1

val frame_rect_Type3 :
  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
  'a1) -> frame -> 'a1

val frame_rect_Type2 :
  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
  'a1) -> frame -> 'a1

val frame_rect_Type1 :
  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
  'a1) -> frame -> 'a1

val frame_rect_Type0 :
  (RTLabs_syntax.internal_function -> Values.val0 Registers.register_env ->
  Graphs.label -> __ -> Pointers.block -> Registers.register Types.option ->
  'a1) -> frame -> 'a1

val func : frame -> RTLabs_syntax.internal_function

val locals : frame -> Values.val0 Registers.register_env

val next : frame -> Graphs.label

val sp : frame -> Pointers.block

val retdst : frame -> Registers.register Types.option

val frame_inv_rect_Type4 :
  frame -> (RTLabs_syntax.internal_function -> Values.val0
  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
  Registers.register Types.option -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type3 :
  frame -> (RTLabs_syntax.internal_function -> Values.val0
  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
  Registers.register Types.option -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type2 :
  frame -> (RTLabs_syntax.internal_function -> Values.val0
  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
  Registers.register Types.option -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type1 :
  frame -> (RTLabs_syntax.internal_function -> Values.val0
  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
  Registers.register Types.option -> __ -> 'a1) -> 'a1

val frame_inv_rect_Type0 :
  frame -> (RTLabs_syntax.internal_function -> Values.val0
  Registers.register_env -> Graphs.label -> __ -> Pointers.block ->
  Registers.register Types.option -> __ -> 'a1) -> 'a1

val frame_jmdiscr : frame -> frame -> __

val adv : Graphs.label -> frame -> frame

type state =
| State of frame * frame List.list * GenMem.mem
| Callstate of AST.ident * RTLabs_syntax.internal_function AST.fundef
   * Values.val0 List.list * Registers.register Types.option
   * frame List.list * GenMem.mem
| Returnstate of Values.val0 Types.option * Registers.register Types.option
   * frame List.list * GenMem.mem
| Finalstate of Integers.int

val state_rect_Type4 :
  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
  (Values.val0 Types.option -> Registers.register Types.option -> frame
  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type5 :
  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
  (Values.val0 Types.option -> Registers.register Types.option -> frame
  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type3 :
  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
  (Values.val0 Types.option -> Registers.register Types.option -> frame
  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type2 :
  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
  (Values.val0 Types.option -> Registers.register Types.option -> frame
  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type1 :
  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
  (Values.val0 Types.option -> Registers.register Types.option -> frame
  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type0 :
  (frame -> frame List.list -> GenMem.mem -> 'a1) -> (AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem -> 'a1) ->
  (Values.val0 Types.option -> Registers.register Types.option -> frame
  List.list -> GenMem.mem -> 'a1) -> (Integers.int -> 'a1) -> state -> 'a1

val state_inv_rect_Type4 :
  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
  List.list -> Registers.register Types.option -> frame List.list ->
  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type3 :
  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
  List.list -> Registers.register Types.option -> frame List.list ->
  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type2 :
  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
  List.list -> Registers.register Types.option -> frame List.list ->
  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type1 :
  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
  List.list -> Registers.register Types.option -> frame List.list ->
  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type0 :
  state -> (frame -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (AST.ident -> RTLabs_syntax.internal_function AST.fundef -> Values.val0
  List.list -> Registers.register Types.option -> frame List.list ->
  GenMem.mem -> __ -> 'a1) -> (Values.val0 Types.option -> Registers.register
  Types.option -> frame List.list -> GenMem.mem -> __ -> 'a1) ->
  (Integers.int -> __ -> 'a1) -> 'a1

val state_jmdiscr : state -> state -> __

val build_state :
  frame -> frame List.list -> GenMem.mem -> Graphs.label -> state

val next_instruction : frame -> RTLabs_syntax.statement

val init_locals :
  (Registers.register, AST.typ) Types.prod List.list -> Values.val0
  Registers.register_env

val reg_store :
  PreIdentifiers.identifier -> Values.val0 -> Values.val0
  Identifiers.identifier_map -> Values.val0 Identifiers.identifier_map
  Errors.res

val params_store :
  (Registers.register, AST.typ) Types.prod List.list -> Values.val0 List.list
  -> Values.val0 Registers.register_env -> Values.val0 Registers.register_env
  Errors.res

val reg_retrieve :
  Values.val0 Registers.register_env -> Registers.register -> Values.val0
  Errors.res

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

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

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

val make_global : RTLabs_syntax.rTLabs_program -> genv

val make_initial_state : RTLabs_syntax.rTLabs_program -> state Errors.res

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

val bind_ok :
  'a1 Errors.res -> ('a1 -> 'a2 Errors.res) -> 'a2 -> ('a1 -> __ -> __ ->
  'a3) -> 'a3

val jmeq_hackT : 'a1 -> 'a1 -> (__ -> 'a2) -> 'a2

val func_block_of_exec :
  genv -> state -> Events.trace -> AST.ident ->
  RTLabs_syntax.internal_function AST.fundef -> Values.val0 List.list ->
  Registers.register Types.option -> frame List.list -> GenMem.mem ->
  Pointers.block Types.sig0