source: driver/extracted/csyntax.mli @ 3106

Last change on this file since 3106 was 3043, checked in by sacerdot, 7 years ago

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

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