Module Frama_c_kernel.Logic_ptree

type constant =
  1. | IntConstant of string
    (*

    integer constant

    *)
  2. | FloatConstant of string
    (*

    real constant

    *)
  3. | StringConstant of string
    (*

    string constant

    *)
  4. | WStringConstant of string
    (*

    wide string constant

    *)

logic constants.

type array_size =
  1. | ASinteger of string
    (*

    integer constant

    *)
  2. | ASidentifier of string
    (*

    a variable or macro

    *)
  3. | ASnone
    (*

    none

    *)

size of logic array.

type logic_type =
  1. | LTvoid
    (*

    C void

    *)
  2. | LTinteger
    (*

    mathematical integers.

    *)
  3. | LTreal
    (*

    mathematical real.

    *)
  4. | LTint of Cil_types.ikind
    (*

    C integral type.

    *)
  5. | LTfloat of Cil_types.fkind
    (*

    C floating-point type

    *)
  6. | LTarray of logic_type * array_size
    (*

    C array

    *)
  7. | LTpointer of logic_type
    (*

    C pointer

    *)
  8. | LTenum of string
    (*

    C enum

    *)
  9. | LTstruct of string
    (*

    C struct

    *)
  10. | LTunion of string
    (*

    C union

    *)
  11. | LTnamed of string * logic_type list
    (*

    declared logic type.

    *)
  12. | LTarrow of logic_type list * logic_type
  13. | 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 =
  1. | Lt
  2. | Gt
  3. | Le
  4. | Ge
  5. | Eq
  6. | Neq

comparison operators.

type binop =
  1. | Badd
  2. | Bsub
  3. | Bmul
  4. | Bdiv
  5. | Bmod
  6. | Bbw_and
  7. | Bbw_or
  8. | Bbw_xor
  9. | Blshift
  10. | Brshift

arithmetic and logic binary operators.

type unop =
  1. | Uminus
  2. | Ustar
  3. | Uamp
  4. | Ubw_not

unary operators.

type lexpr = {
  1. lexpr_node : lexpr_node;
    (*

    kind of expression.

    *)
  2. lexpr_loc : location;
    (*

    position in the source code.

    *)
}

logical expression. The distinction between locations, terms and predicate is done during typing.

and path_elt =
  1. | PLpathField of string
  2. | PLpathIndex of lexpr

construct inside a functional update.

and update_term =
  1. | PLupdateTerm of lexpr
  2. | PLupdateCont of (path_elt list * update_term) list
