open Preamble

open Div_and_mod

open Jmeq

open Russell

open Util

open Bool

open Relations

open Nat

open List

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open Coqlib

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

open Proper

open PositiveMap

open Deqsets

open Extralib

open Lists

open Identifiers

open Integers

open AST

open Division

open Exp

open Arithmetic

open Extranat

open Vector

open FoldStuff

open BitVector

open Z

open BitVectorZ

open Pointers

type val0 =
| Vundef
| Vint of AST.intsize * AST.bvint
| Vnull
| Vptr of Pointers.pointer

val val_rect_Type4 :
  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  'a1) -> val0 -> 'a1

val val_rect_Type5 :
  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  'a1) -> val0 -> 'a1

val val_rect_Type3 :
  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  'a1) -> val0 -> 'a1

val val_rect_Type2 :
  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  'a1) -> val0 -> 'a1

val val_rect_Type1 :
  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  'a1) -> val0 -> 'a1

val val_rect_Type0 :
  'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
  'a1) -> val0 -> 'a1

val val_inv_rect_Type4 :
  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1

val val_inv_rect_Type3 :
  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1

val val_inv_rect_Type2 :
  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1

val val_inv_rect_Type1 :
  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1

val val_inv_rect_Type0 :
  val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
  'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1

val val_discr : val0 -> val0 -> __

val val_jmdiscr : val0 -> val0 -> __

val vzero : AST.intsize -> val0

val vone : AST.intsize -> val0

val mone : AST.intsize -> BitVector.bitVector

val vmone : AST.intsize -> val0

val vtrue : val0

val vfalse : val0

val of_bool : Bool.bool -> val0

val eval_bool_of_val : val0 -> Bool.bool Errors.res

val neg : val0 -> val0

val notint : val0 -> val0

val notbool : val0 -> val0

val zero_ext : AST.intsize -> val0 -> val0

val sign_ext : AST.intsize -> val0 -> val0

val add : val0 -> val0 -> val0

val sub : val0 -> val0 -> val0

val mul : val0 -> val0 -> val0

val v_and : val0 -> val0 -> val0

val or0 : val0 -> val0 -> val0

val xor : val0 -> val0 -> val0

val cmp_match : Integers.comparison -> val0

val cmp_mismatch : Integers.comparison -> val0

val cmp_offset :
  Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool

val cmp_int :
  Nat.nat -> Integers.comparison -> BitVector.bitVector ->
  BitVector.bitVector -> Bool.bool

val cmpu_int :
  Nat.nat -> Integers.comparison -> BitVector.bitVector ->
  BitVector.bitVector -> Bool.bool

val cmp : Integers.comparison -> val0 -> val0 -> val0

val cmpu : Integers.comparison -> val0 -> val0 -> val0

val load_result : AST.typ -> val0 -> val0