Frama_c_kernel.Logic_ptree
type constant =
| IntConstant of string | (* integer constant *) |
| FloatConstant of string | (* real constant *) |
| StringConstant of string | (* string constant *) |
| WStringConstant of string | (* wide string constant *) |
logic constants.
type array_size =
| ASinteger of string | (* integer constant *) |
| ASidentifier of string | (* a variable or macro *) |
| ASnone | (* none *) |
size of logic array.
type logic_type =
| LTvoid | (* C void *) |
| LTinteger | (* mathematical integers. *) |
| LTreal | (* mathematical real. *) |
| LTint of Cil_types.ikind | (* C integral type. *) |
| LTfloat of Cil_types.fkind | (* C floating-point type *) |
| LTarray of logic_type * array_size | (* C array *) |
| LTpointer of logic_type | (* C pointer *) |
| LTenum of string | (* C enum *) |
| LTstruct of string | (* C struct *) |
| LTunion of string | (* C union *) |
| LTnamed of string * logic_type list | (* declared logic type. *) |
| LTarrow of logic_type list * logic_type | |
| LTattribute of logic_type * Cil_types.attribute |
logic types.
type location = Cil_types.location
type quantifiers = (logic_type * string) list
quantifier-bound variables
arithmetic and logic binary operators.
type lexpr = {
lexpr_node : lexpr_node; | (* kind of expression. *) |
lexpr_loc : location; | (* position in the source code. *) |
}
logical expression. The distinction between locations, terms and predicate is done during typing.
construct inside a functional update.
and lexpr_node =
| PLvar of string | (* a variable *) |
| PLapp of string * string list * lexpr list | (* an application. *) |
| PLlambda of quantifiers * lexpr | (* a lambda abstraction. *) |
| PLlet of string * lexpr * lexpr | (* local binding. *) |
| PLconstant of constant | (* a constant. *) |
| PLunop of unop * lexpr | (* unary operator. *) |
| PLbinop of lexpr * binop * lexpr | (* binary operator. *) |
| PLdot of lexpr * string | (* field access ( |
| PLarrow of lexpr * string | (* field access ( |
| PLarrget of lexpr * lexpr | (* array access. *) |
| PLold of lexpr | (* expression refers to pre-state of a function. *) |
| PLat of lexpr * string | (* expression refers to a given program point. *) |
| PLresult | (* value returned by a function. *) |
| PLnull | (* null pointer. *) |
| PLcast of logic_type * lexpr | (* cast. *) |
| PLrange of lexpr option * lexpr option | (* interval of integers. *) |
| PLsizeof of logic_type | (* sizeof a type. *) |
| PLsizeofE of lexpr | (* sizeof the type of an expression. *) |
| PLupdate of lexpr * path_elt list * update_term | (* functional update of the field of a structure. *) |
| PLinitIndex of (lexpr * lexpr) list | (* array constructor. *) |
| PLinitField of (string * lexpr) list | (* struct/union constructor. *) |
| PLtypeof of lexpr | (* type tag for an expression. *) |
| PLtype of logic_type | (* 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 lexpr * relation * lexpr | (* comparison operator. *) |
| PLand of lexpr * lexpr | (* conjunction. *) |
| PLor of lexpr * lexpr | (* disjunction. *) |
| PLxor of lexpr * lexpr | (* logical xor. *) |
| PLimplies of lexpr * lexpr | (* implication. *) |
| PLiff of lexpr * lexpr | (* equivalence. *) |
| PLnot of lexpr | (* negation. *) |
| PLif of lexpr * lexpr * lexpr | (* conditional operator. *) |
| PLforall of quantifiers * lexpr | (* universal quantification. *) |
| PLexists of quantifiers * lexpr | (* existential quantification. *) |
| PLbase_addr of string option * lexpr | (* base address of a pointer. *) |
| PLoffset of string option * lexpr | (* base address of a pointer. *) |
| PLblock_length of string option * lexpr | (* length of the block pointed to by an expression. *) |
| PLvalid of string option * lexpr | (* pointer is valid. *) |
| PLvalid_read of string option * lexpr | (* pointer is valid for reading. *) |
| PLobject_pointer of string option * lexpr | (* object pointer can be created. *) |
| PLvalid_function of lexpr | (* function pointer is compatible with pointed type. *) |
| PLallocable of string option * lexpr | (* pointer is valid for malloc. *) |
| PLfreeable of string option * lexpr | (* pointer is valid for free. *) |
| PLinitialized of string option * lexpr | (* pointer is guaranteed to be initialized *) |
| PLdangling of string option * lexpr | (* pointer is guaranteed to be dangling *) |
| PLfresh of (string * string) option * lexpr * lexpr | (* expression points to a newly allocated block. *) |
| PLseparated of lexpr list | (* separation predicate. *) |
| PLnamed of string * lexpr | (* named expression. *) |
| PLcomprehension of lexpr * quantifiers * lexpr option | (* set of expression defined in comprehension ( |
| PLset of lexpr list | (* sets of elements. *) |
| PLunion of lexpr list | (* union of sets. *) |
| PLinter of lexpr list | (* intersection of sets. *) |
| PLempty | (* empty set. *) |
| PLlist of lexpr list | (* list of elements. *) |
| PLrepeat of lexpr * lexpr | (* repeat a list of elements a number of times. *) |
Kind of expression
type extension = string * lexpr list
type type_annot = {
inv_name : string; | |
this_type : logic_type; | |
this_name : string; | (* name of its argument. *) |
inv : lexpr; |
}
type invariant.
type model_annot = {
model_for_type : logic_type; | |
model_type : logic_type; | |
model_name : string; | (* name of the model field. *) |
}
model field.
type typedef =
| TDsum of (string * logic_type list) list | (* sum type, list of constructors *) |
| TDsyn of logic_type | (* synonym of an existing type *) |
Concrete type definition.
type decl = {
decl_node : decl_node; | (* kind of declaration. *) |
decl_loc : location; | (* position in the source code. *) |
}
global declarations.
and decl_node =
| LDlogic_def of string
* string list
* string list
* logic_type
* (logic_type * string) list
* lexpr | (*
|
| LDlogic_reads of string
* string list
* string list
* logic_type
* (logic_type * string) list
* lexpr list option | (*
|
| LDtype of string * string list * typedef option | (* new logic type and its parameters, optionally followed by its definition. *) |
| LDpredicate_reads of string
* string list
* string list
* (logic_type * string) list
* lexpr list option | (*
|
| LDpredicate_def of string
* string list
* string list
* (logic_type * string) list
* lexpr | (*
|
| LDinductive_def of string
* string list
* string list
* (logic_type * string) list
* (string * string list * string list * lexpr) list | (*
|
| LDlemma of string * string list * string list * toplevel_predicate | (* LDlemma(name,labels,type_params,property) represents axioms and lemmas. Axioms and admit lemmas are fusionned. |
| LDaxiomatic of string * decl list | (*
|
| LDinvariant of string * lexpr | (* global invariant. *) |
| LDtype_annot of type_annot | (* type invariant. *) |
| LDmodel_annot of model_annot | (* model field. *) |
| LDvolatile of lexpr list * string option * string option | (* volatile clause read/write. *) |
| LDextended of global_extension | (* extended global annotation. *) |
and deps =
| From of lexpr list | (* tsets. Empty list means \nothing. *) |
| FromAny | (* Nothing specified. Any location can be involved. *) |
dependencies of an assigned location.
and assigns =
| WritesAny | (* Nothing specified. Anything can be written. *) |
| Writes of from list | (* list of locations that can be written. Empty list means \nothing. *) |
zone assigned with its dependencies.
and allocation =
| FreeAlloc of lexpr list * lexpr list | (* tsets. Empty list means \nothing. *) |
| FreeAllocAny | (* Nothing specified. Semantics depends on where it is written. *) |
allocates and frees.
and variant = lexpr * string option
variant of a loop or a recursive function.
and global_extension =
| Ext_lexpr of string * lexpr list |
| Ext_extension of string * string * extended_decl list |
type behavior = {
mutable b_name : string; | (* name of the behavior. *) |
mutable b_requires : toplevel_predicate list; | (* require clauses. *) |
mutable b_assumes : lexpr list; | (* assume clauses. *) |
mutable b_post_cond : (Cil_types.termination_kind * toplevel_predicate) list; | (* post-condition. *) |
mutable b_assigns : assigns; | (* assignments. *) |
mutable b_allocation : allocation; | (* frees, allocates. *) |
mutable b_extended : extension list; | (* extensions *) |
}
Behavior in a specification. This type shares the name of its constructors with Cil_types.behavior
.
type spec = {
mutable spec_behavior : behavior list; | (* behaviors *) |
mutable spec_variant : variant option; | (* variant for recursive functions. *) |
mutable spec_terminates : lexpr option; | (* termination condition. *) |
mutable spec_complete_behaviors : string list list; | (* list of complete behaviors. It is possible to have more than one set of complete behaviors *) |
mutable spec_disjoint_behaviors : string list list; | (* 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.
Pragmas for the slicing plugin of Frama-C.
Pragmas for the impact plugin of Frama-C.
and pragma =
| Loop_pragma of loop_pragma |
| Slice_pragma of slice_pragma |
| Impact_pragma of impact_pragma |
The various kinds of pragmas.
type code_annot =
| AAssert of string list * toplevel_predicate | (* assertion to be checked. The list of strings is the list of behaviors to which this assertion applies. *) |
| AStmtSpec of string list * spec | (* statement contract (potentially restricted to some enclosing behaviors). *) |
| AInvariant of string list * bool * toplevel_predicate | (* 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 variant | (* loop variant. Note that there can be at most one variant associated to a given statement *) |
| AAssigns of string list * assigns | (* loop assigns. (see |
| AAllocation of string list * allocation | (* loop allocation clause. (see |
| APragma of pragma | (* pragma. *) |
| AExtended of string list * bool * extension | (* 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 decl list | (* global annotation. *) |
| Aspec | (* function specification. *) |
| Acode_annot of location * code_annot | (* code annotation. *) |
| Aloop_annot of location * code_annot list | (* loop annotation. *) |
| Aattribute_annot of location * string | (* attribute annotation. *) |
all kind of annotations
type ext_decl =
| Ext_decl of decl |
| Ext_macro of bool * string * lexpr |
| Ext_include of bool * string * location |
ACSL extension for external spec file *
type ext_module =
string option
* ext_decl list
* ((string * location) option * ext_function list) list
type ext_spec = ext_module list