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 |
|||
| |
LTattribute 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 |
(* |
pointer is guaranteed to be
initialized
| *) |
| |
PLdangling of |
(* |
pointer is guaranteed to be
dangling
| *) |
| |
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