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 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
| 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 : 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