open Preamble

open Proper

open PositiveMap

open Deqsets

open ErrorMessages

open PreIdentifiers

open Errors

open Extralib

open Lists

open Positive

open Identifiers

open Exp

open Arithmetic

open Vector

open Div_and_mod

open Util

open FoldStuff

open BitVector

open Jmeq

open Russell

open List

open Setoids

open Monad

open Option

open Extranat

open Bool

open Relations

open Nat

open Integers

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open AST

open Coqlib

open CostLabel

type type0 =
| Tvoid
| Tint of AST.intsize * AST.signedness
| Tpointer of type0
| Tarray of type0 * Nat.nat
| Tfunction of typelist * type0
| Tstruct of AST.ident * fieldlist
| Tunion of AST.ident * fieldlist
| Tcomp_ptr of AST.ident
and typelist =
| Tnil
| Tcons of type0 * typelist
and fieldlist =
| Fnil
| Fcons of AST.ident * type0 * fieldlist

val type_inv_rect_Type4 :
  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val type_inv_rect_Type3 :
  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val type_inv_rect_Type2 :
  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val type_inv_rect_Type1 :
  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val type_inv_rect_Type0 :
  type0 -> (__ -> 'a1) -> (AST.intsize -> AST.signedness -> __ -> 'a1) ->
  (type0 -> __ -> 'a1) -> (type0 -> Nat.nat -> __ -> 'a1) -> (typelist ->
  type0 -> __ -> 'a1) -> (AST.ident -> fieldlist -> __ -> 'a1) -> (AST.ident
  -> fieldlist -> __ -> 'a1) -> (AST.ident -> __ -> 'a1) -> 'a1

val typelist_inv_rect_Type4 :
  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1

val typelist_inv_rect_Type3 :
  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1

val typelist_inv_rect_Type2 :
  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1

val typelist_inv_rect_Type1 :
  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1

val typelist_inv_rect_Type0 :
  typelist -> (__ -> 'a1) -> (type0 -> typelist -> __ -> 'a1) -> 'a1

val fieldlist_inv_rect_Type4 :
  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
  -> 'a1

val fieldlist_inv_rect_Type3 :
  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
  -> 'a1

val fieldlist_inv_rect_Type2 :
  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
  -> 'a1

val fieldlist_inv_rect_Type1 :
  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
  -> 'a1

val fieldlist_inv_rect_Type0 :
  fieldlist -> (__ -> 'a1) -> (AST.ident -> type0 -> fieldlist -> __ -> 'a1)
  -> 'a1

val type_discr : type0 -> type0 -> __

val typelist_discr : typelist -> typelist -> __

val fieldlist_discr : fieldlist -> fieldlist -> __

val type_jmdiscr : type0 -> type0 -> __

val typelist_jmdiscr : typelist -> typelist -> __

val fieldlist_jmdiscr : fieldlist -> fieldlist -> __

type unary_operation =
| Onotbool
| Onotint
| Oneg

val unary_operation_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1

val unary_operation_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1

val unary_operation_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1

val unary_operation_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1

val unary_operation_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1

val unary_operation_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> unary_operation -> 'a1

val unary_operation_inv_rect_Type4 :
  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type3 :
  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type2 :
  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type1 :
  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val unary_operation_inv_rect_Type0 :
  unary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val unary_operation_discr : unary_operation -> unary_operation -> __

val unary_operation_jmdiscr : unary_operation -> unary_operation -> __

type binary_operation =
| Oadd
| Osub
| Omul
| Odiv
| Omod
| Oand
| Oor
| Oxor
| Oshl
| Oshr
| Oeq
| One
| Olt
| Ogt
| Ole
| Oge

val binary_operation_rect_Type4 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1

val binary_operation_rect_Type5 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1

val binary_operation_rect_Type3 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1

val binary_operation_rect_Type2 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1

val binary_operation_rect_Type1 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1

val binary_operation_rect_Type0 :
  'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1
  -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> binary_operation -> 'a1

val binary_operation_inv_rect_Type4 :
  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type3 :
  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type2 :
  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type1 :
  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val binary_operation_inv_rect_Type0 :
  binary_operation -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ ->
  'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1

val binary_operation_discr : binary_operation -> binary_operation -> __

val binary_operation_jmdiscr : binary_operation -> binary_operation -> __

type expr =
| Expr of expr_descr * type0
and expr_descr =
| Econst_int of AST.intsize * AST.bvint
| Evar of AST.ident
| Ederef of expr
| Eaddrof of expr
| Eunop of unary_operation * expr
| Ebinop of binary_operation * expr * expr
| Ecast of type0 * expr
| Econdition of expr * expr * expr
| Eandbool of expr * expr
| Eorbool of expr * expr
| Esizeof of type0
| Efield of expr * AST.ident
| Ecost of CostLabel.costlabel * expr

