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 = 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
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.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.lexpr
| AStmtSpec of string list * Logic_ptree.spec
| AInvariant of string list * bool * Logic_ptree.lexpr
| 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 * 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