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
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 (*l-value is guaranteed to be initalized*)
| 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