val expr_inv_rect_Type4 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1

val expr_inv_rect_Type3 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1

val expr_inv_rect_Type2 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1

val expr_inv_rect_Type1 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1

val expr_inv_rect_Type0 : expr -> (expr_descr -> type0 -> __ -> 'a1) -> 'a1

val expr_descr_inv_rect_Type4 :
  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
  -> __ -> 'a1) -> 'a1

val expr_descr_inv_rect_Type3 :
  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
  -> __ -> 'a1) -> 'a1

val expr_descr_inv_rect_Type2 :
  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
  -> __ -> 'a1) -> 'a1

val expr_descr_inv_rect_Type1 :
  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
  -> __ -> 'a1) -> 'a1

val expr_descr_inv_rect_Type0 :
  expr_descr -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> (AST.ident -> __
  -> 'a1) -> (expr -> __ -> 'a1) -> (expr -> __ -> 'a1) -> (unary_operation
  -> expr -> __ -> 'a1) -> (binary_operation -> expr -> expr -> __ -> 'a1) ->
  (type0 -> expr -> __ -> 'a1) -> (expr -> expr -> expr -> __ -> 'a1) ->
  (expr -> expr -> __ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (type0 -> __
  -> 'a1) -> (expr -> AST.ident -> __ -> 'a1) -> (CostLabel.costlabel -> expr
  -> __ -> 'a1) -> 'a1

val expr_discr : expr -> expr -> __

val expr_descr_discr : expr_descr -> expr_descr -> __

val expr_jmdiscr : expr -> expr -> __

val expr_descr_jmdiscr : expr_descr -> expr_descr -> __

val typeof : expr -> type0

type label = AST.ident

type statement =
| Sskip
| Sassign of expr * expr
| Scall of expr Types.option * expr * expr List.list
| Ssequence of statement * statement
| Sifthenelse of expr * statement * statement
| Swhile of expr * statement
| Sdowhile of expr * statement
| Sfor of statement * expr * statement * statement
| Sbreak
| Scontinue
| Sreturn of expr Types.option
| Sswitch of expr * labeled_statements
| Slabel of label * statement
| Sgoto of label
| Scost of CostLabel.costlabel * statement
and labeled_statements =
| LSdefault of statement
| LScase of AST.intsize * AST.bvint * statement * labeled_statements

val statement_inv_rect_Type4 :
  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
  'a1

val statement_inv_rect_Type3 :
  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
  'a1

val statement_inv_rect_Type2 :
  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
  'a1

val statement_inv_rect_Type1 :
  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
  'a1

val statement_inv_rect_Type0 :
  statement -> (__ -> 'a1) -> (expr -> expr -> __ -> 'a1) -> (expr
  Types.option -> expr -> expr List.list -> __ -> 'a1) -> (statement ->
  statement -> __ -> 'a1) -> (expr -> statement -> statement -> __ -> 'a1) ->
  (expr -> statement -> __ -> 'a1) -> (expr -> statement -> __ -> 'a1) ->
  (statement -> expr -> statement -> statement -> __ -> 'a1) -> (__ -> 'a1)
  -> (__ -> 'a1) -> (expr Types.option -> __ -> 'a1) -> (expr ->
  labeled_statements -> __ -> 'a1) -> (label -> statement -> __ -> 'a1) ->
  (label -> __ -> 'a1) -> (CostLabel.costlabel -> statement -> __ -> 'a1) ->
  'a1

val labeled_statements_inv_rect_Type4 :
  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1

val labeled_statements_inv_rect_Type3 :
  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1

val labeled_statements_inv_rect_Type2 :
  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1

val labeled_statements_inv_rect_Type1 :
  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1

val labeled_statements_inv_rect_Type0 :
  labeled_statements -> (statement -> __ -> 'a1) -> (AST.intsize -> AST.bvint
  -> statement -> labeled_statements -> __ -> 'a1) -> 'a1

val statement_discr : statement -> statement -> __

val labeled_statements_discr : labeled_statements -> labeled_statements -> __

val statement_jmdiscr : statement -> statement -> __

val labeled_statements_jmdiscr :
  labeled_statements -> labeled_statements -> __

type function0 = { fn_return : type0;
                   fn_params : (AST.ident, type0) Types.prod List.list;
                   fn_vars : (AST.ident, type0) Types.prod List.list;
                   fn_body : statement }

val function_rect_Type4 :
  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1

val function_rect_Type5 :
  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1

val function_rect_Type3 :
  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1

val function_rect_Type2 :
  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1

val function_rect_Type1 :
  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1

val function_rect_Type0 :
  (type0 -> (AST.ident, type0) Types.prod List.list -> (AST.ident, type0)
  Types.prod List.list -> statement -> 'a1) -> function0 -> 'a1

val fn_return : function0 -> type0

val fn_params : function0 -> (AST.ident, type0) Types.prod List.list

val fn_vars : function0 -> (AST.ident, type0) Types.prod List.list

val fn_body : function0 -> statement

val function_inv_rect_Type4 :
  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1

val function_inv_rect_Type3 :
  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1

val function_inv_rect_Type2 :
  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1

val function_inv_rect_Type1 :
  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1

val function_inv_rect_Type0 :
  function0 -> (type0 -> (AST.ident, type0) Types.prod List.list ->
  (AST.ident, type0) Types.prod List.list -> statement -> __ -> 'a1) -> 'a1

val function_discr : function0 -> function0 -> __

val function_jmdiscr : function0 -> function0 -> __

type clight_fundef =
| CL_Internal of function0
| CL_External of AST.ident * typelist * type0

val clight_fundef_rect_Type4 :
  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
  clight_fundef -> 'a1

val clight_fundef_rect_Type5 :
  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
  clight_fundef -> 'a1

val clight_fundef_rect_Type3 :
  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
  clight_fundef -> 'a1

val clight_fundef_rect_Type2 :
  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
  clight_fundef -> 'a1

val clight_fundef_rect_Type1 :
  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
  clight_fundef -> 'a1

val clight_fundef_rect_Type0 :
  (function0 -> 'a1) -> (AST.ident -> typelist -> type0 -> 'a1) ->
  clight_fundef -> 'a1

val clight_fundef_inv_rect_Type4 :
  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
  type0 -> __ -> 'a1) -> 'a1

val clight_fundef_inv_rect_Type3 :
  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
  type0 -> __ -> 'a1) -> 'a1

val clight_fundef_inv_rect_Type2 :
  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
  type0 -> __ -> 'a1) -> 'a1

val clight_fundef_inv_rect_Type1 :
  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
  type0 -> __ -> 'a1) -> 'a1

val clight_fundef_inv_rect_Type0 :
  clight_fundef -> (function0 -> __ -> 'a1) -> (AST.ident -> typelist ->
  type0 -> __ -> 'a1) -> 'a1

val clight_fundef_discr : clight_fundef -> clight_fundef -> __

val clight_fundef_jmdiscr : clight_fundef -> clight_fundef -> __

type clight_program =
  (clight_fundef, (AST.init_data List.list, type0) Types.prod) AST.program

val type_of_params : (AST.ident, type0) Types.prod List.list -> typelist

val type_of_function : function0 -> type0

val type_of_fundef : clight_fundef -> type0

val alignof_fields : fieldlist -> Nat.nat

val alignof : type0 -> Nat.nat

val sizeof_union : fieldlist -> Nat.nat

val sizeof_struct : fieldlist -> Nat.nat -> Nat.nat

val sizeof : type0 -> Nat.nat

val field_offset_rec :
  AST.ident -> fieldlist -> Nat.nat -> Nat.nat Errors.res

val field_offset : AST.ident -> fieldlist -> Nat.nat Errors.res

val field_type : AST.ident -> fieldlist -> type0 Errors.res

val typ_of_type : type0 -> AST.typ

val opttyp_of_type : type0 -> AST.typ Types.option

val typlist_of_typelist : typelist -> AST.typ List.list

type mode =
| By_value of AST.typ
| By_reference
| By_nothing of AST.typ

val mode_rect_Type4 :
  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1

val mode_rect_Type5 :
  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1

val mode_rect_Type3 :
  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1

val mode_rect_Type2 :
  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1

val mode_rect_Type1 :
  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1

val mode_rect_Type0 :
  (AST.typ -> 'a1) -> 'a1 -> (AST.typ -> 'a1) -> AST.typ -> mode -> 'a1

val mode_inv_rect_Type4 :
  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
  (AST.typ -> __ -> __ -> 'a1) -> 'a1

val mode_inv_rect_Type3 :
  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
  (AST.typ -> __ -> __ -> 'a1) -> 'a1

val mode_inv_rect_Type2 :
  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
  (AST.typ -> __ -> __ -> 'a1) -> 'a1

val mode_inv_rect_Type1 :
  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
  (AST.typ -> __ -> __ -> 'a1) -> 'a1

val mode_inv_rect_Type0 :
  AST.typ -> mode -> (AST.typ -> __ -> __ -> 'a1) -> (__ -> __ -> 'a1) ->
  (AST.typ -> __ -> __ -> 'a1) -> 'a1

val mode_discr : AST.typ -> mode -> mode -> __

val mode_jmdiscr : AST.typ -> mode -> mode -> __

val access_mode : type0 -> mode

val signature_of_type : typelist -> type0 -> AST.signature

val external_function :
  AST.ident -> typelist -> type0 -> AST.external_function