sig
  type constant =
      IntConstant of string
    | FloatConstant of string
    | StringConstant of string
    | WStringConstant of string
  type array_size = ASinteger of string | ASidentifier of string | ASnone
  type logic_type =
      LTvoid
    | LTinteger
    | LTreal
    | LTint of Cil_types.ikind
    | LTfloat of Cil_types.fkind
    | LTarray of Logic_ptree.logic_type * Logic_ptree.array_size
    | 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
    | 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
    | PLobject_pointer 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
    | 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 toplevel_predicate = {
    tp_only_check : bool;
    tp_statement : Logic_ptree.lexpr;
  }
  type extension = string * Logic_ptree.lexpr list
  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.toplevel_predicate
    | 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)
    | LDextended of Logic_ptree.global_extension
  and deps = From of Logic_ptree.lexpr list | FromAny
  and from = Logic_ptree.lexpr * Logic_ptree.deps
  and assigns = WritesAny | Writes of Logic_ptree.from list
  and allocation =
      FreeAlloc of Logic_ptree.lexpr list * Logic_ptree.lexpr list
    | FreeAllocAny
  and variant = Logic_ptree.lexpr * string option
  and global_extension =
      Ext_lexpr of string * Logic_ptree.lexpr list
    | Ext_extension of string * string * Logic_ptree.extended_decl list
  and extended_decl = {
    extended_node : Logic_ptree.global_extension;
    extended_loc : Logic_ptree.location;
  }
  type behavior = {
    mutable b_name : string;
    mutable b_requires : Logic_ptree.toplevel_predicate list;
    mutable b_assumes : Logic_ptree.lexpr list;
    mutable b_post_cond :
      (Cil_types.termination_kind * Logic_ptree.toplevel_predicate) list;
    mutable b_assigns : Logic_ptree.assigns;
    mutable b_allocation : Logic_ptree.allocation;
    mutable b_extended : Logic_ptree.extension list;
  }
  type spec = {
    mutable spec_behavior : Logic_ptree.behavior list;
    mutable spec_variant : Logic_ptree.variant option;
    mutable spec_terminates : Logic_ptree.lexpr option;
    mutable spec_complete_behaviors : string list list;
    mutable spec_disjoint_behaviors : string list list;
  }
  type loop_pragma =
      Unroll_specs of Logic_ptree.lexpr list
    | Widen_hints of Logic_ptree.lexpr list
    | Widen_variables of Logic_ptree.lexpr list
  and slice_pragma = SPexpr of Logic_ptree.lexpr | SPctrl | SPstmt
  and impact_pragma = IPexpr of Logic_ptree.lexpr | IPstmt
  and pragma =
      Loop_pragma of Logic_ptree.loop_pragma
    | Slice_pragma of Logic_ptree.slice_pragma
    | Impact_pragma of Logic_ptree.impact_pragma
  type code_annot =
      AAssert of string list * Logic_ptree.toplevel_predicate
    | AStmtSpec of string list * Logic_ptree.spec
    | AInvariant of string list * bool * Logic_ptree.toplevel_predicate
    | AVariant of Logic_ptree.variant
    | AAssigns of string list * Logic_ptree.assigns
    | AAllocation of string list * Logic_ptree.allocation
    | APragma of Logic_ptree.pragma
    | AExtended of string list * bool * Logic_ptree.extension
  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 bool * 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