source: extracted/frontEndOps.mli @ 2716

Last change on this file since 2716 was 2649, checked in by sacerdot, 7 years ago

...

File size: 23.4 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open Extralib
10
11open Lists
12
13open Identifiers
14
15open Integers
16
17open AST
18
19open Division
20
21open Arithmetic
22
23open Extranat
24
25open Vector
26
27open FoldStuff
28
29open BitVector
30
31open Z
32
33open BitVectorZ
34
35open Pointers
36
37open ErrorMessages
38
39open Option
40
41open Setoids
42
43open Monad
44
45open Positive
46
47open PreIdentifiers
48
49open Errors
50
51open Div_and_mod
52
53open Jmeq
54
55open Russell
56
57open Util
58
59open Bool
60
61open Relations
62
63open Nat
64
65open List
66
67open Hints_declaration
68
69open Core_notation
70
71open Pts
72
73open Logic
74
75open Types
76
77open Coqlib
78
79open Values
80
81open FrontEndVal
82
83open Hide
84
85open ByteValues
86
87open GenMem
88
89open FrontEndMem
90
91type constant =
92| Ointconst of AST.intsize * AST.signedness * AST.bvint
93| Oaddrsymbol of AST.ident * Nat.nat
94| Oaddrstack of Nat.nat
95
96val constant_rect_Type4 :
97  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
98  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
99
100val constant_rect_Type5 :
101  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
102  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
103
104val constant_rect_Type3 :
105  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
106  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
107
108val constant_rect_Type2 :
109  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
110  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
111
112val constant_rect_Type1 :
113  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
114  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
115
116val constant_rect_Type0 :
117  (AST.intsize -> AST.signedness -> AST.bvint -> 'a1) -> (AST.ident ->
118  Nat.nat -> 'a1) -> (Nat.nat -> 'a1) -> AST.typ -> constant -> 'a1
119
120val constant_inv_rect_Type4 :
121  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
122  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
123  -> __ -> 'a1) -> 'a1
124
125val constant_inv_rect_Type3 :
126  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
127  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
128  -> __ -> 'a1) -> 'a1
129
130val constant_inv_rect_Type2 :
131  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
132  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
133  -> __ -> 'a1) -> 'a1
134
135val constant_inv_rect_Type1 :
136  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
137  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
138  -> __ -> 'a1) -> 'a1
139
140val constant_inv_rect_Type0 :
141  AST.typ -> constant -> (AST.intsize -> AST.signedness -> AST.bvint -> __ ->
142  __ -> 'a1) -> (AST.ident -> Nat.nat -> __ -> __ -> 'a1) -> (Nat.nat -> __
143  -> __ -> 'a1) -> 'a1
144
145val constant_discr : AST.typ -> constant -> constant -> __
146
147val constant_jmdiscr : AST.typ -> constant -> constant -> __
148
149type unary_operation =
150| Ocastint of AST.intsize * AST.signedness * AST.intsize * AST.signedness
151| Onegint of AST.intsize * AST.signedness
152| Onotbool of AST.typ * AST.intsize * AST.signedness
153| Onotint of AST.intsize * AST.signedness
154| Oid of AST.typ
155| Optrofint of AST.intsize * AST.signedness
156| Ointofptr of AST.intsize * AST.signedness
157
158val unary_operation_rect_Type4 :
159  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
160  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
161  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
162  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
163  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
164
165val unary_operation_rect_Type5 :
166  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
167  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
168  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
169  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
170  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
171
172val unary_operation_rect_Type3 :
173  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
174  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
175  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
176  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
177  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
178
179val unary_operation_rect_Type2 :
180  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
181  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
182  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
183  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
184  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
185
186val unary_operation_rect_Type1 :
187  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
188  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
189  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
190  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
191  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
192
193val unary_operation_rect_Type0 :
194  (AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness -> 'a1) ->
195  (AST.intsize -> AST.signedness -> 'a1) -> (AST.typ -> AST.intsize ->
196  AST.signedness -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
197  (AST.typ -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize
198  -> AST.signedness -> 'a1) -> AST.typ -> AST.typ -> unary_operation -> 'a1
199
200val unary_operation_inv_rect_Type4 :
201  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
202  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
203  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
204  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
205  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
206  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
207  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
208
209val unary_operation_inv_rect_Type3 :
210  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
211  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
212  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
213  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
214  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
215  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
216  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
217
218val unary_operation_inv_rect_Type2 :
219  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
220  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
221  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
222  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
223  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
224  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
225  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
226
227val unary_operation_inv_rect_Type1 :
228  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
229  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
230  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
231  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
232  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
233  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
234  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
235
236val unary_operation_inv_rect_Type0 :
237  AST.typ -> AST.typ -> unary_operation -> (AST.intsize -> AST.signedness ->
238  AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
239  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> AST.intsize ->
240  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
241  AST.signedness -> __ -> __ -> __ -> 'a1) -> (AST.typ -> __ -> __ -> __ ->
242  'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) ->
243  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> 'a1) -> 'a1
244
245val unary_operation_discr :
246  AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
247
248val unary_operation_jmdiscr :
249  AST.typ -> AST.typ -> unary_operation -> unary_operation -> __
250
251type binary_operation =
252| Oadd of AST.intsize * AST.signedness
253| Osub of AST.intsize * AST.signedness
254| Omul of AST.intsize * AST.signedness
255| Odiv of AST.intsize
256| Odivu of AST.intsize
257| Omod of AST.intsize
258| Omodu of AST.intsize
259| Oand of AST.intsize * AST.signedness
260| Oor of AST.intsize * AST.signedness
261| Oxor of AST.intsize * AST.signedness
262| Oshl of AST.intsize * AST.signedness
263| Oshr of AST.intsize * AST.signedness
264| Oshru of AST.intsize * AST.signedness
265| Ocmp of AST.intsize * AST.signedness * AST.signedness * Integers.comparison
266| Ocmpu of AST.intsize * AST.signedness * Integers.comparison
267| Oaddpi of AST.intsize
268| Oaddip of AST.intsize
269| Osubpi of AST.intsize
270| Osubpp of AST.intsize
271| Ocmpp of AST.signedness * Integers.comparison
272
273val binary_operation_rect_Type4 :
274  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
275  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
276  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
277  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
278  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
279  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
280  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
281  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
282  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
283  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
284  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
285  AST.typ -> binary_operation -> 'a1
286
287val binary_operation_rect_Type5 :
288  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
289  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
290  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
291  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
292  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
293  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
294  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
295  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
296  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
297  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
298  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
299  AST.typ -> binary_operation -> 'a1
300
301val binary_operation_rect_Type3 :
302  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
303  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
304  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
305  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
306  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
307  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
308  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
309  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
310  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
311  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
312  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
313  AST.typ -> binary_operation -> 'a1
314
315val binary_operation_rect_Type2 :
316  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
317  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
318  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
319  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
320  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
321  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
322  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
323  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
324  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
325  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
326  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
327  AST.typ -> binary_operation -> 'a1
328
329val binary_operation_rect_Type1 :
330  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
331  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
332  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
333  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
334  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
335  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
336  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
337  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
338  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
339  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
340  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
341  AST.typ -> binary_operation -> 'a1
342
343val binary_operation_rect_Type0 :
344  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
345  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> 'a1) ->
346  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
347  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
348  'a1) -> (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize ->
349  AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness -> 'a1) ->
350  (AST.intsize -> AST.signedness -> 'a1) -> (AST.intsize -> AST.signedness ->
351  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize ->
352  AST.signedness -> Integers.comparison -> 'a1) -> (AST.intsize -> 'a1) ->
353  (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) -> (AST.intsize -> 'a1) ->
354  (AST.signedness -> Integers.comparison -> 'a1) -> AST.typ -> AST.typ ->
355  AST.typ -> binary_operation -> 'a1
356
357val binary_operation_inv_rect_Type4 :
358  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
359  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
360  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
361  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
362  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
363  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
364  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
365  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
366  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
367  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
368  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
369  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
370  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
371  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
372  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
373  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
374  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
375  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
376  -> __ -> __ -> 'a1) -> 'a1
377
378val binary_operation_inv_rect_Type3 :
379  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
380  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
381  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
382  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
383  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
384  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
385  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
386  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
387  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
388  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
389  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
390  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
391  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
392  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
393  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
394  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
395  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
396  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
397  -> __ -> __ -> 'a1) -> 'a1
398
399val binary_operation_inv_rect_Type2 :
400  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
401  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
402  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
403  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
404  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
405  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
406  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
407  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
408  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
409  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
410  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
411  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
412  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
413  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
414  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
415  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
416  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
417  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
418  -> __ -> __ -> 'a1) -> 'a1
419
420val binary_operation_inv_rect_Type1 :
421  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
422  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
423  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
424  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
425  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
426  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
427  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
428  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
429  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
430  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
431  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
432  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
433  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
434  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
435  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
436  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
437  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
438  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
439  -> __ -> __ -> 'a1) -> 'a1
440
441val binary_operation_inv_rect_Type0 :
442  AST.typ -> AST.typ -> AST.typ -> binary_operation -> (AST.intsize ->
443  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
444  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize ->
445  AST.signedness -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
446  -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) ->
447  (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ ->
448  __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __
449  -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1)
450  -> (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
451  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
452  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
453  (AST.intsize -> AST.signedness -> __ -> __ -> __ -> __ -> 'a1) ->
454  (AST.intsize -> AST.signedness -> AST.signedness -> Integers.comparison ->
455  __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> AST.signedness ->
456  Integers.comparison -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __
457  -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1)
458  -> (AST.intsize -> __ -> __ -> __ -> __ -> 'a1) -> (AST.intsize -> __ -> __
459  -> __ -> __ -> 'a1) -> (AST.signedness -> Integers.comparison -> __ -> __
460  -> __ -> __ -> 'a1) -> 'a1
461
462val binary_operation_discr :
463  AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
464
465val binary_operation_jmdiscr :
466  AST.typ -> AST.typ -> AST.typ -> binary_operation -> binary_operation -> __
467
468val eval_constant :
469  AST.typ -> (AST.ident -> Pointers.block Types.option) -> Pointers.block ->
470  constant -> Values.val0 Types.option
471
472val eval_unop :
473  AST.typ -> AST.typ -> unary_operation -> Values.val0 -> Values.val0
474  Types.option
475
476val eval_compare_mismatch : Integers.comparison -> Values.val0 Types.option
477
478val ev_add : Values.val0 -> Values.val0 -> Values.val0 Types.option
479
480val ev_sub : Values.val0 -> Values.val0 -> Values.val0 Types.option
481
482val ev_addpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
483
484val ev_subpi : Values.val0 -> Values.val0 -> Values.val0 Types.option
485
486val ev_subpp :
487  AST.intsize -> Values.val0 -> Values.val0 -> Values.val0 Types.option
488
489val ev_mul : Values.val0 -> Values.val0 -> Values.val0 Types.option
490
491val ev_divs : Values.val0 -> Values.val0 -> Values.val0 Types.option
492
493val ev_mods : Values.val0 -> Values.val0 -> Values.val0 Types.option
494
495val ev_divu : Values.val0 -> Values.val0 -> Values.val0 Types.option
496
497val ev_modu : Values.val0 -> Values.val0 -> Values.val0 Types.option
498
499val ev_and : Values.val0 -> Values.val0 -> Values.val0 Types.option
500
501val ev_or : Values.val0 -> Values.val0 -> Values.val0 Types.option
502
503val ev_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option
504
505val ev_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option
506
507val ev_shr : Values.val0 -> Values.val0 -> Values.val0 Types.option
508
509val ev_shru : Values.val0 -> Values.val0 -> Values.val0 Types.option
510
511val fEtrue : Values.val0
512
513val fEfalse : Values.val0
514
515val fE_of_bool : Bool.bool -> Values.val0
516
517val ev_cmp_match : Integers.comparison -> Values.val0 Types.option
518
519val ev_cmp_mismatch : Integers.comparison -> Values.val0 Types.option
520
521val ev_cmp :
522  Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
523  Types.option
524
525val ev_cmpp :
526  GenMem.mem1 -> Integers.comparison -> Values.val0 -> Values.val0 ->
527  Values.val0 Types.option
528
529val ev_cmpu :
530  Integers.comparison -> Values.val0 -> Values.val0 -> Values.val0
531  Types.option
532
533val eval_binop :
534  GenMem.mem1 -> AST.typ -> AST.typ -> AST.typ -> binary_operation ->
535  Values.val0 -> Values.val0 -> Values.val0 Types.option
536
Note: See TracBrowser for help on using the repository browser.