open Preamble

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

open ErrorMessages

open Option

open Setoids

open Monad

open Positive

open PreIdentifiers

open Errors

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 Values

open FrontEndVal

open Hide

open ByteValues

open GenMem

open FrontEndMem

type constant =
| Ointconst of AST.intsize * AST.signedness * AST.bvint
| Oaddrsymbol of AST.ident * Nat.nat
| Oaddrstack of Nat.nat

val constant_rect_Type4 :
  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1

val constant_rect_Type5 :
  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1

val constant_rect_Type3 :
  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1

val constant_rect_Type2 :
  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1

val constant_rect_Type1 :
  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1

val constant_rect_Type0 :
  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1

val constant_inv_rect_Type4 :
  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
  -> __ -> 'a1) -> 'a1

val constant_inv_rect_Type3 :
  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
  -> __ -> 'a1) -> 'a1

val constant_inv_rect_Type2 :
  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
  -> __ -> 'a1) -> 'a1

val constant_inv_rect_Type1 :
  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
  -> __ -> 'a1) -> 'a1

val constant_inv_rect_Type0 :
  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
  -> __ -> 'a1) -> 'a1

val constant_discr : AST.typ -> constant -> constant -> __

val constant_jmdiscr : AST.typ -> constant -> constant -> __

type unary_operation =
| Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
| Onegint of AST.intsize * AST.signedness
| Onotbool of AST.typ * AST.intsize * AST.signedness
| Onotint of AST.intsize * AST.signedness
| Oid of AST.typ
| Optrofint of AST.intsize * AST.signedness
| Ointofptr of AST.intsize * AST.signedness

val unary_operation_rect_Type4 :
  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1

val unary_operation_rect_Type5 :
  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1

val unary_operation_rect_Type3 :
  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1

val unary_operation_rect_Type2 :
  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1

val unary_operation_rect_Type1 :
  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1

val unary_operation_rect_Type0 :
  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1

val unary_operation_inv_rect_Type4 :
  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type3 :
  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type2 :
  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type1 :
  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type0 :
  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1

val unary_operation_discr :
  AST.typ -> AST.typ -> unary_operation -> unary_operation -> __

val unary_operation_jmdiscr :
  AST.typ -> AST.typ -> unary_operation -> unary_operation -> __

type binary_operation =
| Oadd of AST.intsize * AST.signedness
| Osub of AST.intsize * AST.signedness
| Omul of AST.intsize * AST.signedness
| Odiv of AST.intsize
| Odivu of AST.intsize
| Omod of AST.intsize
| Omodu of AST.intsize
| Oand of AST.intsize * AST.signedness
| Oor of AST.intsize * AST.signedness
| Oxor of AST.intsize * AST.signedness
| Oshl of AST.intsize * AST.signedness
| Oshr of AST.intsize * AST.signedness
| Oshru of AST.intsize * AST.signedness
| Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
| Ocmpu of AST.intsize * AST.signedness * Integers.comparison
| Oaddpi of AST.intsize
| Oaddip of AST.intsize
| Osubpi of AST.intsize
| Osubpp of AST.intsize
| Ocmpp of AST.signedness * Integers.comparison

val binary_operation_rect_Type4 :
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
  AST.typ -> binary_operation -> 'a1

val binary_operation_rect_Type5 :
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
  AST.typ -> binary_operation -> 'a1

val binary_operation_rect_Type3 :
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
  AST.typ -> binary_operation -> 'a1

val binary_operation_rect_Type2 :
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
  AST.typ -> binary_operation -> 'a1

val binary_operation_rect_Type1 :
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
  AST.typ -> binary_operation -> 'a1

val binary_operation_rect_Type0 :
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
  AST.typ -> binary_operation -> 'a1

val binary_operation_inv_rect_Type4 :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type3 :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type2 :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type1 :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type0 :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
  -> __ -> __ -> 'a1) -> 'a1

val binary_operation_discr :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __

val binary_operation_jmdiscr :
  AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __

val eval_constant :
  AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block ->
  constant -> Values.val0 Types.option

val eval_unop :
  AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
  Types.option

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

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

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

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

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

val ev_subpp :
  AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option

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

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

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

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

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

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

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

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

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

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

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

val fEtrue : Values.val0

val fEfalse : Values.val0

val fE_of_bool : Bool.bool -> Values.val0

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

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

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

val ev_cmpp :
  GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
  Values.val0 Types.option

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

val eval_binop :
  GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
  Values.val0 -> Values.val0 -> Values.val0 Types.option