open Preamble

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Lists

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 Identifiers

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open ErrorMessages

open Positive

open PreIdentifiers

open Errors

open Globalenvs

open CostLabel

open FrontEndOps

open Cminor_syntax

open BitVectorTrie

open Graphs

open Order

open Registers

open RTLabs_syntax

type env =
  (Registers.register, AST.typ) Types.prod Identifiers.identifier_map

val populate_env :
  env -> Identifiers.universe -> (AST.ident, AST.typ) Types.prod List.list ->
  (((Registers.register, AST.typ) Types.prod List.list, env) Types.prod,
  Identifiers.universe) Types.prod

val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register

type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
               fx_rettyp : AST.typ Types.option }

val fixed_rect_Type4 :
  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
  -> 'a1

val fixed_rect_Type5 :
  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
  -> 'a1

val fixed_rect_Type3 :
  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
  -> 'a1

val fixed_rect_Type2 :
  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
  -> 'a1

val fixed_rect_Type1 :
  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
  -> 'a1

val fixed_rect_Type0 :
  (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) -> fixed
  -> 'a1

val fx_gotos : fixed -> Identifiers.identifier_set

val fx_env : fixed -> env

val fx_rettyp : fixed -> AST.typ Types.option

val fixed_inv_rect_Type4 :
  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
  -> 'a1) -> 'a1

val fixed_inv_rect_Type3 :
  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
  -> 'a1) -> 'a1

val fixed_inv_rect_Type2 :
  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
  -> 'a1) -> 'a1

val fixed_inv_rect_Type1 :
  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
  -> 'a1) -> 'a1

