69 open Hints_declaration
94 | Ointconst of AST.intsize * AST.signedness * AST.bvint
95 | Oaddrsymbol of AST.ident * Nat.nat
96 | Oaddrstack of Nat.nat
98 val constant_rect_Type4 :
99 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
100 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
102 val constant_rect_Type5 :
103 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
104 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
106 val constant_rect_Type3 :
107 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
108 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
110 val constant_rect_Type2 :
111 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
112 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
114 val constant_rect_Type1 :
115 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
116 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
118 val constant_rect_Type0 :
119 (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
120 Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
122 val constant_inv_rect_Type4 :
123 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
124 __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
127 val constant_inv_rect_Type3 :
128 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
129 __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
132 val constant_inv_rect_Type2 :
133 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
134 __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
137 val constant_inv_rect_Type1 :
138 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
139 __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
142 val constant_inv_rect_Type0 :
143 AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
144 __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
147 val constant_discr : AST.typ -> constant -> constant -> __
149 val constant_jmdiscr : AST.typ -> constant -> constant -> __
151 type unary_operation =
152 | Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
153 | Onegint of AST.intsize * AST.signedness
154 | Onotbool of AST.typ * AST.intsize * AST.signedness
155 | Onotint of AST.intsize * AST.signedness
157 | Optrofint of AST.intsize * AST.signedness
158 | Ointofptr of AST.intsize * AST.signedness
160 val unary_operation_rect_Type4 :
161 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
162 (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
163 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
164 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
165 -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
167 val unary_operation_rect_Type5 :
168 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
169 (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
170 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
171 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
172 -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
174 val unary_operation_rect_Type3 :
175 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
176 (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
177 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
178 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
179 -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
181 val unary_operation_rect_Type2 :
182 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
183 (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
184 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
185 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
186 -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
188 val unary_operation_rect_Type1 :
189 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
190 (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
191 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
192 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
193 -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
195 val unary_operation_rect_Type0 :
196 (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
197 (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
198 AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
199 (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
200 -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
202 val unary_operation_inv_rect_Type4 :
203 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
204 AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
205 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
206 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
207 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
208 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
209 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
211 val unary_operation_inv_rect_Type3 :
212 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
213 AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
214 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
215 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
216 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
217 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
218 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
220 val unary_operation_inv_rect_Type2 :
221 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
222 AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
223 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
224 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
225 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
226 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
227 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
229 val unary_operation_inv_rect_Type1 :
230 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
231 AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
232 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
233 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
234 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
235 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
236 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
238 val unary_operation_inv_rect_Type0 :
239 AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
240 AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
241 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
242 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
243 AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
244 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
245 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
247 val unary_operation_discr :
248 AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
250 val unary_operation_jmdiscr :
251 AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
253 type binary_operation =
254 | Oadd of AST.intsize * AST.signedness
255 | Osub of AST.intsize * AST.signedness
256 | Omul of AST.intsize * AST.signedness
257 | Odiv of AST.intsize
258 | Odivu of AST.intsize
259 | Omod of AST.intsize
260 | Omodu of AST.intsize
261 | Oand of AST.intsize * AST.signedness
262 | Oor of AST.intsize * AST.signedness
263 | Oxor of AST.intsize * AST.signedness
264 | Oshl of AST.intsize * AST.signedness
265 | Oshr of AST.intsize * AST.signedness
266 | Oshru of AST.intsize * AST.signedness
267 | Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
268 | Ocmpu of AST.intsize * AST.signedness * Integers.comparison
269 | Oaddpi of AST.intsize
270 | Oaddip of AST.intsize
271 | Osubpi of AST.intsize
272 | Osubpp of AST.intsize
273 | Ocmpp of AST.signedness * Integers.comparison
275 val binary_operation_rect_Type4 :
276 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
277 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
278 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
279 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
280 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
281 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
282 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
283 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
284 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
285 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
286 (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
287 AST.typ -> binary_operation -> 'a1
289 val binary_operation_rect_Type5 :
290 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
291 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
292 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
293 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
294 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
295 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
296 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
297 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
298 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
299 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
300 (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
301 AST.typ -> binary_operation -> 'a1
303 val binary_operation_rect_Type3 :
304 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
305 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
306 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
307 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
308 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
309 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
310 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
311 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
312 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
313 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
314 (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
315 AST.typ -> binary_operation -> 'a1
317 val binary_operation_rect_Type2 :
318 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
319 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
320 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
321 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
322 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
323 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
324 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
325 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
326 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
327 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
328 (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
329 AST.typ -> binary_operation -> 'a1
331 val binary_operation_rect_Type1 :
332 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
333 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
334 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
335 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
336 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
337 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
338 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
339 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
340 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
341 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
342 (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
343 AST.typ -> binary_operation -> 'a1
345 val binary_operation_rect_Type0 :
346 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
347 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
348 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
349 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
350 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
351 AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
352 (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
353 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
354 AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
355 (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
356 (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
357 AST.typ -> binary_operation -> 'a1
359 val binary_operation_inv_rect_Type4 :
360 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
361 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
362 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
363 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
364 -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
365 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
366 __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
367 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
368 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
369 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
370 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
371 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
372 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
373 __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
374 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
375 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
376 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
377 -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
378 -> __ -> __ -> 'a1) -> 'a1
380 val binary_operation_inv_rect_Type3 :
381 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
382 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
383 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
384 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
385 -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
386 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
387 __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
388 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
389 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
390 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
391 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
392 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
393 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
394 __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
395 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
396 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
397 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
398 -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
399 -> __ -> __ -> 'a1) -> 'a1
401 val binary_operation_inv_rect_Type2 :
402 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
403 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
404 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
405 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
406 -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
407 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
408 __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
409 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
410 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
411 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
412 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
413 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
414 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
415 __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
416 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
417 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
418 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
419 -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
420 -> __ -> __ -> 'a1) -> 'a1
422 val binary_operation_inv_rect_Type1 :
423 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
424 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
425 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
426 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
427 -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
428 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
429 __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
430 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
431 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
432 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
433 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
434 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
435 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
436 __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
437 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
438 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
439 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
440 -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
441 -> __ -> __ -> 'a1) -> 'a1
443 val binary_operation_inv_rect_Type0 :
444 AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
445 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
446 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
447 AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
448 -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
449 (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
450 __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
451 -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
452 -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
453 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
454 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
455 (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
456 (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
457 __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
458 Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
459 -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
460 -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
461 -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
462 -> __ -> __ -> 'a1) -> 'a1
464 val binary_operation_discr :
465 AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
467 val binary_operation_jmdiscr :
468 AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
471 AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block ->
472 constant -> Values.val0 Types.option
475 AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
478 val eval_compare_mismatch : Integers.comparison -> Values.val0 Types.option
480 val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option
482 val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option
484 val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
486 val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
489 AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option
491 val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option
493 val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option
495 val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option
497 val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option
499 val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option
501 val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
503 val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
505 val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
507 val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
509 val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option
511 val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option
513 val fEtrue : Values.val0
515 val fEfalse : Values.val0
517 val fE_of_bool : Bool.bool -> Values.val0
519 val ev_cmp_match : Integers.comparison -> Values.val0 Types.option
521 val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
524 Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
528 GenMem.mem -> Integers.comparison -> Values.val0 -> Values.val0 ->
529 Values.val0 Types.option
532 Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
536 GenMem.mem -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
537 Values.val0 -> Values.val0 -> Values.val0 Types.option