sig
  type file = {
    mutable fileName : Filepath.Normalized.t;
    mutable globals : Cil_types.global list;
    mutable globinit : Cil_types.fundec option;
    mutable globinitcalled : bool;
  }
  and global =
      GType of Cil_types.typeinfo * Cil_types.location
    | GCompTag of Cil_types.compinfo * Cil_types.location
    | GCompTagDecl of Cil_types.compinfo * Cil_types.location
    | GEnumTag of Cil_types.enuminfo * Cil_types.location
    | GEnumTagDecl of Cil_types.enuminfo * Cil_types.location
    | GVarDecl of Cil_types.varinfo * Cil_types.location
    | GFunDecl of Cil_types.funspec * Cil_types.varinfo * Cil_types.location
    | GVar of Cil_types.varinfo * Cil_types.initinfo * Cil_types.location
    | GFun of Cil_types.fundec * Cil_types.location
    | GAsm of string * Cil_types.location
    | GPragma of Cil_types.attribute * Cil_types.location
    | GText of string
    | GAnnot of Cil_types.global_annotation * Cil_types.location
  and typ =
      TVoid of Cil_types.attributes
    | TInt of Cil_types.ikind * Cil_types.attributes
    | TFloat of Cil_types.fkind * Cil_types.attributes
    | TPtr of Cil_types.typ * Cil_types.attributes
    | TArray of Cil_types.typ * Cil_types.exp option *
        Cil_types.bitsSizeofTypCache * Cil_types.attributes
    | TFun of Cil_types.typ *
        (string * Cil_types.typ * Cil_types.attributes) list option * 
        bool * Cil_types.attributes
    | TNamed of Cil_types.typeinfo * Cil_types.attributes
    | TComp of Cil_types.compinfo * Cil_types.bitsSizeofTypCache *
        Cil_types.attributes
    | TEnum of Cil_types.enuminfo * Cil_types.attributes
    | TBuiltin_va_list of Cil_types.attributes
  and ikind =
      IBool
    | IChar
    | ISChar
    | IUChar
    | IInt
    | IUInt
    | IShort
    | IUShort
    | ILong
    | IULong
    | ILongLong
    | IULongLong
  and fkind = FFloat | FDouble | FLongDouble
  and bitsSizeofTyp =
      Not_Computed
    | Computed of int
    | Not_Computable of (string * Cil_types.typ)
  and bitsSizeofTypCache = { mutable scache : Cil_types.bitsSizeofTyp; }
  and attribute =
      Attr of string * Cil_types.attrparam list
    | AttrAnnot of string
  and attributes = Cil_types.attribute list
  and attrparam =
      AInt of Integer.t
    | AStr of string
    | ACons of string * Cil_types.attrparam list
    | ASizeOf of Cil_types.typ
    | ASizeOfE of Cil_types.attrparam
    | AAlignOf of Cil_types.typ
    | AAlignOfE of Cil_types.attrparam
    | AUnOp of Cil_types.unop * Cil_types.attrparam
    | ABinOp of Cil_types.binop * Cil_types.attrparam * Cil_types.attrparam
    | ADot of Cil_types.attrparam * string
    | AStar of Cil_types.attrparam
    | AAddrOf of Cil_types.attrparam
    | AIndex of Cil_types.attrparam * Cil_types.attrparam
    | AQuestion of Cil_types.attrparam * Cil_types.attrparam *
        Cil_types.attrparam
  and compinfo = {
    mutable cstruct : bool;
    corig_name : string;
    mutable cname : string;
    mutable ckey : int;
    mutable cfields : Cil_types.fieldinfo list option;
    mutable cattr : Cil_types.attributes;
    mutable creferenced : bool;
  }
  and fieldinfo = {
    mutable fcomp : Cil_types.compinfo;
    mutable forder : int;
    forig_name : string;
    mutable fname : string;
    mutable ftype : Cil_types.typ;
    mutable fbitfield : int option;
    mutable fattr : Cil_types.attributes;
    mutable floc : Cil_types.location;
    mutable faddrof : bool;
    mutable fsize_in_bits : int option;
    mutable foffset_in_bits : int option;
    mutable fpadding_in_bits : int option;
  }
  and enuminfo = {
    eorig_name : string;
    mutable ename : string;
    mutable eitems : Cil_types.enumitem list;
    mutable eattr : Cil_types.attributes;
    mutable ereferenced : bool;
    mutable ekind : Cil_types.ikind;
  }
  and enumitem = {
    eiorig_name : string;
    mutable einame : string;
    mutable eival : Cil_types.exp;
    mutable eihost : Cil_types.enuminfo;
    eiloc : Cil_types.location;
  }
  and typeinfo = {
    torig_name : string;
    mutable tname : string;
    mutable ttype : Cil_types.typ;
    mutable treferenced : bool;
  }
  and varinfo = {
    mutable vname : string;
    vorig_name : string;
    mutable vtype : Cil_types.typ;
    mutable vattr : Cil_types.attributes;
    mutable vstorage : Cil_types.storage;
    mutable vglob : bool;
    mutable vdefined : bool;
    mutable vformal : bool;
    mutable vinline : bool;
    mutable vdecl : Cil_types.location;
    mutable vid : int;
    mutable vaddrof : bool;
    mutable vreferenced : bool;
    vtemp : bool;
    mutable vdescr : string option;
    mutable vdescrpure : bool;
    mutable vghost : bool;
    vsource : bool;
    mutable vlogic_var_assoc : Cil_types.logic_var option;
  }
  and storage = NoStorage | Static | Register | Extern
  and exp = {
    eid : int;
    enode : Cil_types.exp_node;
    eloc : Cil_types.location;
  }
  and exp_node =
      Const of Cil_types.constant
    | Lval of Cil_types.lval
    | SizeOf of Cil_types.typ
    | SizeOfE of Cil_types.exp
    | SizeOfStr of string
    | AlignOf of Cil_types.typ
    | AlignOfE of Cil_types.exp
    | UnOp of Cil_types.unop * Cil_types.exp * Cil_types.typ
    | BinOp of Cil_types.binop * Cil_types.exp * Cil_types.exp *
        Cil_types.typ
    | CastE of Cil_types.typ * Cil_types.exp
    | AddrOf of Cil_types.lval
    | StartOf of Cil_types.lval
    | Info of Cil_types.exp * Cil_types.exp_info
  and exp_info = { exp_type : Cil_types.logic_type; exp_name : string list; }
  and constant =
      CInt64 of Integer.t * Cil_types.ikind * string option
    | CStr of string
    | CWStr of int64 list
    | CChr of char
    | CReal of float * Cil_types.fkind * string option
    | CEnum of Cil_types.enumitem
  and unop = Neg | BNot | LNot
  and binop =
      PlusA
    | PlusPI
    | IndexPI
    | MinusA
    | MinusPI
    | MinusPP
    | Mult
    | Div
    | Mod
    | Shiftlt
    | Shiftrt
    | Lt
    | Gt
    | Le
    | Ge
    | Eq
    | Ne
    | BAnd
    | BXor
    | BOr
    | LAnd
    | LOr
  and lval = Cil_types.lhost * Cil_types.offset
  and lhost = Var of Cil_types.varinfo | Mem of Cil_types.exp
  and offset =
      NoOffset
    | Field of Cil_types.fieldinfo * Cil_types.offset
    | Index of Cil_types.exp * Cil_types.offset
  and init =
      SingleInit of Cil_types.exp
    | CompoundInit of Cil_types.typ *
        (Cil_types.offset * Cil_types.init) list
  and initinfo = { mutable init : Cil_types.init option; }
  and constructor_kind = Plain_func | Constructor
  and local_init =
      AssignInit of Cil_types.init
    | ConsInit of Cil_types.varinfo * Cil_types.exp list *
        Cil_types.constructor_kind
  and fundec = {
    mutable svar : Cil_types.varinfo;
    mutable sformals : Cil_types.varinfo list;
    mutable slocals : Cil_types.varinfo list;
    mutable smaxid : int;
    mutable sbody : Cil_types.block;
    mutable smaxstmtid : int option;
    mutable sallstmts : Cil_types.stmt list;
    mutable sspec : Cil_types.funspec;
  }
  and block = {
    mutable battrs : Cil_types.attributes;
    mutable bscoping : bool;
    mutable blocals : Cil_types.varinfo list;
    mutable bstatics : Cil_types.varinfo list;
    mutable bstmts : Cil_types.stmt list;
  }
  and stmt = {
    mutable labels : Cil_types.label list;
    mutable skind : Cil_types.stmtkind;
    mutable sid : int;
    mutable succs : Cil_types.stmt list;
    mutable preds : Cil_types.stmt list;
    mutable ghost : bool;
    mutable sattr : Cil_types.attributes;
  }
  and label =
      Label of string * Cil_types.location * bool
    | Case of Cil_types.exp * Cil_types.location
    | Default of Cil_types.location
  and stmtkind =
      Instr of Cil_types.instr
    | Return of Cil_types.exp option * Cil_types.location
    | Goto of Cil_types.stmt Stdlib.ref * Cil_types.location
    | Break of Cil_types.location
    | Continue of Cil_types.location
    | If of Cil_types.exp * Cil_types.block * Cil_types.block *
        Cil_types.location
    | Switch of Cil_types.exp * Cil_types.block * Cil_types.stmt list *
        Cil_types.location
    | Loop of Cil_types.code_annotation list * Cil_types.block *
        Cil_types.location * Cil_types.stmt option * Cil_types.stmt option
    | Block of Cil_types.block
    | UnspecifiedSequence of
        (Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
         Cil_types.lval list * Cil_types.stmt Stdlib.ref list)
        list
    | Throw of (Cil_types.exp * Cil_types.typ) option * Cil_types.location
    | TryCatch of Cil_types.block *
        (Cil_types.catch_binder * Cil_types.block) list * Cil_types.location
    | TryFinally of Cil_types.block * Cil_types.block * Cil_types.location
    | TryExcept of Cil_types.block * (Cil_types.instr list * Cil_types.exp) *
        Cil_types.block * Cil_types.location
  and catch_binder =
      Catch_exn of Cil_types.varinfo *
        (Cil_types.varinfo * Cil_types.block) list
    | Catch_all
  and instr =
      Set of Cil_types.lval * Cil_types.exp * Cil_types.location
    | Call of Cil_types.lval option * Cil_types.exp * Cil_types.exp list *
        Cil_types.location
    | Local_init of Cil_types.varinfo * Cil_types.local_init *
        Cil_types.location
    | Asm of Cil_types.attributes * string list *
        Cil_types.extended_asm option * Cil_types.location
    | Skip of Cil_types.location
    | Code_annot of Cil_types.code_annotation * Cil_types.location
  and extended_asm = {
    asm_outputs : (string option * string * Cil_types.lval) list;
    asm_inputs : (string option * string * Cil_types.exp) list;
    asm_clobbers : string list;
    asm_gotos : Cil_types.stmt Stdlib.ref list;
  }
  and location = Filepath.position * Filepath.position
  and logic_constant =
      Integer of Integer.t * string option
    | LStr of string
    | LWStr of int64 list
    | LChr of char
    | LReal of Cil_types.logic_real
    | LEnum of Cil_types.enumitem
  and logic_real = {
    r_literal : string;
    r_nearest : float;
    r_upper : float;
    r_lower : float;
  }
  and logic_type =
      Ctype of Cil_types.typ
    | Ltype of Cil_types.logic_type_info * Cil_types.logic_type list
    | Lvar of string
    | Linteger
    | Lreal
    | Larrow of Cil_types.logic_type list * Cil_types.logic_type
  and identified_term = { it_id : int; it_content : Cil_types.term; }
  and logic_label =
      StmtLabel of Cil_types.stmt Stdlib.ref
    | FormalLabel of string
    | BuiltinLabel of Cil_types.logic_builtin_label
  and logic_builtin_label =
      Here
    | Old
    | Pre
    | Post
    | LoopEntry
    | LoopCurrent
    | Init
  and term = {
    term_node : Cil_types.term_node;
    term_loc : Filepath.position * Filepath.position;
    term_type : Cil_types.logic_type;
    term_name : string list;
  }
  and term_node =
      TConst of Cil_types.logic_constant
    | TLval of Cil_types.term_lval
    | TSizeOf of Cil_types.typ
    | TSizeOfE of Cil_types.term
    | TSizeOfStr of string
    | TAlignOf of Cil_types.typ
    | TAlignOfE of Cil_types.term
    | TUnOp of Cil_types.unop * Cil_types.term
    | TBinOp of Cil_types.binop * Cil_types.term * Cil_types.term
    | TCastE of Cil_types.typ * Cil_types.term
    | TAddrOf of Cil_types.term_lval
    | TStartOf of Cil_types.term_lval
    | Tapp of Cil_types.logic_info * Cil_types.logic_label list *
        Cil_types.term list
    | Tlambda of Cil_types.quantifiers * Cil_types.term
    | TDataCons of Cil_types.logic_ctor_info * Cil_types.term list
    | Tif of Cil_types.term * Cil_types.term * Cil_types.term
    | Tat of Cil_types.term * Cil_types.logic_label
    | Tbase_addr of Cil_types.logic_label * Cil_types.term
    | Toffset of Cil_types.logic_label * Cil_types.term
    | Tblock_length of Cil_types.logic_label * Cil_types.term
    | Tnull
    | TLogic_coerce of Cil_types.logic_type * Cil_types.term
    | TUpdate of Cil_types.term * Cil_types.term_offset * Cil_types.term
    | Ttypeof of Cil_types.term
    | Ttype of Cil_types.typ
    | Tempty_set
    | Tunion of Cil_types.term list
    | Tinter of Cil_types.term list
    | Tcomprehension of Cil_types.term * Cil_types.quantifiers *
        Cil_types.predicate option
    | Trange of Cil_types.term option * Cil_types.term option
    | Tlet of Cil_types.logic_info * Cil_types.term
  and term_lval = Cil_types.term_lhost * Cil_types.term_offset
  and term_lhost =
      TVar of Cil_types.logic_var
    | TResult of Cil_types.typ
    | TMem of Cil_types.term
  and model_info = {
    mi_name : string;
    mi_field_type : Cil_types.logic_type;
    mi_base_type : Cil_types.typ;
    mi_decl : Cil_types.location;
    mutable mi_attr : Cil_types.attributes;
  }
  and term_offset =
      TNoOffset
    | TField of Cil_types.fieldinfo * Cil_types.term_offset
    | TModel of Cil_types.model_info * Cil_types.term_offset
    | TIndex of Cil_types.term * Cil_types.term_offset
  and logic_info = {
    mutable l_var_info : Cil_types.logic_var;
    mutable l_labels : Cil_types.logic_label list;
    mutable l_tparams : string list;
    mutable l_type : Cil_types.logic_type option;
    mutable l_profile : Cil_types.logic_var list;
    mutable l_body : Cil_types.logic_body;
  }
  and builtin_logic_info = {
    mutable bl_name : string;
    mutable bl_labels : Cil_types.logic_label list;
    mutable bl_params : string list;
    mutable bl_type : Cil_types.logic_type option;
    mutable bl_profile : (string * Cil_types.logic_type) list;
  }
  and logic_body =
      LBnone
    | LBreads of Cil_types.identified_term list
    | LBterm of Cil_types.term
    | LBpred of Cil_types.predicate
    | LBinductive of
        (string * Cil_types.logic_label list * string list *
         Cil_types.predicate)
        list
  and logic_type_info = {
    mutable lt_name : string;
    lt_params : string list;
    mutable lt_def : Cil_types.logic_type_def option;
    mutable lt_attr : Cil_types.attributes;
  }
  and logic_type_def =
      LTsum of Cil_types.logic_ctor_info list
    | LTsyn of Cil_types.logic_type
  and logic_var_kind = LVGlobal | LVC | LVFormal | LVQuant | LVLocal
  and logic_var = {
    mutable lv_name : string;
    mutable lv_id : int;
    mutable lv_type : Cil_types.logic_type;
    mutable lv_kind : Cil_types.logic_var_kind;
    mutable lv_origin : Cil_types.varinfo option;
    mutable lv_attr : Cil_types.attributes;
  }
  and logic_ctor_info = {
    mutable ctor_name : string;
    ctor_type : Cil_types.logic_type_info;
    ctor_params : Cil_types.logic_type list;
  }
  and quantifiers = Cil_types.logic_var list
  and relation = Rlt | Rgt | Rle | Rge | Req | Rneq
  and predicate_node =
      Pfalse
    | Ptrue
    | Papp of Cil_types.logic_info * Cil_types.logic_label list *
        Cil_types.term list
    | Pseparated of Cil_types.term list
    | Prel of Cil_types.relation * Cil_types.term * Cil_types.term
    | Pand of Cil_types.predicate * Cil_types.predicate
    | Por of Cil_types.predicate * Cil_types.predicate
    | Pxor of Cil_types.predicate * Cil_types.predicate
    | Pimplies of Cil_types.predicate * Cil_types.predicate
    | Piff of Cil_types.predicate * Cil_types.predicate
    | Pnot of Cil_types.predicate
    | Pif of Cil_types.term * Cil_types.predicate * Cil_types.predicate
    | Plet of Cil_types.logic_info * Cil_types.predicate
    | Pforall of Cil_types.quantifiers * Cil_types.predicate
    | Pexists of Cil_types.quantifiers * Cil_types.predicate
    | Pat of Cil_types.predicate * Cil_types.logic_label
    | Pobject_pointer of Cil_types.logic_label * Cil_types.term
    | Pvalid_read of Cil_types.logic_label * Cil_types.term
    | Pvalid of Cil_types.logic_label * Cil_types.term
    | Pvalid_function of Cil_types.term
    | Pinitialized of Cil_types.logic_label * Cil_types.term
    | Pdangling of Cil_types.logic_label * Cil_types.term
    | Pallocable of Cil_types.logic_label * Cil_types.term
    | Pfreeable of Cil_types.logic_label * Cil_types.term
    | Pfresh of Cil_types.logic_label * Cil_types.logic_label *
        Cil_types.term * Cil_types.term
  and identified_predicate = {
    ip_id : int;
    ip_content : Cil_types.toplevel_predicate;
  }
  and predicate_kind = Assert | Check | Admit
  and toplevel_predicate = {
    tp_kind : Cil_types.predicate_kind;
    tp_statement : Cil_types.predicate;
  }
  and predicate = {
    pred_name : string list;
    pred_loc : Cil_types.location;
    pred_content : Cil_types.predicate_node;
  }
  and variant = Cil_types.term * Cil_types.logic_info option
  and allocation =
      FreeAlloc of Cil_types.identified_term list *
        Cil_types.identified_term list
    | FreeAllocAny
  and deps = From of Cil_types.identified_term list | FromAny
  and from = Cil_types.identified_term * Cil_types.deps
  and assigns = WritesAny | Writes of Cil_types.from list
  and spec = {
    mutable spec_behavior : Cil_types.behavior list;
    mutable spec_variant : Cil_types.variant option;
    mutable spec_terminates : Cil_types.identified_predicate option;
    mutable spec_complete_behaviors : string list list;
    mutable spec_disjoint_behaviors : string list list;
  }
  and acsl_extension = {
    ext_id : int;
    ext_name : string;
    ext_loc : Cil_types.location;
    ext_has_status : bool;
    ext_kind : Cil_types.acsl_extension_kind;
  }
  and acsl_extension_kind =
      Ext_id of int
    | Ext_terms of Cil_types.term list
    | Ext_preds of Cil_types.predicate list
    | Ext_annot of string * Cil_types.acsl_extension list
  and ext_category =
      Ext_contract
    | Ext_global
    | Ext_code_annot of Cil_types.ext_code_annot_context
  and ext_code_annot_context =
      Ext_here
    | Ext_next_stmt
    | Ext_next_loop
    | Ext_next_both
  and behavior = {
    mutable b_name : string;
    mutable b_requires : Cil_types.identified_predicate list;
    mutable b_assumes : Cil_types.identified_predicate list;
    mutable b_post_cond :
      (Cil_types.termination_kind * Cil_types.identified_predicate) list;
    mutable b_assigns : Cil_types.assigns;
    mutable b_allocation : Cil_types.allocation;
    mutable b_extended : Cil_types.acsl_extension list;
  }
  and termination_kind = Normal | Exits | Breaks | Continues | Returns
  and loop_pragma =
      Unroll_specs of Cil_types.term list
    | Widen_hints of Cil_types.term list
    | Widen_variables of Cil_types.term list
  and slice_pragma = SPexpr of Cil_types.term | SPctrl | SPstmt
  and impact_pragma = IPexpr of Cil_types.term | IPstmt
  and pragma =
      Loop_pragma of Cil_types.loop_pragma
    | Slice_pragma of Cil_types.slice_pragma
    | Impact_pragma of Cil_types.impact_pragma
  and code_annotation_node =
      AAssert of string list * Cil_types.toplevel_predicate
    | AStmtSpec of string list * Cil_types.spec
    | AInvariant of string list * bool * Cil_types.toplevel_predicate
    | AVariant of Cil_types.variant
    | AAssigns of string list * Cil_types.assigns
    | AAllocation of string list * Cil_types.allocation
    | APragma of Cil_types.pragma
    | AExtended of string list * bool * Cil_types.acsl_extension
  and funspec = Cil_types.spec
  and code_annotation = {
    annot_id : int;
    annot_content : Cil_types.code_annotation_node;
  }
  and funbehavior = Cil_types.behavior
  and global_annotation =
      Dfun_or_pred of Cil_types.logic_info * Cil_types.location
    | Dvolatile of Cil_types.identified_term list *
        Cil_types.varinfo option * Cil_types.varinfo option *
        Cil_types.attributes * Cil_types.location
    | Daxiomatic of string * Cil_types.global_annotation list *
        Cil_types.attributes * Cil_types.location
    | Dtype of Cil_types.logic_type_info * Cil_types.location
    | Dlemma of string * Cil_types.logic_label list * string list *
        Cil_types.toplevel_predicate * Cil_types.attributes *
        Cil_types.location
    | Dinvariant of Cil_types.logic_info * Cil_types.location
    | Dtype_annot of Cil_types.logic_info * Cil_types.location
    | Dmodel_annot of Cil_types.model_info * Cil_types.location
    | Dextended of Cil_types.acsl_extension * Cil_types.attributes *
        Cil_types.location
    | Dcustom_annot of Cil_types.custom_tree * string *
        Cil_types.attributes * Cil_types.location
  and custom_tree = CustomDummy
  type kinstr = Kstmt of Cil_types.stmt | Kglobal
  type cil_function =
      Definition of (Cil_types.fundec * Cil_types.location)
    | Declaration of
        (Cil_types.funspec * Cil_types.varinfo *
         Cil_types.varinfo list option * Cil_types.location)
  type kernel_function = {
    mutable fundec : Cil_types.cil_function;
    mutable spec : Cil_types.funspec;
  }
  type localisation =
      VGlobal
    | VLocal of Cil_types.kernel_function
    | VFormal of Cil_types.kernel_function
  type syntactic_scope =
      Program
    | Translation_unit of Filepath.Normalized.t
    | Block_scope of Cil_types.stmt
  type mach = {
    sizeof_short : int;
    sizeof_int : int;
    sizeof_long : int;
    sizeof_longlong : int;
    sizeof_ptr : int;
    sizeof_float : int;
    sizeof_double : int;
    sizeof_longdouble : int;
    sizeof_void : int;
    sizeof_fun : int;
    size_t : string;
    wchar_t : string;
    ptrdiff_t : string;
    alignof_short : int;
    alignof_int : int;
    alignof_long : int;
    alignof_longlong : int;
    alignof_ptr : int;
    alignof_float : int;
    alignof_double : int;
    alignof_longdouble : int;
    alignof_str : int;
    alignof_fun : int;
    char_is_unsigned : bool;
    underscore_name : bool;
    const_string_literals : bool;
    little_endian : bool;
    alignof_aligned : int;
    has__builtin_va_list : bool;
    compiler : string;
    cpp_arch_flags : string list;
    version : string;
  }
end