59 open Hints_declaration
77 | Tint of AST.intsize * AST.signedness
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
86 | Tcons of type0 * typelist
89 | Fcons of AST.ident * type0 * fieldlist
91 val 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
97 val 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
103 val 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
109 val 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
115 val 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
121 val typelist_inv_rect_Type4 :
122 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
124 val typelist_inv_rect_Type3 :
125 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
127 val typelist_inv_rect_Type2 :
128 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
130 val typelist_inv_rect_Type1 :
131 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
133 val typelist_inv_rect_Type0 :
134 typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
136 val fieldlist_inv_rect_Type4 :
137 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
140 val fieldlist_inv_rect_Type3 :
141 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
144 val fieldlist_inv_rect_Type2 :
145 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
148 val fieldlist_inv_rect_Type1 :
149 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
152 val fieldlist_inv_rect_Type0 :
153 fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
156 val type_discr : type0 -> type0 -> __
158 val typelist_discr : typelist -> typelist -> __
160 val fieldlist_discr : fieldlist -> fieldlist -> __
162 val type_jmdiscr : type0 -> type0 -> __
164 val typelist_jmdiscr : typelist -> typelist -> __
166 val fieldlist_jmdiscr : fieldlist -> fieldlist -> __
168 type unary_operation =
173 val unary_operation_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
175 val unary_operation_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
177 val unary_operation_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
179 val unary_operation_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
181 val unary_operation_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
183 val unary_operation_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
185 val unary_operation_inv_rect_Type4 :
186 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
188 val unary_operation_inv_rect_Type3 :
189 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
191 val unary_operation_inv_rect_Type2 :
192 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
194 val unary_operation_inv_rect_Type1 :
195 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
197 val unary_operation_inv_rect_Type0 :
198 unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
200 val unary_operation_discr : unary_operation -> unary_operation -> __
202 val unary_operation_jmdiscr : unary_operation -> unary_operation -> __
204 type binary_operation =
222 val 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
226 val 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
230 val 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
234 val 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
238 val 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
242 val 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
246 val 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
252 val 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
258 val 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
264 val 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
270 val 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
276 val binary_operation_discr : binary_operation -> binary_operation -> __
278 val binary_operation_jmdiscr : binary_operation -> binary_operation -> __
281 | Expr of expr_descr * type0
283 | Econst_int of AST.intsize * AST.bvint
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
294 | Efield of expr * AST.ident
295 | Ecost of CostLabel.costlabel * expr
297 val expr_inv_rect_Type4 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
299 val expr_inv_rect_Type3 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
301 val expr_inv_rect_Type2 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
303 val expr_inv_rect_Type1 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
305 val expr_inv_rect_Type0 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
307 val 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
316 val 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
325 val 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
334 val 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
343 val 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
352 val expr_discr : expr -> expr -> __
354 val expr_descr_discr : expr_descr -> expr_descr -> __
356 val expr_jmdiscr : expr -> expr -> __
358 val expr_descr_jmdiscr : expr_descr -> expr_descr -> __
360 val typeof : expr -> type0
362 type label = AST.ident
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
375 | Sreturn of expr Types.option
376 | Sswitch of expr * labeled_statements
377 | Slabel of label * statement
379 | Scost of CostLabel.costlabel * statement
380 and labeled_statements =
381 | LSdefault of statement
382 | LScase of AST.intsize * AST.bvint * statement * labeled_statements
384 val 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) ->
395 val 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) ->
406 val 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) ->
417 val 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) ->
428 val 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) ->
439 val labeled_statements_inv_rect_Type4 :
440 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
441 -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
443 val labeled_statements_inv_rect_Type3 :
444 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
445 -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
447 val labeled_statements_inv_rect_Type2 :
448 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
449 -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
451 val labeled_statements_inv_rect_Type1 :
452 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
453 -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
455 val labeled_statements_inv_rect_Type0 :
456 labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
457 -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
459 val statement_discr : statement -> statement -> __
461 val labeled_statements_discr : labeled_statements -> labeled_statements -> __
463 val statement_jmdiscr : statement -> statement -> __
465 val labeled_statements_jmdiscr :
466 labeled_statements -> labeled_statements -> __
468 type 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 }
473 val function_rect_Type4 :
474 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
475 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
477 val function_rect_Type5 :
478 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
479 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
481 val function_rect_Type3 :
482 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
483 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
485 val function_rect_Type2 :
486 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
487 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
489 val function_rect_Type1 :
490 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
491 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
493 val function_rect_Type0 :
494 (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
495 Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1
497 val fn_return : function0 -> type0
499 val fn_params : function0 -> (AST.ident, type0) Types.prod List.list
501 val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list
503 val fn_body : function0 -> statement
505 val 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
509 val 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
513 val 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
517 val 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
521 val 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
525 val function_discr : function0 -> function0 -> __
527 val function_jmdiscr : function0 -> function0 -> __
530 | CL_Internal of function0
531 | CL_External of AST.ident * typelist * type0
533 val clight_fundef_rect_Type4 :
534 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
537 val clight_fundef_rect_Type5 :
538 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
541 val clight_fundef_rect_Type3 :
542 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
545 val clight_fundef_rect_Type2 :
546 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
549 val clight_fundef_rect_Type1 :
550 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
553 val clight_fundef_rect_Type0 :
554 (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
557 val clight_fundef_inv_rect_Type4 :
558 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
559 type0 -> __ -> 'a1) -> 'a1
561 val clight_fundef_inv_rect_Type3 :
562 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
563 type0 -> __ -> 'a1) -> 'a1
565 val clight_fundef_inv_rect_Type2 :
566 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
567 type0 -> __ -> 'a1) -> 'a1
569 val clight_fundef_inv_rect_Type1 :
570 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
571 type0 -> __ -> 'a1) -> 'a1
573 val clight_fundef_inv_rect_Type0 :
574 clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
575 type0 -> __ -> 'a1) -> 'a1
577 val clight_fundef_discr : clight_fundef -> clight_fundef -> __
579 val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __
581 type clight_program =
582 (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
584 val type_of_params : (AST.ident, type0) Types.prod List.list -> typelist
586 val type_of_function : function0 -> type0
588 val type_of_fundef : clight_fundef -> type0
590 val alignof_fields : fieldlist -> Nat.nat
592 val alignof : type0 -> Nat.nat
594 val sizeof_union : fieldlist -> Nat.nat
596 val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat
598 val sizeof : type0 -> Nat.nat
600 val field_offset_rec :
601 AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res
603 val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res
605 val field_type : AST.ident -> fieldlist -> type0 Errors.res
607 val typ_of_type : type0 -> AST.typ
609 val opttyp_of_type : type0 -> AST.typ Types.option
611 val typlist_of_typelist : typelist -> AST.typ List.list
614 | By_value of AST.typ
616 | By_nothing of AST.typ
618 val mode_rect_Type4 :
619 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
621 val mode_rect_Type5 :
622 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
624 val mode_rect_Type3 :
625 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
627 val mode_rect_Type2 :
628 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
630 val mode_rect_Type1 :
631 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
633 val mode_rect_Type0 :
634 (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
636 val mode_inv_rect_Type4 :
637 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
638 (AST.typ -> __ -> __ -> 'a1) -> 'a1
640 val mode_inv_rect_Type3 :
641 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
642 (AST.typ -> __ -> __ -> 'a1) -> 'a1
644 val mode_inv_rect_Type2 :
645 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
646 (AST.typ -> __ -> __ -> 'a1) -> 'a1
648 val mode_inv_rect_Type1 :
649 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
650 (AST.typ -> __ -> __ -> 'a1) -> 'a1
652 val mode_inv_rect_Type0 :
653 AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
654 (AST.typ -> __ -> __ -> 'a1) -> 'a1
656 val mode_discr : AST.typ -> mode -> mode -> __
658 val mode_jmdiscr : AST.typ -> mode -> mode -> __
660 val access_mode : type0 -> mode
662 val signature_of_type : typelist -> type0 -> AST.signature
664 val external_function :
665 AST.ident -> typelist -> type0 -> AST.external_function