Module Logic_ptree

module Logic_ptree: sig .. end

logic constants.


type constant = 
| IntConstant of string (*

integer constant

*)
| FloatConstant of string (*

real constant

*)
| StringConstant of string (*

string constant

*)
| WStringConstant of string (*

wide string constant

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

type path_elt = 
| PLpathField of string
| PLpathIndex of lexpr

kind of expression.

type update_term = 
| PLupdateTerm of lexpr
| PLupdateCont of (path_elt list * update_term) list
type 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.

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

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

*)
type deps = 
| From of lexpr list (*

tsets. Empty list means \nothing.

*)
| FromAny (*

Nothing specified. Any location can be involved.

*)

dependencies of an assigned location.

type from = lexpr * deps 
type 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.

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

type variant = lexpr * string option 

variant of a loop or a recursive function.

type global_extension = 
| Ext_lexpr of string * lexpr list
| Ext_extension of string * string * extended_decl list
type 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
type slice_pragma = 
| SPexpr of lexpr
| SPctrl
| SPstmt

Pragmas for the slicing plugin of Frama-C.

type impact_pragma = 
| IPexpr of lexpr
| IPstmt

Pragmas for the impact plugin of Frama-C.

type 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
  • Change in 18.0-Argon
*)

all annotations that can be found in the code. This type shares the name of its constructors with Cil_types.code_annotation_node.

custom trees

type custom_tree = 
| CustomType of logic_type
| CustomLexpr of lexpr
| CustomOther of string * custom_tree list
type annot = 
| Adecl of decl list (*

global annotation.

*)
| Aspec
| Acode_annot of location * code_annot (*

code annotation.

*)
| Aloop_annot of location * code_annot list (*

loop annotation.

*)
| Aattribute_annot of location * string (*

attribute annotation.

*)
| Acustom of location * string * custom_tree

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