sig   type file = {     mutable fileName : string;     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;     mutable cattr : Cil_types.attributes;     mutable cdefined : bool;     mutable creferenced : bool;   }   and fieldinfo = {     mutable fcomp : Cil_types.compinfo;     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 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 blocals : 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;   }   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 Pervasives.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 Pervasives.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     | 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 Pervasives.ref list;   }   and location = Lexing.position * Lexing.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 Pervasives.ref     | LogicLabel of (Cil_types.stmt option * string)   and term = {     term_node : Cil_types.term_node;     term_loc : Lexing.position * Lexing.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 * 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     | TCoerce of Cil_types.term * Cil_types.typ     | TCoerceE of Cil_types.term * 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;   }   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 = {     lt_name : string;     lt_params : string list;     mutable lt_def : Cil_types.logic_type_def option;   }   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;   }   and logic_ctor_info = {     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 * 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     | 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     | Psubtype of Cil_types.term * Cil_types.term   and identified_predicate = {     ip_id : int;     ip_content : Cil_types.predicate;   }   and predicate = {     pred_name : string list;     pred_loc : Cil_types.location;     pred_content : Cil_types.predicate_node;   }   and 'term variant = 'term * string option   and 'locs allocation = FreeAlloc of 'locs list * 'locs list | FreeAllocAny   and 'locs deps = From of 'locs list | FromAny   and 'locs from = 'locs * 'locs Cil_types.deps   and 'locs assigns = WritesAny | Writes of 'locs Cil_types.from list   and spec = {     mutable spec_behavior : Cil_types.behavior list;     mutable spec_variant : Cil_types.term 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 = string * 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   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.identified_term Cil_types.assigns;     mutable b_allocation : Cil_types.identified_term Cil_types.allocation;     mutable b_extended : Cil_types.acsl_extension list;   }   and termination_kind = Normal | Exits | Breaks | Continues | Returns   and 'term loop_pragma =       Unroll_specs of 'term list     | Widen_hints of 'term list     | Widen_variables of 'term list   and 'term slice_pragma = SPexpr of 'term | SPctrl | SPstmt   and 'term impact_pragma = IPexpr of 'term | IPstmt   and 'term pragma =       Loop_pragma of 'term Cil_types.loop_pragma     | Slice_pragma of 'term Cil_types.slice_pragma     | Impact_pragma of 'term Cil_types.impact_pragma   and code_annotation_node =       AAssert of string list * Cil_types.predicate     | AStmtSpec of string list * Cil_types.spec     | AInvariant of string list * bool * Cil_types.predicate     | AVariant of Cil_types.term Cil_types.variant     | AAssigns of string list * Cil_types.identified_term Cil_types.assigns     | AAllocation of string list *         Cil_types.identified_term Cil_types.allocation     | APragma of Cil_types.term Cil_types.pragma     | AExtended of string list * 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.location     | Daxiomatic of string * Cil_types.global_annotation list *         Cil_types.location     | Dtype of Cil_types.logic_type_info * Cil_types.location     | Dlemma of string * bool * Cil_types.logic_label list * string list *         Cil_types.predicate * 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     | Dcustom_annot of Cil_types.custom_tree * string * 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 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;     __thread_is_keyword : bool;     compiler : string;     version : string;   } end