source: extracted/csyntax.mli @ 3009

Last change on this file since 3009 was 3001, checked in by sacerdot, 7 years ago

New extraction.

File size: 22.3 KB
RevLine 
[2601]1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
[2649]9open ErrorMessages
10
[2601]11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Lists
18
19open Positive
20
21open Identifiers
22
[2717]23open Exp
24
[2601]25open Arithmetic
26
27open Vector
28
29open Div_and_mod
30
[2773]31open Util
32
33open FoldStuff
34
35open BitVector
36
[2601]37open Jmeq
38
39open Russell
40
41open List
42
[2773]43open Setoids
[2601]44
[2773]45open Monad
[2601]46
[2773]47open Option
[2601]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
[2649]71open Coqlib
72
[2601]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
[2773]216| One
[2601]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
[3001]664val external_function0 :
[2601]665  AST.ident -> typelist -> type0 -> AST.external_function
666
Note: See TracBrowser for help on using the repository browser.