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
array_size =
| |
ASinteger of |
(* |
integer constant
| *) |
| |
ASidentifier of |
(* |
a variable or macro
| *) |
| |
ASnone |
(* |
none
| *) |
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 |
typelocation =
Cil_types.location
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.
| *) |
| |
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.
| *) |
| |
PLobject_pointer of |
(* |
object pointer can be created.
| *) |
| |
PLvalid_function of |
(* |
function pointer is compatible with pointed type.
| *) |
| |
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.
| *) |
| |
PLcomprehension of |
(* |
set of expression defined in comprehension
()
| *) |
| |
PLset of |
(* |
sets of elements.
| *) |
| |
PLunion of |
(* |
union of sets.
| *) |
| |
PLinter of |
(* |
intersection of sets.
| *) |
| |
PLempty |
(* |
empty set.
| *) |
| |
PLlist of |
(* |
list of elements.
| *) |
| |
PLrepeat of |
(* |
repeat a list of elements a number of times.
| *) |
typeextension =
string * lexpr list
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,
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, 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,
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.
| *) |
| |
LDextended of |
(* |
extended global annotation.
| *) |
type
deps =
| |
From of |
(* |
tsets. Empty list means \nothing.
| *) |
| |
FromAny |
(* |
Nothing specified. Any location can be involved.
| *) |
typefrom =
lexpr * deps
type
assigns =
| |
WritesAny |
(* |
Nothing specified. Anything can be written.
| *) |
| |
Writes of |
(* |
list of locations that can be written. Empty list means \nothing.
| *) |
type
allocation =
| |
FreeAlloc of |
(* |
tsets. Empty list means \nothing.
| *) |
| |
FreeAllocAny |
(* |
Nothing specified. Semantics depends on where it
is written.
| *) |
typevariant =
lexpr * string option
type
behavior = {
|
mutable b_name : |
(* |
name of the behavior.
| *) |
|
mutable b_requires : |
(* |
require clauses.
| *) |
|
mutable b_assumes : |
(* |
assume clauses.
| *) |
|
mutable b_post_cond : |
(* |
post-condition.
| *) |
|
mutable b_assigns : |
(* |
assignments.
| *) |
|
mutable b_allocation : |
(* |
frees, allocates.
| *) |
|
mutable b_extended : |
(* |
extensions
| *) |
Cil_types.behavior
.type
spec = {
|
mutable spec_behavior : |
(* |
behaviors
| *) |
|
mutable spec_variant : |
(* |
variant for recursive functions.
| *) |
|
mutable spec_terminates : |
(* |
termination condition.
| *) |
|
mutable spec_complete_behaviors : |
(* |
list of complete behaviors.
It is possible to have more than one set of complete behaviors
| *) |
|
mutable spec_disjoint_behaviors : |
(* |
list of disjoint behaviors.
It is possible to have more than one set of disjoint behaviors
| *) |
Cil_types.spec
.type
loop_pragma =
| |
Unroll_specs of |
| |
Widen_hints of |
| |
Widen_variables of |
type
slice_pragma =
| |
SPexpr of |
| |
SPctrl |
| |
SPstmt |
type
impact_pragma =
| |
IPexpr of |
| |
IPstmt |
type
pragma =
| |
Loop_pragma of |
| |
Slice_pragma of |
| |
Impact_pragma of |
type
assertion_kind =
| |
Assert |
| |
Check |
type
code_annot =
| |
AAssert of |
(* |
assertion to be checked. The list of strings is the list of
behaviors to which this assertion applies.
| *) |
| |
AStmtSpec of |
(* |
statement contract
(potentially restricted to some enclosing behaviors).
| *) |
| |
AInvariant of |
(* |
loop/code invariant. The list of strings is the list of behaviors to which
this invariant applies. The boolean flag is true for normal loop
invariants and false for invariant-as-assertions.
| *) |
| |
AVariant of |
(* |
loop variant. Note that there can be at most one variant associated to a
given statement
| *) |
| |
AAssigns of |
(* |
loop assigns. (see
b_assigns in the behaviors for other assigns). At
most one clause associated to a given (statement, behavior) couple. | *) |
| |
AAllocation of |
(* |
loop allocation clause. (see
b_allocation in the behaviors for other
allocation clauses).
At most one clause associated to a given (statement, behavior) couple.Since Oxygen-20120901 when [b_allocation] has been added. | *) |
| |
APragma of |
(* |
pragma.
| *) |
| |
AExtended of |
(* |
extension in a code or loop (when boolean flag is true) annotation.
Since Silicon-20161101 Change in 18.0-Argon | *) |
Cil_types.code_annotation_node
.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_stmt of |
| |
Ext_glob of |
typeext_module =
string option * ext_decl list *
((string * location) option * ext_function list) list
typeext_spec =
ext_module list