open Preamble

open ErrorMessages

open Option

open Setoids

open Monad

open Jmeq

open Russell

open Positive

open PreIdentifiers

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Errors

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 Coqlib

open Values

open FrontEndVal

open Hide

open ByteValues

open Division

open Z

open BitVectorZ

open Pointers

open GenMem

open FrontEndMem

type 'f genv_t = { functions : 'f PositiveMap.positive_map;
                   nextfunction : Positive.pos;
                   symbols : Pointers.block Identifiers.identifier_map }

val genv_t_rect_Type4 :
  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2

val genv_t_rect_Type5 :
  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2

val genv_t_rect_Type3 :
  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2

val genv_t_rect_Type2 :
  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2

val genv_t_rect_Type1 :
  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2

val genv_t_rect_Type0 :
  ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
  Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2

val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map

val nextfunction : 'a1 genv_t -> Positive.pos

val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map

val genv_t_inv_rect_Type4 :
  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2

val genv_t_inv_rect_Type3 :
  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2

val genv_t_inv_rect_Type2 :
  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2

val genv_t_inv_rect_Type1 :
  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2

val genv_t_inv_rect_Type0 :
  'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
  Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2

val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __

val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __

val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t

val add_funct : (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t

val add_symbol : AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t

val empty_mem : GenMem.mem

val empty : 'a1 genv_t

val add_functs :
  'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t

val find_symbol : 'a1 genv_t -> AST.ident -> Pointers.block Types.option

val store_init_data :
  'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
  GenMem.mem Types.option

val size_init_data : AST.init_data -> Nat.nat

val store_init_data_list :
  'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data
  List.list -> GenMem.mem Types.option

val size_init_data_list : AST.init_data List.list -> Nat.nat

val add_globals :
  ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem) Types.prod ->
  ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
  genv_t, GenMem.mem) Types.prod

val init_globals :
  ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem ->
  ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
  GenMem.mem Errors.res

val globalenv_allocmem :
  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1 genv_t,
  GenMem.mem) Types.prod

val globalenv :
  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t

val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t

val init_mem :
  ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
  Errors.res

val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem

val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option

val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option

val symbol_for_block : 'a1 genv_t -> Pointers.block -> AST.ident Types.option

val symbol_of_function_block : 'a1 genv_t -> Pointers.block -> AST.ident

val symbol_of_function_block' :
  'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident

val find_funct_ptr_id :
  'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option

val opt_eq_from_res__o__ffpi_drop__o__inject :
  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
  Types.sig0

val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
  'a2) Types.dPair -> __ Types.sig0

val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
  Types.sig0 -> __ Types.sig0

val jmeq_to_eq__o__ffpi_drop__o__inject :
  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0

val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
  Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
  Types.sig0

val dpi1__o__ffpi_drop__o__inject :
  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
  -> __ Types.sig0

val eject__o__ffpi_drop__o__inject :
  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
  Types.sig0

val ffpi_drop__o__inject :
  Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0

val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident

val symbol_of_function_val' : 'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident

val find_funct_id :
  'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option

val opt_eq_from_res__o__ffi_drop__o__inject :
  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
  Types.sig0

val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2)
  Types.dPair -> __ Types.sig0

val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
  Types.sig0 -> __ Types.sig0

val jmeq_to_eq__o__ffi_drop__o__inject :
  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0

val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
  Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
  Types.sig0

val dpi1__o__ffi_drop__o__inject :
  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
  __ Types.sig0

val eject__o__ffi_drop__o__inject :
  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
  Types.sig0

val ffi_drop__o__inject :
  Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0

val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos

val alloc_pair :
  GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
  GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1

val prod_jmdiscr : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __

val related_globals_rect_Type4 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
  -> 'a3

val related_globals_rect_Type5 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
  -> 'a3

val related_globals_rect_Type3 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
  -> 'a3

val related_globals_rect_Type2 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
  -> 'a3

val related_globals_rect_Type1 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
  -> 'a3

val related_globals_rect_Type0 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
  -> 'a3

val related_globals_inv_rect_Type4 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
  'a3) -> 'a3

val related_globals_inv_rect_Type3 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
  'a3) -> 'a3

val related_globals_inv_rect_Type2 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
  'a3) -> 'a3

val related_globals_inv_rect_Type1 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
  'a3) -> 'a3

val related_globals_inv_rect_Type0 :
  ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __ ->
  'a3) -> 'a3

val related_globals_discr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __

val related_globals_jmdiscr : ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __

val related_globals_gen_rect_Type4 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_rect_Type5 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_rect_Type3 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_rect_Type2 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_rect_Type1 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_rect_Type0 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_inv_rect_Type4 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_inv_rect_Type3 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_inv_rect_Type2 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_inv_rect_Type1 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_inv_rect_Type0 :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
  -> __ -> __ -> __ -> 'a3) -> 'a3

val related_globals_gen_discr :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __

val related_globals_gen_jmdiscr :
  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __

open Extra_bool