open Preamble

open Deqsets

open Sets

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Listb

open Proper

open PositiveMap

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Setoids

open Monad

open Option

open Div_and_mod

open Jmeq

open Russell

open Util

open Lists

open Positive

open Identifiers

open CostLabel

open Coqlib

open Exp

open Arithmetic

open Vector

open FoldStuff

open BitVector

open Extranat

open Integers

open AST

open Csyntax

open Fresh

open CexecInd

open SmallstepExec

open Cexec

open IO

open IOMonad

open Star

open ClassifyOp

open Events

open Smallstep

open Extra_bool

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

open Globalenvs

open Csem

open TypeComparison

open Frontend_misc

open MemProperties

open MemoryInjections

val convert_break_to_goto :
  Csyntax.statement -> Csyntax.label -> Csyntax.statement

val produce_cond :
  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
  Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
  Identifiers.universe) Types.prod

val simplify_switch :
  Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
  (Csyntax.statement, Identifiers.universe) Types.prod

val switch_removal_branches :
  Csyntax.labeled_statements -> Identifiers.universe ->
  ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
  List.list) Types.prod, Identifiers.universe) Types.prod

val switch_removal :
  Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
  (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
  Identifiers.universe) Types.prod

val ret_st :
  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
  Identifiers.universe) Types.prod -> 'a1

val ret_vars :
  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
  Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
  List.list

val ret_u :
  (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
  Identifiers.universe) Types.prod -> Identifiers.universe

val least_identifier : PreIdentifiers.identifier

val max_of_expr : Csyntax.expr -> AST.ident

val max_of_ls : Csyntax.labeled_statements -> AST.ident

val max_of_statement : Csyntax.statement -> AST.ident

val max_id_of_function : Csyntax.function0 -> AST.ident

val function_switch_removal :
  Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
  Types.prod List.list) Types.prod

val fundef_switch_removal : Csyntax.clight_fundef -> Csyntax.clight_fundef

val program_switch_removal : Csyntax.clight_program -> Csyntax.clight_program

val nonempty_block_rect_Type4 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1

val nonempty_block_rect_Type5 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1

val nonempty_block_rect_Type3 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1

val nonempty_block_rect_Type2 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1

val nonempty_block_rect_Type1 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1

val nonempty_block_rect_Type0 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1

val nonempty_block_inv_rect_Type4 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1

val nonempty_block_inv_rect_Type3 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1

val nonempty_block_inv_rect_Type2 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1

val nonempty_block_inv_rect_Type1 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1

val nonempty_block_inv_rect_Type0 :
  GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1

val nonempty_block_discr : GenMem.mem -> Pointers.block -> __

val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __

val sr_memext_rect_Type4 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  'a1) -> 'a1

val sr_memext_rect_Type5 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  'a1) -> 'a1

val sr_memext_rect_Type3 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  'a1) -> 'a1

val sr_memext_rect_Type2 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  'a1) -> 'a1

val sr_memext_rect_Type1 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  'a1) -> 'a1

val sr_memext_rect_Type0 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  'a1) -> 'a1

val sr_memext_inv_rect_Type4 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val sr_memext_inv_rect_Type3 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val sr_memext_inv_rect_Type2 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val sr_memext_inv_rect_Type1 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val sr_memext_inv_rect_Type0 :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __ ->
  __ -> 'a1) -> 'a1

val sr_memext_discr :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __

val sr_memext_jmdiscr :
  GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __

val env_codomain :
  Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
  Pointers.block Frontend_misc.lset