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
  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 : Cil_types.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
    | 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
    | PLsingleton of Logic_ptree.lexpr
    | PLunion of Logic_ptree.lexpr list
    | PLinter of Logic_ptree.lexpr list
    | PLempty
  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 : Cil_types.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 spec =
      (Logic_ptree.lexpr, Logic_ptree.lexpr, Logic_ptree.lexpr)
      Cil_types.spec
  type code_annot =
      (Logic_ptree.lexpr, Logic_ptree.lexpr, Logic_ptree.lexpr,
       Logic_ptree.lexpr)
      Cil_types.code_annot
  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 Cil_types.location * Logic_ptree.code_annot
    | Aloop_annot of Cil_types.location * Logic_ptree.code_annot list
    | Aattribute_annot of Cil_types.location * string
    | Acustom of Cil_types.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 * Cil_types.location
  type ext_function =
      Ext_spec of Logic_ptree.spec * Cil_types.location
    | Ext_loop_spec of string * Logic_ptree.annot * Cil_types.location
    | Ext_stmt_spec of string * Logic_ptree.annot * Cil_types.location
    | Ext_glob of Logic_ptree.ext_decl
  type ext_module =
      string * Logic_ptree.ext_decl list *
      ((string * Cil_types.location) * Logic_ptree.ext_function list) list
  type ext_spec = Logic_ptree.ext_module list
end