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
*)
logic constants.
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 * constant option (*
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 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 : Cil_types.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.
*)
| PLcoercion of lexpr * logic_type (*
coercion of an expression in a given type.
*)
| PLcoercionE of lexpr * lexpr (*
coercion of the first expression into the type of the second one.
*)
| 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.
*)
| 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.
*)
| PLsubtype of lexpr * lexpr (*
first type tag is a subtype of second one.
*)
| PLcomprehension of lexpr * quantifiers * lexpr option (*
set of expression defined in comprehension ()
*)
| PLsingleton of lexpr (*
singleton sets.
*)
| PLunion of lexpr list (*
union of sets.
*)
| PLinter of lexpr list (*
intersection of sets.
*)
| PLempty (*
empty set.
*)
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 : Cil_types.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 * bool * string list * string list * lexpr (*
LDlemma(name,is_axiom,labels,type_params,property) represents a lemma or an axiom name. is_axiom is true for an axiom and false for a lemma. 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.
*)
type deps = lexpr Cil_types.deps 
C locations.
type spec = (lexpr, lexpr, lexpr) Cil_types.spec 
specification of a C function.
type code_annot = (lexpr, lexpr, lexpr, lexpr)
Cil_types.code_annot
type assigns = lexpr Cil_types.assigns 
assignment performed by a C function.
type variant = lexpr Cil_types.variant 
variant for loop or recursive function.

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 Cil_types.location * code_annot (*
code annotation.
*)
| Aloop_annot of Cil_types.location * code_annot list (*
loop annotation.
*)
| Aattribute_annot of Cil_types.location * string (*
attribute annotation.
*)
| Acustom of Cil_types.location * string * custom_tree
all kind of annotations
type ext_decl = 
| Ext_decl of decl
| Ext_macro of string * lexpr
| Ext_include of bool * string * Cil_types.location
ACSL extension for external spec file *
type ext_function = 
| Ext_spec of spec * Cil_types.location
| Ext_loop_spec of string * annot * Cil_types.location
| Ext_stmt_spec of string * annot * Cil_types.location
| Ext_glob of ext_decl
type ext_module = string * ext_decl list *
((string * Cil_types.location) * ext_function list) list
type ext_spec = ext_module list