extracted/csyntax.mli

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open ErrorMessages
  10
  11 open PreIdentifiers
  12
  13 open Errors
  14
  15 open Extralib
  16
  17 open Lists
  18
  19 open Positive
  20
  21 open Identifiers
  22
  23 open Exp
  24
  25 open Arithmetic
  26
  27 open Vector
  28
  29 open Div_and_mod
  30
  31 open Util
  32
  33 open FoldStuff
  34
  35 open BitVector
  36
  37 open Jmeq
  38
  39 open Russell
  40
  41 open List
  42
  43 open Setoids
  44
  45 open Monad
  46
  47 open Option
  48
  49 open Extranat
  50
  51 open Bool
  52
  53 open Relations
  54
  55 open Nat
  56
  57 open Integers
  58
  59 open Hints_declaration
  60
  61 open Core_notation
  62
  63 open Pts
  64
  65 open Logic
  66
  67 open Types
  68
  69 open AST
  70
  71 open Coqlib
  72
  73 open CostLabel
  74
  75 type 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
  84 and typelist =
  85 | Tnil
  86 | Tcons of type0 * typelist
  87 and fieldlist =
  88 | Fnil
  89 | Fcons of AST.ident * type0 * fieldlist
  90
  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
  96
  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
 102
 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
 108
 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
 114
 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
 120
 121 val typelist_inv_rect_Type4 :
 122   typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
 123
 124 val typelist_inv_rect_Type3 :
 125   typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
 126
 127 val typelist_inv_rect_Type2 :
 128   typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
 129
 130 val typelist_inv_rect_Type1 :
 131   typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
 132
 133 val typelist_inv_rect_Type0 :
 134   typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1
 135
 136 val fieldlist_inv_rect_Type4 :
 137   fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
 138   -> 'a1
 139
 140 val fieldlist_inv_rect_Type3 :
 141   fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
 142   -> 'a1
 143
 144 val fieldlist_inv_rect_Type2 :
 145   fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
 146   -> 'a1
 147
 148 val fieldlist_inv_rect_Type1 :
 149   fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
 150   -> 'a1
 151
 152 val fieldlist_inv_rect_Type0 :
 153   fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
 154   -> 'a1
 155
 156 val type_discr : type0 -> type0 -> __
 157
 158 val typelist_discr : typelist -> typelist -> __
 159
 160 val fieldlist_discr : fieldlist -> fieldlist -> __
 161
 162 val type_jmdiscr : type0 -> type0 -> __
 163
 164 val typelist_jmdiscr : typelist -> typelist -> __
 165
 166 val fieldlist_jmdiscr : fieldlist -> fieldlist -> __
 167
 168 type unary_operation =
 169 | Onotbool
 170 | Onotint
 171 | Oneg
 172
 173 val unary_operation_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
 174
 175 val unary_operation_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
 176
 177 val unary_operation_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
 178
 179 val unary_operation_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
 180
 181 val unary_operation_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
 182
 183 val unary_operation_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1
 184
 185 val unary_operation_inv_rect_Type4 :
 186   unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 187
 188 val unary_operation_inv_rect_Type3 :
 189   unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 190
 191 val unary_operation_inv_rect_Type2 :
 192   unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 193
 194 val unary_operation_inv_rect_Type1 :
 195   unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 196
 197 val unary_operation_inv_rect_Type0 :
 198   unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1
 199
 200 val unary_operation_discr : unary_operation -> unary_operation -> __
 201
 202 val unary_operation_jmdiscr : unary_operation -> unary_operation -> __
 203
 204 type 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
 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
 225
 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
 229
 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
 233
 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
 237
 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
 241
 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
 245
 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
 251
 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
 257
 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
 263
 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
 269
 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
 275
 276 val binary_operation_discr : binary_operation -> binary_operation -> __
 277
 278 val binary_operation_jmdiscr : binary_operation -> binary_operation -> __
 279
 280 type expr =
 281 | Expr of expr_descr * type0
 282 and 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
 297 val expr_inv_rect_Type4 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
 298
 299 val expr_inv_rect_Type3 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
 300
 301 val expr_inv_rect_Type2 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
 302
 303 val expr_inv_rect_Type1 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
 304
 305 val expr_inv_rect_Type0 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1
 306
 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
 314   -> __ -> 'a1) -> 'a1
 315
 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
 323   -> __ -> 'a1) -> 'a1
 324
 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
 332   -> __ -> 'a1) -> 'a1
 333
 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
 341   -> __ -> 'a1) -> 'a1
 342
 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
 350   -> __ -> 'a1) -> 'a1
 351
 352 val expr_discr : expr -> expr -> __
 353
 354 val expr_descr_discr : expr_descr -> expr_descr -> __
 355
 356 val expr_jmdiscr : expr -> expr -> __
 357
 358 val expr_descr_jmdiscr : expr_descr -> expr_descr -> __
 359
 360 val typeof : expr -> type0
 361
 362 type label = AST.ident
 363
 364 type 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
 380 and labeled_statements =
 381 | LSdefault of statement
 382 | LScase of AST.intsize * AST.bvint * statement * labeled_statements
 383
 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) ->
 393   'a1
 394
 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) ->
 404   'a1
 405
 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) ->
 415   'a1
 416
 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) ->
 426   'a1
 427
 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) ->
 437   'a1
 438
 439 val labeled_statements_inv_rect_Type4 :
 440   labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
 441   -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
 442
 443 val labeled_statements_inv_rect_Type3 :
 444   labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
 445   -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
 446
 447 val labeled_statements_inv_rect_Type2 :
 448   labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
 449   -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
 450
 451 val labeled_statements_inv_rect_Type1 :
 452   labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
 453   -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
 454
 455 val labeled_statements_inv_rect_Type0 :
 456   labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
 457   -> statement -> labeled_statements -> __ -> 'a1) -> 'a1
 458
 459 val statement_discr : statement -> statement -> __
 460
 461 val labeled_statements_discr : labeled_statements -> labeled_statements -> __
 462
 463 val statement_jmdiscr : statement -> statement -> __
 464
 465 val labeled_statements_jmdiscr :
 466   labeled_statements -> labeled_statements -> __
 467
 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 }
 472
 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
 476
 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
 480
 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
 484
 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
 488
 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
 492
 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
 496
 497 val fn_return : function0 -> type0
 498
 499 val fn_params : function0 -> (AST.ident, type0) Types.prod List.list
 500
 501 val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list
 502
 503 val fn_body : function0 -> statement
 504
 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
 508
 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
 512
 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
 516
 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
 520
 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
 524
 525 val function_discr : function0 -> function0 -> __
 526
 527 val function_jmdiscr : function0 -> function0 -> __
 528
 529 type clight_fundef =
 530 | CL_Internal of function0
 531 | CL_External of AST.ident * typelist * type0
 532
 533 val clight_fundef_rect_Type4 :
 534   (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
 535   clight_fundef -> 'a1
 536
 537 val clight_fundef_rect_Type5 :
 538   (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
 539   clight_fundef -> 'a1
 540
 541 val clight_fundef_rect_Type3 :
 542   (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
 543   clight_fundef -> 'a1
 544
 545 val clight_fundef_rect_Type2 :
 546   (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
 547   clight_fundef -> 'a1
 548
 549 val clight_fundef_rect_Type1 :
 550   (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
 551   clight_fundef -> 'a1
 552
 553 val clight_fundef_rect_Type0 :
 554   (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
 555   clight_fundef -> 'a1
 556
 557 val clight_fundef_inv_rect_Type4 :
 558   clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
 559   type0 -> __ -> 'a1) -> 'a1
 560
 561 val clight_fundef_inv_rect_Type3 :
 562   clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
 563   type0 -> __ -> 'a1) -> 'a1
 564
 565 val clight_fundef_inv_rect_Type2 :
 566   clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
 567   type0 -> __ -> 'a1) -> 'a1
 568
 569 val clight_fundef_inv_rect_Type1 :
 570   clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
 571   type0 -> __ -> 'a1) -> 'a1
 572
 573 val clight_fundef_inv_rect_Type0 :
 574   clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
 575   type0 -> __ -> 'a1) -> 'a1
 576
 577 val clight_fundef_discr : clight_fundef -> clight_fundef -> __
 578
 579 val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __
 580
 581 type clight_program =
 582   (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program
 583
 584 val type_of_params : (AST.ident, type0) Types.prod List.list -> typelist
 585
 586 val type_of_function : function0 -> type0
 587
 588 val type_of_fundef : clight_fundef -> type0
 589
 590 val alignof_fields : fieldlist -> Nat.nat
 591
 592 val alignof : type0 -> Nat.nat
 593
 594 val sizeof_union : fieldlist -> Nat.nat
 595
 596 val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat
 597
 598 val sizeof : type0 -> Nat.nat
 599
 600 val field_offset_rec :
 601   AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res
 602
 603 val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res
 604
 605 val field_type : AST.ident -> fieldlist -> type0 Errors.res
 606
 607 val typ_of_type : type0 -> AST.typ
 608
 609 val opttyp_of_type : type0 -> AST.typ Types.option
 610
 611 val typlist_of_typelist : typelist -> AST.typ List.list
 612
 613 type mode =
 614 | By_value of AST.typ
 615 | By_reference
 616 | By_nothing of AST.typ
 617
 618 val mode_rect_Type4 :
 619   (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
 620
 621 val mode_rect_Type5 :
 622   (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
 623
 624 val mode_rect_Type3 :
 625   (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
 626
 627 val mode_rect_Type2 :
 628   (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
 629
 630 val mode_rect_Type1 :
 631   (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
 632
 633 val mode_rect_Type0 :
 634   (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1
 635
 636 val mode_inv_rect_Type4 :
 637   AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
 638   (AST.typ -> __ -> __ -> 'a1) -> 'a1
 639
 640 val mode_inv_rect_Type3 :
 641   AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
 642   (AST.typ -> __ -> __ -> 'a1) -> 'a1
 643
 644 val mode_inv_rect_Type2 :
 645   AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
 646   (AST.typ -> __ -> __ -> 'a1) -> 'a1
 647
 648 val mode_inv_rect_Type1 :
 649   AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
 650   (AST.typ -> __ -> __ -> 'a1) -> 'a1
 651
 652 val mode_inv_rect_Type0 :
 653   AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
 654   (AST.typ -> __ -> __ -> 'a1) -> 'a1
 655
 656 val mode_discr : AST.typ -> mode -> mode -> __
 657
 658 val mode_jmdiscr : AST.typ -> mode -> mode -> __
 659
 660 val access_mode : type0 -> mode
 661
 662 val signature_of_type : typelist -> type0 -> AST.signature
 663
 664 val external_function :
 665   AST.ident -> typelist -> type0 -> AST.external_function
 666