source: extracted/csyntax.mli @ 2716

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

...

File size: 22.3 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Positive
26
27open Identifiers
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Jmeq
36
37open Russell
38
39open List
40
41open Util
42
43open FoldStuff
44
45open BitVector
46
47open Extranat
48
49open Bool
50
51open Relations
52
53open Nat
54
55open Integers
56
57open Hints_declaration
58
59open Core_notation
60
61open Pts
62
63open Logic
64
65open Types
66
67open AST
68
69open Coqlib
70
71open CostLabel
72
73type type0 =
74| Tvoid
75| Tint of AST.intsize * AST.signedness
76| Tpointer of type0
77| Tarray of type0 * Nat.nat
78| Tfunction of typelist * type0
79| Tstruct of AST.ident * fieldlist
80| Tunion of AST.ident * fieldlist
81| Tcomp_ptr of AST.ident
82and typelist =
83| Tnil
84| Tcons of type0 * typelist
85and fieldlist =
86| Fnil
87| Fcons of AST.ident * type0 * fieldlist
88
89val type_inv_rect_Type4 :
90  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
91  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
92  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
93  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
94
95val type_inv_rect_Type3 :
96  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
97  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
98  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
99  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
100
101val type_inv_rect_Type2 :
102  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
103  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
104  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
105  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
106
107val type_inv_rect_Type1 :
108  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
109  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
110  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
111  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
112
113val type_inv_rect_Type0 :
114  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
115  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
116  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
117  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1
118
119val typelist_inv_rect_Type4 :
120  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
121
122val typelist_inv_rect_Type3 :
123  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
124
125val typelist_inv_rect_Type2 :
126  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
127
128val typelist_inv_rect_Type1 :
129  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
130
131val typelist_inv_rect_Type0 :
132  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
133
134val fieldlist_inv_rect_Type4 :
135  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
136  -> 'a1
137
138val fieldlist_inv_rect_Type3 :
139  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
140  -> 'a1
141
142val fieldlist_inv_rect_Type2 :
143  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
144  -> 'a1
145
146val fieldlist_inv_rect_Type1 :
147  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
148  -> 'a1
149
150val fieldlist_inv_rect_Type0 :
151  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
152  -> 'a1
153
154val type_discr : type0 -> type0 -> __
155
156val typelist_discr : typelist -> typelist -> __
157
158val fieldlist_discr : fieldlist -> fieldlist -> __
159
160val type_jmdiscr : type0 -> type0 -> __
161
162val typelist_jmdiscr : typelist -> typelist -> __
163
164val fieldlist_jmdiscr : fieldlist -> fieldlist -> __
165
166type unary_operation =
167| Onotbool
168| Onotint
169| Oneg
170
171val unary_operation_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
172
173val unary_operation_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
174
175val unary_operation_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
176
177val unary_operation_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
178
179val unary_operation_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
180
181val unary_operation_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
182
183val unary_operation_inv_rect_Type4 :
184  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
185
186val unary_operation_inv_rect_Type3 :
187  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
188
189val unary_operation_inv_rect_Type2 :
190  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
191
192val unary_operation_inv_rect_Type1 :
193  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
194
195val unary_operation_inv_rect_Type0 :
196  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
197
198val unary_operation_discr : unary_operation -> unary_operation -> __
199
200val unary_operation_jmdiscr : unary_operation -> unary_operation -> __
201
202type binary_operation =
203| Oadd
204| Osub
205| Omul
206| Odiv
207| Omod
208| Oand
209| Oor
210| Oxor
211| Oshl
212| Oshr
213| Oeq
214| One0
215| Olt
216| Ogt
217| Ole
218| Oge
219
220val binary_operation_rect_Type4 :
221  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
222  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
223
224val binary_operation_rect_Type5 :
225  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
226  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
227
228val binary_operation_rect_Type3 :
229  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
230  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
231
232val binary_operation_rect_Type2 :
233  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
234  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
235
236val binary_operation_rect_Type1 :
237  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
238  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
239
240val binary_operation_rect_Type0 :
241  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
242  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1
243
244val binary_operation_inv_rect_Type4 :
245  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
246  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
247  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
248  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
249
250val binary_operation_inv_rect_Type3 :
251  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
252  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
253  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
254  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
255
256val binary_operation_inv_rect_Type2 :
257  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
258  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
259  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
260  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
261
262val binary_operation_inv_rect_Type1 :
263  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
264  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
265  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
266  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
267
268val binary_operation_inv_rect_Type0 :
269  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
270  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
271  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
272  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
273
274val binary_operation_discr : binary_operation -> binary_operation -> __
275
276val binary_operation_jmdiscr : binary_operation -> binary_operation -> __
277
278type expr =
279| Expr of expr_descr * type0
280and expr_descr =
281| Econst_int of AST.intsize * AST.bvint
282| Evar of AST.ident
283| Ederef of expr
284| Eaddrof of expr
285| Eunop of unary_operation * expr
286| Ebinop of binary_operation * expr * expr
287| Ecast of type0 * expr
288| Econdition of expr * expr * expr
289| Eandbool of expr * expr
290| Eorbool of expr * expr
291| Esizeof of type0
292| Efield of expr * AST.ident
293| Ecost of CostLabel.costlabel * expr
294
295val expr_inv_rect_Type4 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
296
297val expr_inv_rect_Type3 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
298
299val expr_inv_rect_Type2 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
300
301val expr_inv_rect_Type1 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
302
303val expr_inv_rect_Type0 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
304
305val expr_descr_inv_rect_Type4 :
306  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
307  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
308  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
309  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
310  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
311  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
312  -> __ -> 'a1) -> 'a1
313
314val expr_descr_inv_rect_Type3 :
315  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
316  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
317  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
318  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
319  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
320  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
321  -> __ -> 'a1) -> 'a1
322
323val expr_descr_inv_rect_Type2 :
324  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
325  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
326  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
327  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
328  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
329  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
330  -> __ -> 'a1) -> 'a1
331
332val expr_descr_inv_rect_Type1 :
333  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
334  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
335  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
336  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
337  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
338  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
339  -> __ -> 'a1) -> 'a1
340
341val expr_descr_inv_rect_Type0 :
342  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
343  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
344  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
345  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
346  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
347  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
348  -> __ -> 'a1) -> 'a1
349
350val expr_discr : expr -> expr -> __
351
352val expr_descr_discr : expr_descr -> expr_descr -> __
353
354val expr_jmdiscr : expr -> expr -> __
355
356val expr_descr_jmdiscr : expr_descr -> expr_descr -> __
357
358val typeof : expr -> type0
359
360type label = AST.ident
361
362type statement =
363| Sskip
364| Sassign of expr * expr
365| Scall of expr Types.option * expr * expr List.list
366| Ssequence of statement * statement
367| Sifthenelse of expr * statement * statement
368| Swhile of expr * statement
369| Sdowhile of expr * statement
370| Sfor of statement * expr * statement * statement
371| Sbreak
372| Scontinue
373| Sreturn of expr Types.option
374| Sswitch of expr * labeled_statements
375| Slabel of label * statement
376| Sgoto of label
377| Scost of CostLabel.costlabel * statement
378and labeled_statements =
379| LSdefault of statement
380| LScase of AST.intsize * AST.bvint * statement * labeled_statements
381
382val statement_inv_rect_Type4 :
383  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
384  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
385  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
386  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
387  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
388  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
389  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
390  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
391  'a1
392
393val statement_inv_rect_Type3 :
394  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
395  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
396  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
397  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
398  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
399  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
400  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
401  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
402  'a1
403
404val statement_inv_rect_Type2 :
405  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
406  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
407  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
408  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
409  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
410  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
411  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
412  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
413  'a1
414
415val statement_inv_rect_Type1 :
416  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
417  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
418  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
419  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
420  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
421  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
422  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
423  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
424  'a1
425
426val statement_inv_rect_Type0 :
427  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
428  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
429  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
430  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
431  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
432  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
433  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
434  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
435  'a1
436
437val labeled_statements_inv_rect_Type4 :
438  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
439  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
440
441val labeled_statements_inv_rect_Type3 :
442  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
443  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
444
445val labeled_statements_inv_rect_Type2 :
446  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
447  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
448
449val labeled_statements_inv_rect_Type1 :
450  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
451  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
452
453val labeled_statements_inv_rect_Type0 :
454  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
455  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
456
457val statement_discr : statement -> statement -> __
458
459val labeled_statements_discr : labeled_statements -> labeled_statements -> __
460
461val statement_jmdiscr : statement -> statement -> __
462
463val labeled_statements_jmdiscr :
464  labeled_statements -> labeled_statements -> __
465
466type function0 = { fn_return : type0;
467                   fn_params : (AST.ident, type0) Types.prod List.list;
468                   fn_vars : (AST.ident, type0) Types.prod List.list;
469                   fn_body : statement }
470
471val function_rect_Type4 :
472  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
473  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
474
475val function_rect_Type5 :
476  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
477  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
478
479val function_rect_Type3 :
480  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
481  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
482
483val function_rect_Type2 :
484  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
485  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
486
487val function_rect_Type1 :
488  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
489  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
490
491val function_rect_Type0 :
492  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
493  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
494
495val fn_return : function0 -> type0
496
497val fn_params : function0 -> (AST.ident, type0) Types.prod List.list
498
499val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list
500
501val fn_body : function0 -> statement
502
503val function_inv_rect_Type4 :
504  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
505  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
506
507val function_inv_rect_Type3 :
508  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
509  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
510
511val function_inv_rect_Type2 :
512  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
513  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
514
515val function_inv_rect_Type1 :
516  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
517  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
518
519val function_inv_rect_Type0 :
520  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
521  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1
522
523val function_discr : function0 -> function0 -> __
524
525val function_jmdiscr : function0 -> function0 -> __
526
527type clight_fundef =
528| CL_Internal of function0
529| CL_External of AST.ident * typelist * type0
530
531val clight_fundef_rect_Type4 :
532  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
533  clight_fundef -> 'a1
534
535val clight_fundef_rect_Type5 :
536  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
537  clight_fundef -> 'a1
538
539val clight_fundef_rect_Type3 :
540  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
541  clight_fundef -> 'a1
542
543val clight_fundef_rect_Type2 :
544  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
545  clight_fundef -> 'a1
546
547val clight_fundef_rect_Type1 :
548  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
549  clight_fundef -> 'a1
550
551val clight_fundef_rect_Type0 :
552  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
553  clight_fundef -> 'a1
554
555val clight_fundef_inv_rect_Type4 :
556  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
557  type0 -> __ -> 'a1) -> 'a1
558
559val clight_fundef_inv_rect_Type3 :
560  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
561  type0 -> __ -> 'a1) -> 'a1
562
563val clight_fundef_inv_rect_Type2 :
564  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
565  type0 -> __ -> 'a1) -> 'a1
566
567val clight_fundef_inv_rect_Type1 :
568  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
569  type0 -> __ -> 'a1) -> 'a1
570
571val clight_fundef_inv_rect_Type0 :
572  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
573  type0 -> __ -> 'a1) -> 'a1
574
575val clight_fundef_discr : clight_fundef -> clight_fundef -> __
576
577val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __
578
579type clight_program =
580  (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
581
582val type_of_params : (AST.ident, type0) Types.prod List.list -> typelist
583
584val type_of_function : function0 -> type0
585
586val type_of_fundef : clight_fundef -> type0
587
588val alignof_fields : fieldlist -> Nat.nat
589
590val alignof : type0 -> Nat.nat
591
592val sizeof_union : fieldlist -> Nat.nat
593
594val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat
595
596val sizeof : type0 -> Nat.nat
597
598val field_offset_rec :
599  AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res
600
601val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res
602
603val field_type : AST.ident -> fieldlist -> type0 Errors.res
604
605val typ_of_type : type0 -> AST.typ
606
607val opttyp_of_type : type0 -> AST.typ Types.option
608
609val typlist_of_typelist : typelist -> AST.typ List.list
610
611type mode =
612| By_value of AST.typ
613| By_reference
614| By_nothing of AST.typ
615
616val mode_rect_Type4 :
617  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
618
619val mode_rect_Type5 :
620  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
621
622val mode_rect_Type3 :
623  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
624
625val mode_rect_Type2 :
626  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
627
628val mode_rect_Type1 :
629  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
630
631val mode_rect_Type0 :
632  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
633
634val mode_inv_rect_Type4 :
635  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
636  (AST.typ -> __ -> __ -> 'a1) -> 'a1
637
638val mode_inv_rect_Type3 :
639  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
640  (AST.typ -> __ -> __ -> 'a1) -> 'a1
641
642val mode_inv_rect_Type2 :
643  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
644  (AST.typ -> __ -> __ -> 'a1) -> 'a1
645
646val mode_inv_rect_Type1 :
647  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
648  (AST.typ -> __ -> __ -> 'a1) -> 'a1
649
650val mode_inv_rect_Type0 :
651  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
652  (AST.typ -> __ -> __ -> 'a1) -> 'a1
653
654val mode_discr : AST.typ -> mode -> mode -> __
655
656val mode_jmdiscr : AST.typ -> mode -> mode -> __
657
658val access_mode : type0 -> mode
659
660val signature_of_type : typelist -> type0 -> AST.signature
661
662val external_function0 :
663  AST.ident -> typelist -> type0 -> AST.external_function
664
Note: See TracBrowser for help on using the repository browser.