and lexpr_node =
  1. | PLvar of string
    (*

    a variable

    *)
  2. | PLapp of string * string list * lexpr list
    (*

    an application.

    *)
  3. | PLlambda of quantifiers * lexpr
    (*

    a lambda abstraction.

    *)
  4. | PLlet of string * lexpr * lexpr
    (*

    local binding.

    *)
  5. | PLconstant of constant
    (*

    a constant.

    *)
  6. | PLunop of unop * lexpr
    (*

    unary operator.

    *)
  7. | PLbinop of lexpr * binop * lexpr
    (*

    binary operator.

    *)
  8. | PLdot of lexpr * string
    (*

    field access (a.x)

    *)
  9. | PLarrow of lexpr * string
    (*

    field access (a->x)

    *)
  10. | PLarrget of lexpr * lexpr
    (*

    array access.

    *)
  11. | PLold of lexpr
    (*

    expression refers to pre-state of a function.

    *)
  12. | PLat of lexpr * string
    (*

    expression refers to a given program point.

    *)
  13. | PLresult
    (*

    value returned by a function.

    *)
  14. | PLnull
    (*

    null pointer.

    *)
  15. | PLcast of logic_type * lexpr
    (*

    cast.

    *)
  16. | PLrange of lexpr option * lexpr option
    (*

    interval of integers.

    *)
  17. | PLsizeof of logic_type
    (*

    sizeof a type.

    *)
  18. | PLsizeofE of lexpr
    (*

    sizeof the type of an expression.

    *)
  19. | PLupdate of lexpr * path_elt list * update_term
    (*

    functional update of the field of a structure.

    *)
  20. | PLinitIndex of (lexpr * lexpr) list
    (*

    array constructor.

    *)
  21. | PLinitField of (string * lexpr) list
    (*

    struct/union constructor.

    *)
  22. | PLtypeof of lexpr
    (*

    type tag for an expression.

    *)
  23. | PLtype of logic_type
    (*

    type tag for a C type.

    *)
  24. | PLfalse
    (*

    false (either as a term or a predicate.

    *)
  25. | PLtrue
    (*

    true (either as a term or a predicate.

    *)
  26. | PLrel of lexpr * relation * lexpr
    (*

    comparison operator.

    *)
  27. | PLand of lexpr * lexpr
    (*

    conjunction.

    *)
  28. | PLor of lexpr * lexpr
    (*

    disjunction.

    *)
  29. | PLxor of lexpr * lexpr
    (*

    logical xor.

    *)
  30. | PLimplies of lexpr * lexpr
    (*

    implication.

    *)
  31. | PLiff of lexpr * lexpr
    (*

    equivalence.

    *)
  32. | PLnot of lexpr
    (*

    negation.

    *)
  33. | PLif of lexpr * lexpr * lexpr
    (*

    conditional operator.

    *)
  34. | PLforall of quantifiers * lexpr
    (*

    universal quantification.

    *)
  35. | PLexists of quantifiers * lexpr
    (*

    existential quantification.

    *)
  36. | PLbase_addr of string option * lexpr
    (*

    base address of a pointer.

    *)
  37. | PLoffset of string option * lexpr
    (*

    base address of a pointer.

    *)
  38. | PLblock_length of string option * lexpr
    (*

    length of the block pointed to by an expression.

    *)
  39. | PLvalid of string option * lexpr
    (*

    pointer is valid.

    *)
  40. | PLvalid_read of string option * lexpr
    (*

    pointer is valid for reading.

    *)
  41. | PLobject_pointer of string option * lexpr
    (*

    object pointer can be created.

    *)
  42. | PLvalid_function of lexpr
    (*

    function pointer is compatible with pointed type.

    *)
  43. | PLallocable of string option * lexpr
    (*

    pointer is valid for malloc.

    *)
  44. | PLfreeable of string option * lexpr
    (*

    pointer is valid for free.

    *)
  45. | PLinitialized of string option * lexpr
    (*

    pointer is guaranteed to be initialized

    *)
  46. | PLdangling of string option * lexpr
    (*

    pointer is guaranteed to be dangling

    *)
  47. | PLfresh of (string * string) option * lexpr * lexpr
    (*

    expression points to a newly allocated block.

    *)
  48. | PLseparated of lexpr list
    (*

    separation predicate.

    *)
  49. | PLnamed of string * lexpr
    (*

    named expression.

    *)
  50. | PLcomprehension of lexpr * quantifiers * lexpr option
    (*

    set of expression defined in comprehension ({ e | integer i; P(i)})

    *)
  51. | PLset of lexpr list
    (*

    sets of elements.

    *)
  52. | PLunion of lexpr list
    (*

    union of sets.

    *)
  53. | PLinter of lexpr list
    (*

    intersection of sets.

    *)
  54. | PLempty
    (*

    empty set.

    *)
  55. | PLlist of lexpr list
    (*

    list of elements.

    *)
  56. | PLrepeat of lexpr * lexpr
    (*

    repeat a list of elements a number of times.

    *)

Kind of expression

type toplevel_predicate = {
  1. tp_kind : Cil_types.predicate_kind;
  2. tp_statement : lexpr;
}
type extension = string * lexpr list
type type_annot = {
  1. inv_name : string;
  2. this_type : logic_type;
  3. this_name : string;
    (*

    name of its argument.

    *)
  4. inv : lexpr;
}

type invariant.

type model_annot = {
  1. model_for_type : logic_type;
  2. model_type : logic_type;
  3. model_name : string;
    (*

    name of the model field.

    *)
}

model field.

type typedef =
  1. | TDsum of (string * logic_type list) list
    (*

    sum type, list of constructors

    *)
  2. | TDsyn of logic_type
    (*

    synonym of an existing type

    *)

Concrete type definition.

type decl = {
  1. decl_node : decl_node;
    (*

    kind of declaration.

    *)
  2. decl_loc : location;
    (*

    position in the source code.

    *)
}

global declarations.

and decl_node =
  1. | 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.

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

    *)
  3. | LDtype of string * string list * typedef option
    (*

    new logic type and its parameters, optionally followed by its definition.

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

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

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

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

    *)
  8. | LDaxiomatic of string * decl list
    (*

    LDaxiomatic(id,decls) represents a block of axiomatic definitions.

    *)
  9. | LDinvariant of string * lexpr
    (*

    global invariant.

    *)
  10. | LDtype_annot of type_annot
    (*

    type invariant.

    *)
  11. | LDmodel_annot of model_annot
    (*

    model field.

    *)
  12. | LDvolatile of lexpr list * string option * string option
    (*

    volatile clause read/write.

    *)
  13. | LDextended of global_extension
    (*

    extended global annotation.

    *)
and deps =
  1. | From of lexpr list
    (*

    tsets. Empty list means \nothing.

    *)
  2. | FromAny
    (*

    Nothing specified. Any location can be involved.

    *)

dependencies of an assigned location.

and from = lexpr * deps
and assigns =
  1. | WritesAny
    (*

    Nothing specified. Anything can be written.

    *)
  2. | Writes of from list
    (*

    list of locations that can be written. Empty list means \nothing.

    *)

zone assigned with its dependencies.

and allocation =
  1. | FreeAlloc of lexpr list * lexpr list
    (*

    tsets. Empty list means \nothing.

    *)
  2. | 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 =
  1. | Ext_lexpr of string * lexpr list
  2. | Ext_extension of string * string * extended_decl list
and extended_decl = {
  1. extended_node : global_extension;
  2. extended_loc : location;
}
type behavior = {
  1. mutable b_name : string;
    (*

    name of the behavior.

    *)
  2. mutable b_requires : toplevel_predicate list;
    (*

    require clauses.

    *)
  3. mutable b_assumes : lexpr list;
    (*

    assume clauses.

    *)
  4. mutable b_post_cond : (Cil_types.termination_kind * toplevel_predicate) list;
    (*

    post-condition.

    *)
  5. mutable b_assigns : assigns;
    (*

    assignments.

    *)
  6. mutable b_allocation : allocation;
    (*

    frees, allocates.

    *)
  7. mutable b_extended : extension list;
    (*

    extensions

    *)
}

Behavior in a specification. This type shares the name of its constructors with Cil_types.behavior.

type spec = {
  1. mutable spec_behavior : behavior list;
    (*

    behaviors

    *)
  2. mutable spec_variant : variant option;
    (*

    variant for recursive functions.

    *)
  3. mutable spec_terminates : lexpr option;
    (*

    termination condition.

    *)
  4. mutable spec_complete_behaviors : string list list;
    (*

    list of complete behaviors. It is possible to have more than one set of complete behaviors

    *)
  5. 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 =
  1. | Unroll_specs of lexpr list
  2. | Widen_hints of lexpr list
  3. | Widen_variables of lexpr list
and slice_pragma =
  1. | SPexpr of lexpr
  2. | SPctrl
  3. | SPstmt

Pragmas for the slicing plugin of Frama-C.

and impact_pragma =
  1. | IPexpr of lexpr
  2. | IPstmt

Pragmas for the impact plugin of Frama-C.

and pragma =
  1. | Loop_pragma of loop_pragma
  2. | Slice_pragma of slice_pragma
  3. | Impact_pragma of impact_pragma

The various kinds of pragmas.

type code_annot =
  1. | AAssert of string list * toplevel_predicate
    (*

    assertion to be checked. The list of strings is the list of behaviors to which this assertion applies.

    *)
  2. | AStmtSpec of string list * spec
    (*

    statement contract (potentially restricted to some enclosing behaviors).

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

    *)
  4. | AVariant of variant
    (*

    loop variant. Note that there can be at most one variant associated to a given statement

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

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

    pragma.

    *)
  8. | 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 =
  1. | Adecl of decl list
    (*

    global annotation.

    *)
  2. | Aspec
    (*

    function specification.

    *)
  3. | Acode_annot of location * code_annot
    (*

    code annotation.

    *)
  4. | Aloop_annot of location * code_annot list
    (*

    loop annotation.

    *)
  5. | Aattribute_annot of location * string
    (*

    attribute annotation.

    *)

all kind of annotations

type ext_decl =
  1. | Ext_decl of decl
  2. | Ext_macro of bool * string * lexpr
  3. | Ext_include of bool * string * location

ACSL extension for external spec file *

type ext_function =
  1. | Ext_spec of spec * location
  2. | Ext_stmt of string list * annot * location
  3. | 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