module Logic_ptree:sig
..end
type
constant =
| |
IntConstant of |
(* | integer constant | *) |
| |
FloatConstant of |
(* | real constant | *) |
| |
StringConstant of |
(* | string constant | *) |
| |
WStringConstant of |
(* | wide string constant | *) |
type
logic_type =
| |
LTvoid |
(* | C void | *) |
| |
LTinteger |
(* | mathematical integers. | *) |
| |
LTreal |
(* | mathematical real. | *) |
| |
LTint of |
(* | C integral type. | *) |
| |
LTfloat of |
(* | C floating-point type | *) |
| |
LTarray of |
(* | C array | *) |
| |
LTpointer of |
(* | C pointer | *) |
| |
LTenum of |
(* | C enum | *) |
| |
LTstruct of |
(* | C struct | *) |
| |
LTunion of |
(* | C union | *) |
| |
LTnamed of |
(* | declared logic type. | *) |
| |
LTarrow of |
typequantifiers =
(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 : |
(* | kind of expression. | *) |
|
lexpr_loc : |
(* | position in the source code. | *) |
type
path_elt =
| |
PLpathField of |
| |
PLpathIndex of |
type
update_term =
| |
PLupdateTerm of |
| |
PLupdateCont of |
type
lexpr_node =
| |
PLvar of |
(* | a variable | *) |
| |
PLapp of |
(* | an application. | *) |
| |
PLlambda of |
(* | a lambda abstraction. | *) |
| |
PLlet of |
(* | local binding. | *) |
| |
PLconstant of |
(* | a constant. | *) |
| |
PLunop of |
(* | unary operator. | *) |
| |
PLbinop of |
(* | binary operator. | *) |
| |
PLdot of |
(* | field access () | *) |
| |
PLarrow of |
(* | field access () | *) |
| |
PLarrget of |
(* | array access. | *) |
| |
PLold of |
(* | expression refers to pre-state of a function. | *) |
| |
PLat of |
(* | expression refers to a given program point. | *) |
| |
PLresult |
(* | value returned by a function. | *) |
| |
PLnull |
(* | null pointer. | *) |
| |
PLcast of |
(* | cast. | *) |
| |
PLrange of |
(* | interval of integers. | *) |
| |
PLsizeof of |
(* | sizeof a type. | *) |
| |
PLsizeofE of |
(* | sizeof the type of an expression. | *) |
| |
PLcoercion of |
(* | coercion of an expression in a given type. | *) |
| |
PLcoercionE of |
(* | coercion of the first expression into the type of the second one. | *) |
| |
PLupdate of |
(* | functional update of the field of a structure. | *) |
| |
PLinitIndex of |
(* | array constructor. | *) |
| |
PLinitField of |
(* | struct/union constructor. | *) |
| |
PLtypeof of |
(* | type tag for an expression. | *) |
| |
PLtype of |
(* | type tag for a C type. | *) |
| |
PLfalse |
(* | false (either as a term or a predicate. | *) |
| |
PLtrue |
(* | true (either as a term or a predicate. | *) |
| |
PLrel of |
(* | comparison operator. | *) |
| |
PLand of |
(* | conjunction. | *) |
| |
PLor of |
(* | disjunction. | *) |
| |
PLxor of |
(* | logical xor. | *) |
| |
PLimplies of |
(* | implication. | *) |
| |
PLiff of |
(* | equivalence. | *) |
| |
PLnot of |
(* | negation. | *) |
| |
PLif of |
(* | conditional operator. | *) |
| |
PLforall of |
(* | universal quantification. | *) |
| |
PLexists of |
(* | existential quantification. | *) |
| |
PLbase_addr of |
(* | base address of a pointer. | *) |
| |
PLoffset of |
(* | base address of a pointer. | *) |
| |
PLblock_length of |
(* | length of the block pointed to by an expression. | *) |
| |
PLvalid of |
(* | pointer is valid. | *) |
| |
PLvalid_read of |
(* | pointer is valid for reading. | *) |
| |
PLallocable of |
(* | pointer is valid for malloc. | *) |
| |
PLfreeable of |
(* | pointer is valid for free. | *) |
| |
PLinitialized of |
(* | l-value is guaranteed to be initalized | *) |
| |
PLfresh of |
(* | expression points to a newly allocated block. | *) |
| |
PLseparated of |
(* | separation predicate. | *) |
| |
PLnamed of |
(* | named expression. | *) |
| |
PLsubtype of |
(* | first type tag is a subtype of second one. | *) |
| |
PLcomprehension of |
(* | set of expression defined in comprehension () | *) |
| |
PLsingleton of |
(* | singleton sets. | *) |
| |
PLunion of |
(* | union of sets. | *) |
| |
PLinter of |
(* | intersection of sets. | *) |
| |
PLempty |
(* | empty set. | *) |
type
type_annot = {
|
inv_name : |
|||
|
this_type : |
|||
|
this_name : |
(* | name of its argument. | *) |
|
inv : |
type
model_annot = {
|
model_for_type : |
|||
|
model_type : |
|||
|
model_name : |
(* | name of the model field. | *) |
type
typedef =
| |
TDsum of |
(* | sum type, list of constructors | *) |
| |
TDsyn of |
(* | synonym of an existing type | *) |
type
decl = {
|
decl_node : |
(* | kind of declaration. | *) |
|
decl_loc : |
(* | position in the source code. | *) |
type
decl_node =
| |
LDlogic_def of |
(* | LDlogic_def(name,labels,type_params,
return_type, parameters, definition)
represents the definition of a logic function name whose
return type is return_type and arguments are parameters .
Its label arguments are labels . Polymorphic functions have
their type parameters in type_params . definition is the
body of the defined function. | *) |
| |
LDlogic_reads of |
(* | LDlogic_reads(name,labels,type_params,
return_type, parameters, reads_tsets) represents the declaration
of logic function. It has the same
arguments as LDlogic_def , except that the definition is
abstracted to a set of read accesses in read_tsets . | *) |
| |
LDtype of |
(* | new logic type and its parameters, optionally followed by its definition. | *) |
| |
LDpredicate_reads of |
(* | LDpredicate_reads(name,labels,type_params,
parameters, reads_tsets)
represents the declaration of a new predicate. It is similar to
LDlogic_reads except that it has no return_type . | *) |
| |
LDpredicate_def of |
(* | LDpredicate_def(name,labels,type_params, parameters, def)
represents the definition of a new predicate. It is similar to
LDlogic_def except that it has no return_type . | *) |
| |
LDinductive_def of |
(* | LDinductive_def(name,labels,type_params, parameters, indcases)
represents an inductive definition of a new predicate. | *) |
| |
LDlemma of |
(* | LDlemma(name,is_axiom,labels,type_params,property) represents
a lemma or an axiom name .
is_axiom is true for an axiom and false for a lemma. labels
is the list of label arguments and
type_params the list of type parameters. Last, property is the
statement of the lemma. | *) |
| |
LDaxiomatic of |
(* | LDaxiomatic(id,decls)
represents a block of axiomatic definitions. | *) |
| |
LDinvariant of |
(* | global invariant. | *) |
| |
LDtype_annot of |
(* | type invariant. | *) |
| |
LDmodel_annot of |
(* | model field. | *) |
| |
LDvolatile of |
(* | volatile clause read/write. | *) |
typedeps =
lexpr Cil_types.deps
typespec =
(lexpr, lexpr, lexpr) Cil_types.spec
typecode_annot =
(lexpr, lexpr, lexpr, lexpr)
Cil_types.code_annot
typeassigns =
lexpr Cil_types.assigns
typevariant =
lexpr Cil_types.variant
type
custom_tree =
| |
CustomType of |
| |
CustomLexpr of |
| |
CustomOther of |
type
annot =
| |
Adecl of |
(* | global annotation. | *) |
| |
Aspec |
|||
| |
Acode_annot of |
(* | code annotation. | *) |
| |
Aloop_annot of |
(* | loop annotation. | *) |
| |
Aattribute_annot of |
(* | attribute annotation. | *) |
| |
Acustom of |
type
ext_decl =
| |
Ext_decl of |
| |
Ext_macro of |
| |
Ext_include of |
type
ext_function =
| |
Ext_spec of |
| |
Ext_loop_spec of |
| |
Ext_stmt_spec of |
| |
Ext_glob of |
typeext_module =
string * ext_decl list *
((string * Cil_types.location) * ext_function list) list
typeext_spec =
ext_module list