19 open Hints_declaration
83 | Vint of AST.intsize * AST.bvint
85 | Vptr of Pointers.pointer
88 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
92 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
96 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
100 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
104 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
108 'a1 -> (AST.intsize -> AST.bvint -> 'a1) -> 'a1 -> (Pointers.pointer ->
111 val val_inv_rect_Type4 :
112 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
113 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
115 val val_inv_rect_Type3 :
116 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
117 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
119 val val_inv_rect_Type2 :
120 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
121 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
123 val val_inv_rect_Type1 :
124 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
125 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
127 val val_inv_rect_Type0 :
128 val0 -> (__ -> 'a1) -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (__ ->
129 'a1) -> (Pointers.pointer -> __ -> 'a1) -> 'a1
131 val val_discr : val0 -> val0 -> __
133 val val_jmdiscr : val0 -> val0 -> __
135 val vzero : AST.intsize -> val0
137 val vone : AST.intsize -> val0
139 val mone : AST.intsize -> BitVector.bitVector
141 val vmone : AST.intsize -> val0
147 val of_bool : Bool.bool -> val0
149 val eval_bool_of_val : val0 -> Bool.bool Errors.res
151 val neg : val0 -> val0
153 val notint : val0 -> val0
155 val notbool : val0 -> val0
157 val zero_ext : AST.intsize -> val0 -> val0
159 val sign_ext : AST.intsize -> val0 -> val0
161 val add : val0 -> val0 -> val0
163 val sub : val0 -> val0 -> val0
165 val mul : val0 -> val0 -> val0
167 val v_and : val0 -> val0 -> val0
169 val or0 : val0 -> val0 -> val0
171 val xor : val0 -> val0 -> val0
173 val cmp_match : Integers.comparison -> val0
175 val cmp_mismatch : Integers.comparison -> val0
178 Integers.comparison -> Pointers.offset -> Pointers.offset -> Bool.bool
181 Nat.nat -> Integers.comparison -> BitVector.bitVector ->
182 BitVector.bitVector -> Bool.bool
185 Nat.nat -> Integers.comparison -> BitVector.bitVector ->
186 BitVector.bitVector -> Bool.bool
188 val cmp : Integers.comparison -> val0 -> val0 -> val0
190 val cmpu : Integers.comparison -> val0 -> val0 -> val0
192 val load_result : AST.typ -> val0 -> val0