val fixed_inv_rect_Type0 :
  fixed -> (Identifiers.identifier_set -> env -> AST.typ Types.option -> __
  -> 'a1) -> 'a1

val fixed_discr : fixed -> fixed -> __

val fixed_jmdiscr : fixed -> fixed -> __

type resultok = __

type goto_map =
  PreIdentifiers.identifier Identifiers.identifier_map
  (* singleton inductive, whose constructor was mk_goto_map *)

val goto_map_rect_Type4 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1

val goto_map_rect_Type5 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1

val goto_map_rect_Type3 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1

val goto_map_rect_Type2 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1

val goto_map_rect_Type1 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1

val goto_map_rect_Type0 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (PreIdentifiers.identifier
  Identifiers.identifier_map -> __ -> __ -> 'a1) -> goto_map -> 'a1

val gm_map :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map

val goto_map_inv_rect_Type4 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
  'a1) -> 'a1

val goto_map_inv_rect_Type3 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
  'a1) -> 'a1

val goto_map_inv_rect_Type2 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
  'a1) -> 'a1

val goto_map_inv_rect_Type1 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
  'a1) -> 'a1

val goto_map_inv_rect_Type0 :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> __ ->
  'a1) -> 'a1

val goto_map_discr :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __

val goto_map_jmdiscr :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map -> goto_map -> __

val dpi1__o__gm_map__o__inject :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
  Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map
  Types.sig0

val eject__o__gm_map__o__inject :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0

val gm_map__o__inject :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0

val dpi1__o__gm_map :
  fixed -> RTLabs_syntax.statement Graphs.graph -> (goto_map, 'a1)
  Types.dPair -> PreIdentifiers.identifier Identifiers.identifier_map

val eject__o__gm_map :
  fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map Types.sig0 ->
  PreIdentifiers.identifier Identifiers.identifier_map

type partial_fn = { pf_labgen : Identifiers.universe;
                    pf_reggen : Identifiers.universe;
                    pf_params : (Registers.register, AST.typ) Types.prod
                                List.list;
                    pf_locals : (Registers.register, AST.typ) Types.prod
                                List.list; pf_result : resultok;
                    pf_stacksize : Nat.nat;
                    pf_graph : RTLabs_syntax.statement Graphs.graph;
                    pf_gotos : goto_map;
                    pf_labels : PreIdentifiers.identifier
                                Identifiers.identifier_map Types.sig0;
                    pf_entry : Graphs.label Types.sig0;
                    pf_exit : Graphs.label Types.sig0 }

val partial_fn_rect_Type4 :
  fixed -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
  partial_fn -> 'a1

val partial_fn_rect_Type5 :
  fixed -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
  partial_fn -> 'a1

val partial_fn_rect_Type3 :
  fixed -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
  partial_fn -> 'a1

val partial_fn_rect_Type2 :
  fixed -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
  partial_fn -> 'a1

val partial_fn_rect_Type1 :
  fixed -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
  partial_fn -> 'a1

val partial_fn_rect_Type0 :
  fixed -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> 'a1) ->
  partial_fn -> 'a1

val pf_labgen : fixed -> partial_fn -> Identifiers.universe

val pf_reggen : fixed -> partial_fn -> Identifiers.universe

val pf_params :
  fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list

val pf_locals :
  fixed -> partial_fn -> (Registers.register, AST.typ) Types.prod List.list

val pf_result : fixed -> partial_fn -> resultok

val pf_stacksize : fixed -> partial_fn -> Nat.nat

val pf_graph : fixed -> partial_fn -> RTLabs_syntax.statement Graphs.graph

val pf_gotos : fixed -> partial_fn -> goto_map

val pf_labels :
  fixed -> partial_fn -> PreIdentifiers.identifier Identifiers.identifier_map
  Types.sig0

val pf_entry : fixed -> partial_fn -> Graphs.label Types.sig0

val pf_exit : fixed -> partial_fn -> Graphs.label Types.sig0

val partial_fn_inv_rect_Type4 :
  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
  'a1

val partial_fn_inv_rect_Type3 :
  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
  'a1

val partial_fn_inv_rect_Type2 :
  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
  'a1

val partial_fn_inv_rect_Type1 :
  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
  'a1

val partial_fn_inv_rect_Type0 :
  fixed -> partial_fn -> (Identifiers.universe -> Identifiers.universe ->
  (Registers.register, AST.typ) Types.prod List.list -> (Registers.register,
  AST.typ) Types.prod List.list -> resultok -> __ -> Nat.nat ->
  RTLabs_syntax.statement Graphs.graph -> __ -> goto_map ->
  PreIdentifiers.identifier Identifiers.identifier_map Types.sig0 -> __ ->
  Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> __ -> __ -> 'a1) ->
  'a1

val partial_fn_jmdiscr : fixed -> partial_fn -> partial_fn -> __

val fn_contains_rect_Type4 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_rect_Type5 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_rect_Type3 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_rect_Type2 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_rect_Type1 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_rect_Type0 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_inv_rect_Type4 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_inv_rect_Type3 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_inv_rect_Type2 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_inv_rect_Type1 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_inv_rect_Type0 :
  fixed -> partial_fn -> partial_fn -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val fn_contains_discr : fixed -> partial_fn -> partial_fn -> __

val fn_contains_jmdiscr : fixed -> partial_fn -> partial_fn -> __

val fill_in_statement :
  fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
  partial_fn Types.sig0

val add_to_graph :
  fixed -> Graphs.label -> RTLabs_syntax.statement -> partial_fn ->
  partial_fn Types.sig0

val change_entry :
  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0

val add_fresh_to_graph :
  fixed -> (Graphs.label -> RTLabs_syntax.statement) -> partial_fn ->
  partial_fn Types.sig0

val fresh_reg :
  fixed -> partial_fn -> AST.typ -> (partial_fn Types.sig0,
  Registers.register Types.sig0) Types.dPair

val choose_reg :
  fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
  Types.sig0, Registers.register Types.sig0) Types.dPair

val foldr_all : ('a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2

val foldr_all' :
  ('a1 -> __ -> 'a1 List.list -> 'a2 -> 'a2) -> 'a2 -> 'a1 List.list -> 'a2

val eject' : ('a1, 'a2) Types.dPair -> 'a1

val choose_regs :
  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list -> partial_fn
  -> (partial_fn Types.sig0, Registers.register List.list Types.sig0)
  Types.dPair

val add_stmt_inv_rect_Type4 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
  'a1) -> 'a1

val add_stmt_inv_rect_Type5 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
  'a1) -> 'a1

val add_stmt_inv_rect_Type3 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
  'a1) -> 'a1

val add_stmt_inv_rect_Type2 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
  'a1) -> 'a1

val add_stmt_inv_rect_Type1 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
  'a1) -> 'a1

val add_stmt_inv_rect_Type0 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ ->
  'a1) -> 'a1

val add_stmt_inv_inv_rect_Type4 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
  -> 'a1) -> 'a1

val add_stmt_inv_inv_rect_Type3 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
  -> 'a1) -> 'a1

val add_stmt_inv_inv_rect_Type2 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
  -> 'a1) -> 'a1

val add_stmt_inv_inv_rect_Type1 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
  -> 'a1) -> 'a1

val add_stmt_inv_inv_rect_Type0 :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> (__ -> __ -> __
  -> 'a1) -> 'a1

val add_stmt_inv_discr :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __

val add_stmt_inv_jmdiscr :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn -> __

type fn_con_because =
| Fn_con_eq of partial_fn
| Fn_con_sig of partial_fn * partial_fn * partial_fn Types.sig0
| Fn_con_addinv of partial_fn * partial_fn * Cminor_syntax.stmt
   * partial_fn Types.sig0

val fn_con_because_rect_Type4 :
  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
  fn_con_because -> 'a1

val fn_con_because_rect_Type5 :
  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
  fn_con_because -> 'a1

val fn_con_because_rect_Type3 :
  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
  fn_con_because -> 'a1

val fn_con_because_rect_Type2 :
  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
  fn_con_because -> 'a1

val fn_con_because_rect_Type1 :
  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
  fn_con_because -> 'a1

val fn_con_because_rect_Type0 :
  fixed -> (partial_fn -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  partial_fn Types.sig0 -> 'a1) -> (partial_fn -> partial_fn -> __ ->
  Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
  fn_con_because -> 'a1

val fn_con_because_inv_rect_Type4 :
  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
  Types.sig0 -> __ -> __ -> 'a1) -> 'a1

val fn_con_because_inv_rect_Type3 :
  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
  Types.sig0 -> __ -> __ -> 'a1) -> 'a1

val fn_con_because_inv_rect_Type2 :
  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
  Types.sig0 -> __ -> __ -> 'a1) -> 'a1

val fn_con_because_inv_rect_Type1 :
  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
  Types.sig0 -> __ -> __ -> 'a1) -> 'a1

val fn_con_because_inv_rect_Type0 :
  fixed -> partial_fn -> fn_con_because -> (partial_fn -> __ -> __ -> 'a1) ->
  (partial_fn -> partial_fn -> __ -> partial_fn Types.sig0 -> __ -> __ ->
  'a1) -> (partial_fn -> partial_fn -> __ -> Cminor_syntax.stmt -> partial_fn
  Types.sig0 -> __ -> __ -> 'a1) -> 'a1

val fn_con_because_discr :
  fixed -> partial_fn -> fn_con_because -> fn_con_because -> __

val fn_con_because_jmdiscr :
  fixed -> partial_fn -> fn_con_because -> fn_con_because -> __

val fn_con_because_left : fixed -> partial_fn -> fn_con_because -> partial_fn

val add_expr :
  fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> Registers.register
  Types.sig0 -> partial_fn Types.sig0

val add_exprs :
  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair List.list ->
  Registers.register List.list -> partial_fn -> partial_fn Types.sig0

val stmt_inv_rect_Type4 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_rect_Type5 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_rect_Type3 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_rect_Type2 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_rect_Type1 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_rect_Type0 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_inv_rect_Type4 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_inv_rect_Type3 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_inv_rect_Type2 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_inv_rect_Type1 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_inv_rect_Type0 :
  fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1

val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __

val stmt_inv_jmdiscr : fixed -> Cminor_syntax.stmt -> __

val expr_is_cst_ident :
  AST.typ -> Cminor_syntax.expr -> AST.ident Types.option

val option_jmdiscr : 'a1 Types.option -> 'a1 Types.option -> __

val dPair_jmdiscr : ('a1, 'a2) Types.dPair -> ('a1, 'a2) Types.dPair -> __

val add_return :
  fixed -> (AST.typ, Cminor_syntax.expr) Types.dPair Types.option ->
  partial_fn -> partial_fn Types.sig0

val record_goto_label :
  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn

val add_goto_dummy :
  fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0

val add_stmt :
  fixed -> Cminor_syntax.stmt -> partial_fn -> partial_fn Types.sig0

val patch_gotos : fixed -> partial_fn -> partial_fn Types.sig0

val c2ra_function :
  Cminor_syntax.internal_function -> RTLabs_syntax.internal_function

val cminor_to_rtlabs :
  Cminor_syntax.cminor_program -> RTLabs_syntax.rTLabs_program