Frama-C API - `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
*)
| LTboolean
(*
booleans
*)
| 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

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 : 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.

and path_elt =

| PLpathField of string
| PLpathIndex of lexpr

construct inside a functional update.

and update_term =

| PLupdateTerm of lexpr
| PLupdateCont of (path_elt list * update_term) list

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 (a.x)
*)
| PLarrow of lexpr * string
(*
field access (a->x)
*)
| 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 ({ e | integer i; P(i)})
*)
| 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 toplevel_predicate = {

tp_kind : Cil_types.predicate_kind;
tp_statement : lexpr;

}

type extension = {

ext_name : string;
ext_plugin : string;
ext_content : lexpr list;

}

ACSL extension.

before 30.0-Zinc
Was of type 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 loader = {

loader_name : string;
loader_plugin : string;

}

loader type used by module importers.

since 30.0-Zinc

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_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 string * string list * string list * logic_type * (logic_type * string) list * lexpr list option
(*
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 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_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 string * string list * string list * (logic_type * string) list * lexpr
(*
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 string * string list * string list * (logic_type * string) list * (string * string list * string list * lexpr) list
(*
LDinductive_def(name,labels,type_params, parameters, indcases) represents an inductive definition of a new predicate.
*)
| 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. 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 string * decl list
(*
LDaxiomatic(id,decls) represents a block of axiomatic definitions.
*)
| LDmodule of string * decl list
(*
LDmodule(id,decls) represents a module of axiomatic definitions.
*)
| LDimport of {
1. import_loader : loader option;
2. module_name : string;
3. module_alias : string option;
}
(*
LDimport(loader,module,alias) imports symbols from module using the specified loader, with optional alias.
*)
| 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 from = lexpr * deps

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.

since Oxygen-20120901

and variant = lexpr * string option

variant of a loop or a recursive function.

and global_extension =

| Ext_lexpr of extension
(*
- before 30.0-Zinc
  Was of type string * lexpr list.
*)
| Ext_extension of {
1. gext_name : string;
2. gext_plugin : string;
3. gext_kind : string;
4. gext_content : extended_decl list;
}
(*
- before 30.0-Zinc
  Was of type string * string * extended_decl list.
*)

Global ACSL extension.

and extended_decl = {

extended_node : global_extension;
extended_loc : location;

}

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.

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 b_assigns in the behaviors for other assigns). At most one clause associated to a given (statement, behavior) couple.
*)
| AAllocation of string list * allocation
(*
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.
*)
| AExtended of string list * bool * extension
(*
extension in a code or loop (when boolean flag is true) annotation.
- since Silicon-20161101
*)

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_function =

| Ext_spec of spec * location
| Ext_stmt of string list * annot * location
| Ext_glob of ext_decl

type ext_module = string option * ext_decl list * ((string * location) option * ext_function list) list

type ext_spec = ext_module list

Frama-C API - Logic_ptree

Frama-C API - `Logic_ptree`