open Preamble

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 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 Globalenvs

open CostLabel

open Csyntax

open Events

open Smallstep

open TypeComparison

open ClassifyOp

val sem_neg : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option

val sem_notint : Values.val0 -> Values.val0 Types.option

val sem_notbool : Values.val0 -> Csyntax.type0 -> Values.val0 Types.option

val sem_add :
  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
  Types.option

val sem_sub :
  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
  Csyntax.type0 -> Values.val0 Types.option

val sem_mul :
  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
  Types.option

val sem_div :
  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
  Types.option

val sem_mod :
  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
  Types.option

val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option

val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option

val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option

val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option

val sem_shr :
  Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 -> Values.val0
  Types.option

val sem_cmp_mismatch : Integers.comparison -> Values.val0 Types.option

val sem_cmp_match : Integers.comparison -> Values.val0 Types.option

val sem_cmp :
  Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
  Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option

val cast_bool_to_target :
  Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option

val sem_unary_operation :
  Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
  Types.option

val sem_binary_operation :
  Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
  Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0 Types.option

val cast_int_int :
  AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
  BitVector.bitVector

type genv = Csyntax.clight_fundef Globalenvs.genv_t

type env = Pointers.block Identifiers.identifier_map

val empty_env : env

val load_value_of_type :
  Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
  Values.val0 Types.option

val store_value_of_type :
  Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
  Values.val0 -> GenMem.mem Types.option

val blocks_of_env : env -> Pointers.block List.list

val select_switch :
  AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
  Csyntax.labeled_statements Types.option

val seq_of_labeled_statement :
  Csyntax.labeled_statements -> Csyntax.statement

type cont =
| Kstop
| Kseq of Csyntax.statement * cont
| Kwhile of Csyntax.expr * Csyntax.statement * cont
| Kdowhile of Csyntax.expr * Csyntax.statement * cont
| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
| Kswitch of cont
| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
           Types.prod Types.option * Csyntax.function0 * env * cont

val cont_rect_Type4 :
  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1

val cont_rect_Type3 :
  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1

val cont_rect_Type2 :
  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1

val cont_rect_Type1 :
  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1

val cont_rect_Type0 :
  'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
  Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
  (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
  'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
  Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0 ->
  env -> cont -> 'a1 -> 'a1) -> cont -> 'a1

val cont_inv_rect_Type4 :
  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type3 :
  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type2 :
  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type1 :
  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_inv_rect_Type0 :
  cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
  'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont ->
  (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement ->
  Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__ ->
  'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
  Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env -> cont
  -> (__ -> 'a1) -> __ -> 'a1) -> 'a1

val cont_discr : cont -> cont -> __

val cont_jmdiscr : cont -> cont -> __

val call_cont : cont -> cont

type state =
| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
   * cont * GenMem.mem
| Returnstate of Values.val0 * cont * GenMem.mem
| Finalstate of Integers.int

val state_rect_Type4 :
  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
  (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type5 :
  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
  (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type3 :
  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
  (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type2 :
  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
  (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type1 :
  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
  (Integers.int -> 'a1) -> state -> 'a1

val state_rect_Type0 :
  (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
  'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
  cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1) ->
  (Integers.int -> 'a1) -> state -> 'a1

val state_inv_rect_Type4 :
  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type3 :
  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type2 :
  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type1 :
  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1

val state_inv_rect_Type0 :
  state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
  GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
  Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
  -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1

val state_discr : state -> state -> __

val state_jmdiscr : state -> state -> __

val find_label_ls :
  Csyntax.label -> Csyntax.labeled_statements -> cont -> (Csyntax.statement,
  cont) Types.prod Types.option

val find_label :
  Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
  Types.prod Types.option

val fun_typeof : Csyntax.expr -> Csyntax.type0