module Logic_ptree:sig
..end
logic constants.
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 | *) |
size of logic array.
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 |
logic types.
typelocation =
Cil_types.location
typequantifiers =
(logic_type * string) list
quantifier-bound variables
type
relation =
| |
Lt |
| |
Gt |
| |
Le |
| |
Ge |
| |
Eq |
| |
Neq |
comparison operators.
type
binop =
| |
Badd |
| |
Bsub |
| |
Bmul |
| |
Bdiv |
| |
Bmod |
| |
Bbw_and |
| |
Bbw_or |
| |
Bbw_xor |
| |
Blshift |
| |
Brshift |
arithmetic and logic binary operators.
type
unop =
| |
Uminus |
| |
Ustar |
| |
Uamp |
| |
Ubw_not |
unary operators.
type
lexpr = {
|
lexpr_node : |
(* | kind of expression. | *) |
|
lexpr_loc : |
(* | position in the source code. | *) |
}
logical expression. The distinction between locations, terms and predicate is done during typing.
type
path_elt =
| |
PLpathField of |
| |
PLpathIndex of |
construct inside a functional update.
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. | *) |
Kind of expression
type
toplevel_predicate = {
|
tp_kind : |
|
tp_statement : |
}
typeextension =
string * lexpr list
type
type_annot = {
|
inv_name : |
|||
|
this_type : |
|||
|
this_name : |
(* | name of its argument. | *) |
|
inv : |
}
type invariant.
type
model_annot = {
|
model_for_type : |
|||
|
model_type : |
|||
|
model_name : |
(* | name of the model field. | *) |
}
model field.
type
typedef =
| |
TDsum of |
(* | sum type, list of constructors | *) |
| |
TDsyn of |
(* | synonym of an existing type | *) |
Concrete type definition.
type
decl = {
|
decl_node : |
(* | kind of declaration. | *) |
|
decl_loc : |
(* | position in the source code. | *) |
}
global declarations.
type
decl_node =
| |
LDlogic_def of |
(* |
| *) |
| |
LDlogic_reads of |
(* |
| *) |
| |
LDtype of |
(* | new logic type and its parameters, optionally followed by its definition. | *) |
| |
LDpredicate_reads of |
(* |
| *) |
| |
LDpredicate_def of |
(* |
| *) |
| |
LDinductive_def of |
(* |
| *) |
| |
LDlemma of |
(* | LDlemma(name,labels,type_params,property) represents axioms and
lemmas. Axioms and admit lemmas are fusionned.
| *) |
| |
LDaxiomatic of |
(* |
| *) |
| |
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. | *) |
dependencies of an assigned location.
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. | *) |
zone assigned with its dependencies.
type
allocation =
| |
FreeAlloc of |
(* | tsets. Empty list means \nothing. | *) |
| |
FreeAllocAny |
(* | Nothing specified. Semantics depends on where it is written. | *) |
allocates and frees.
typevariant =
lexpr * string option
variant of a loop or a recursive function.
type
global_extension =
| |
Ext_lexpr of |
| |
Ext_extension of |
type
extended_decl = {
|
extended_node : |
|
extended_loc : |
}
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 | *) |
}
Behavior in a specification. This type shares the name of its constructors
with 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 | *) |
}
Function or statement contract. This type shares the name of its
constructors with Cil_types.spec
.
Pragmas for the value analysis plugin of Frama-C.
type
loop_pragma =
| |
Unroll_specs of |
| |
Widen_hints of |
| |
Widen_variables of |
type
slice_pragma =
| |
SPexpr of |
| |
SPctrl |
| |
SPstmt |
Pragmas for the slicing plugin of Frama-C.
type
impact_pragma =
| |
IPexpr of |
| |
IPstmt |
Pragmas for the impact plugin of Frama-C.
type
pragma =
| |
Loop_pragma of |
| |
Slice_pragma of |
| |
Impact_pragma of |
The various kinds of pragmas.
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 | *) |
| |
AAllocation of |
(* | loop allocation clause. (see
| *) |
| |
APragma of |
(* | pragma. | *) |
| |
AExtended of |
(* | extension in a code or loop (when boolean flag is true) annotation.
| *) |
all annotations that can be found in the code. This type shares the name of
its constructors with Cil_types.code_annotation_node
.
type
annot =
| |
Adecl of |
(* | global annotation. | *) |
| |
Aspec |
|||
| |
Acode_annot of |
(* | code annotation. | *) |
| |
Aloop_annot of |
(* | loop annotation. | *) |
| |
Aattribute_annot of |
(* | attribute annotation. | *) |
all kind of annotations
type
ext_decl =
| |
Ext_decl of |
| |
Ext_macro of |
| |
Ext_include of |
ACSL extension for external spec file *
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