Module 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

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 = 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_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.

*)
| 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 string * lexpr list
| Ext_extension of string * string * extended_decl list
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.

Pragmas for the value analysis plugin of Frama-C.

type loop_pragma =
| Unroll_specs of lexpr list
| Widen_hints of lexpr list
| Widen_variables of lexpr list
and slice_pragma =
| SPexpr of lexpr
| SPctrl
| SPstmt

Pragmas for the slicing plugin of Frama-C.

and impact_pragma =
| IPexpr of lexpr
| IPstmt

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 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.
*)
| APragma of pragma(*

pragma.

*)
| 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