package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct