sig   type constant =       IntConstant of string     | FloatConstant of string     | StringConstant of string     | WStringConstant of string   type logic_type =       LTvoid     | LTinteger     | LTreal     | LTint of Cil_types.ikind     | LTfloat of Cil_types.fkind     | LTarray of Logic_ptree.logic_type * Logic_ptree.constant option     | LTpointer of Logic_ptree.logic_type     | LTenum of string     | LTstruct of string     | LTunion of string     | LTnamed of string * Logic_ptree.logic_type list     | LTarrow of Logic_ptree.logic_type list * Logic_ptree.logic_type     | LTattribute of Logic_ptree.logic_type * Cil_types.attribute   type location = Cil_types.location   type quantifiers = (Logic_ptree.logic_type * string) list   type relation = Lt | Gt | Le | Ge | Eq | Neq   type binop =       Badd     | Bsub     | Bmul     | Bdiv     | Bmod     | Bbw_and     | Bbw_or     | Bbw_xor     | Blshift     | Brshift   type unop = Uminus | Ustar | Uamp | Ubw_not   type lexpr = {     lexpr_node : Logic_ptree.lexpr_node;     lexpr_loc : Logic_ptree.location;   }   and path_elt = PLpathField of string | PLpathIndex of Logic_ptree.lexpr   and update_term =       PLupdateTerm of Logic_ptree.lexpr     | PLupdateCont of         (Logic_ptree.path_elt list * Logic_ptree.update_term) list   and lexpr_node =       PLvar of string     | PLapp of string * string list * Logic_ptree.lexpr list     | PLlambda of Logic_ptree.quantifiers * Logic_ptree.lexpr     | PLlet of string * Logic_ptree.lexpr * Logic_ptree.lexpr     | PLconstant of Logic_ptree.constant     | PLunop of Logic_ptree.unop * Logic_ptree.lexpr     | PLbinop of Logic_ptree.lexpr * Logic_ptree.binop * Logic_ptree.lexpr     | PLdot of Logic_ptree.lexpr * string     | PLarrow of Logic_ptree.lexpr * string     | PLarrget of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLold of Logic_ptree.lexpr     | PLat of Logic_ptree.lexpr * string     | PLresult     | PLnull     | PLcast of Logic_ptree.logic_type * Logic_ptree.lexpr     | PLrange of Logic_ptree.lexpr option * Logic_ptree.lexpr option     | PLsizeof of Logic_ptree.logic_type     | PLsizeofE of Logic_ptree.lexpr     | PLcoercion of Logic_ptree.lexpr * Logic_ptree.logic_type     | PLcoercionE of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLupdate of Logic_ptree.lexpr * Logic_ptree.path_elt list *         Logic_ptree.update_term     | PLinitIndex of (Logic_ptree.lexpr * Logic_ptree.lexpr) list     | PLinitField of (string * Logic_ptree.lexpr) list     | PLtypeof of Logic_ptree.lexpr     | PLtype of Logic_ptree.logic_type     | PLfalse     | PLtrue     | PLrel of Logic_ptree.lexpr * Logic_ptree.relation * Logic_ptree.lexpr     | PLand of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLor of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLxor of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLimplies of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLiff of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLnot of Logic_ptree.lexpr     | PLif of Logic_ptree.lexpr * Logic_ptree.lexpr * Logic_ptree.lexpr     | PLforall of Logic_ptree.quantifiers * Logic_ptree.lexpr     | PLexists of Logic_ptree.quantifiers * Logic_ptree.lexpr     | PLbase_addr of string option * Logic_ptree.lexpr     | PLoffset of string option * Logic_ptree.lexpr     | PLblock_length of string option * Logic_ptree.lexpr     | PLvalid of string option * Logic_ptree.lexpr     | PLvalid_read of string option * Logic_ptree.lexpr     | PLvalid_function of Logic_ptree.lexpr     | PLallocable of string option * Logic_ptree.lexpr     | PLfreeable of string option * Logic_ptree.lexpr     | PLinitialized of string option * Logic_ptree.lexpr     | PLdangling of string option * Logic_ptree.lexpr     | PLfresh of (string * string) option * Logic_ptree.lexpr *         Logic_ptree.lexpr     | PLseparated of Logic_ptree.lexpr list     | PLnamed of string * Logic_ptree.lexpr     | PLsubtype of Logic_ptree.lexpr * Logic_ptree.lexpr     | PLcomprehension of Logic_ptree.lexpr * Logic_ptree.quantifiers *         Logic_ptree.lexpr option     | PLset of Logic_ptree.lexpr list     | PLunion of Logic_ptree.lexpr list     | PLinter of Logic_ptree.lexpr list     | PLempty     | PLlist of Logic_ptree.lexpr list     | PLrepeat of Logic_ptree.lexpr * Logic_ptree.lexpr   type type_annot = {     inv_name : string;     this_type : Logic_ptree.logic_type;     this_name : string;     inv : Logic_ptree.lexpr;   }   type model_annot = {     model_for_type : Logic_ptree.logic_type;     model_type : Logic_ptree.logic_type;     model_name : string;   }   type typedef =       TDsum of (string * Logic_ptree.logic_type list) list     | TDsyn of Logic_ptree.logic_type   type decl = {     decl_node : Logic_ptree.decl_node;     decl_loc : Logic_ptree.location;   }   and decl_node =       LDlogic_def of string * string list * string list *         Logic_ptree.logic_type * (Logic_ptree.logic_type * string) list *         Logic_ptree.lexpr     | LDlogic_reads of string * string list * string list *         Logic_ptree.logic_type * (Logic_ptree.logic_type * string) list *         Logic_ptree.lexpr list option     | LDtype of string * string list * Logic_ptree.typedef option     | LDpredicate_reads of string * string list * string list *         (Logic_ptree.logic_type * string) list *         Logic_ptree.lexpr list option     | LDpredicate_def of string * string list * string list *         (Logic_ptree.logic_type * string) list * Logic_ptree.lexpr     | LDinductive_def of string * string list * string list *         (Logic_ptree.logic_type * string) list *         (string * string list * string list * Logic_ptree.lexpr) list     | LDlemma of string * bool * string list * string list *         Logic_ptree.lexpr     | LDaxiomatic of string * Logic_ptree.decl list     | LDinvariant of string * Logic_ptree.lexpr     | LDtype_annot of Logic_ptree.type_annot     | LDmodel_annot of Logic_ptree.model_annot     | LDvolatile of Logic_ptree.lexpr list * (string option * string option)   and deps = Logic_ptree.lexpr Cil_types.deps   type extension = string * Logic_ptree.lexpr list   type behavior = {     mutable b_name : string;     mutable b_requires : Logic_ptree.lexpr list;     mutable b_assumes : Logic_ptree.lexpr list;     mutable b_post_cond :       (Cil_types.termination_kind * Logic_ptree.lexpr) list;     mutable b_assigns : Logic_ptree.lexpr Cil_types.assigns;     mutable b_allocation : Logic_ptree.lexpr Cil_types.allocation;     mutable b_extended : Logic_ptree.extension list;   }   type spec = {     mutable spec_behavior : Logic_ptree.behavior list;     mutable spec_variant : Logic_ptree.lexpr Cil_types.variant option;     mutable spec_terminates : Logic_ptree.lexpr option;     mutable spec_complete_behaviors : string list list;     mutable spec_disjoint_behaviors : string list list;   }   type code_annot =       AAssert of string list * Logic_ptree.lexpr     | AStmtSpec of string list * Logic_ptree.spec     | AInvariant of string list * bool * Logic_ptree.lexpr     | AVariant of Logic_ptree.lexpr Cil_types.variant     | AAssigns of string list * Logic_ptree.lexpr Cil_types.assigns     | AAllocation of string list * Logic_ptree.lexpr Cil_types.allocation     | APragma of Logic_ptree.lexpr Cil_types.pragma     | AExtended of string list * Logic_ptree.extension   type assigns = Logic_ptree.lexpr Cil_types.assigns   type variant = Logic_ptree.lexpr Cil_types.variant   type custom_tree =       CustomType of Logic_ptree.logic_type     | CustomLexpr of Logic_ptree.lexpr     | CustomOther of string * Logic_ptree.custom_tree list   type annot =       Adecl of Logic_ptree.decl list     | Aspec     | Acode_annot of Logic_ptree.location * Logic_ptree.code_annot     | Aloop_annot of Logic_ptree.location * Logic_ptree.code_annot list     | Aattribute_annot of Logic_ptree.location * string     | Acustom of Logic_ptree.location * string * Logic_ptree.custom_tree   type ext_decl =       Ext_decl of Logic_ptree.decl     | Ext_macro of string * Logic_ptree.lexpr     | Ext_include of bool * string * Logic_ptree.location   type ext_function =       Ext_spec of Logic_ptree.spec * Logic_ptree.location     | Ext_stmt of string list * Logic_ptree.annot * Logic_ptree.location     | Ext_glob of Logic_ptree.ext_decl   type ext_module =       string option * Logic_ptree.ext_decl list *       ((string * Logic_ptree.location) option * Logic_ptree.ext_function list)       list   type ext_spec = Logic_ptree.ext_module list end