package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Common Types and Signatures

General Definitions

type 'a sequence = {
  1. pre : 'a;
  2. post : 'a;
}
type 'a binder = {
  1. bind : 'b 'c. 'a -> ('b -> 'c) -> 'b -> 'c;
}
type equation =
  1. | Set of Lang.F.term * Lang.F.term
    (*

    Set(a,b) is a := b.

    *)
  2. | Assert of Lang.F.pred

Oriented equality or arbitrary relation

type acs =
  1. | RW
    (*

    Read-Write Access

    *)
  2. | RD
    (*

    Read-Only Access

    *)
  3. | OBJ
    (*

    Valid Object Pointer

    *)

Access conditions

type 'a value =
  1. | Val of Lang.F.term
  2. | Loc of 'a

Abstract location or concrete value

type 'a rloc =
  1. | Rloc of Ctypes.c_object * 'a
  2. | Rrange of 'a * Ctypes.c_object * Lang.F.term option * Lang.F.term option

Contiguous set of locations

type 'a sloc =
  1. | Sloc of 'a
  2. | Sarray of 'a * Ctypes.c_object * int
    (*

    full sized range (optimized assigns)

    *)
  3. | Srange of 'a * Ctypes.c_object * Lang.F.term option * Lang.F.term option
  4. | Sdescr of Lang.F.var list * 'a * Lang.F.pred

Structured set of locations

type 'a region = (Ctypes.c_object * 'a sloc) list

Typed set of locations

type 'a logic =
  1. | Vexp of Lang.F.term
  2. | Vloc of 'a
  3. | Lset of 'a sloc list

Logical values, locations, or sets of

type scope =
  1. | Enter
  2. | Leave

Scope management for locals and formals

type 'a result =
  1. | R_loc of 'a
  2. | R_var of Lang.F.var

Container for the returned value of a function

type polarity = [
  1. | `Positive
  2. | `Negative
  3. | `NoPolarity
]

Polarity of predicate compilation

type frame = string * Definitions.trigger list * Lang.F.pred list * Lang.F.term * Lang.F.term

Frame Conditions. Consider a function phi(m) over memory m, we want memories m1,m2 and condition p such that p(m1,m2) -> phi(m1) = phi(m2).

  • name used for generating lemma
  • triggers for the lemma
  • conditions for the frame lemma to hold
  • mem1,mem2 to two memories for which the lemma holds

Reversing Models

It is sometimes possible to reverse memory models abstractions into ACSL left-values via the definitions below.

type s_lval = s_host * s_offset list

Reversed ACSL left-value

and s_host =
  1. | Mvar of Frama_c_kernel.Cil_types.varinfo
    (*

    Variable

    *)
  2. | Mmem of Lang.F.term
    (*

    Pointed value

    *)
  3. | Mval of s_lval
    (*

    Pointed value of another abstract left-value

    *)
and s_offset =
  1. | Mfield of Frama_c_kernel.Cil_types.fieldinfo
  2. | Mindex of Lang.F.term
type mval =
  1. | Mterm
    (*

    Not a state-related value

    *)
  2. | Maddr of s_lval
    (*

    The value is the address of an l-value in current memory

    *)
  3. | Mlval of s_lval * Lang.datakind
    (*

    The value is the value of an l-value in current memory

    *)
  4. | Mchunk of string * Lang.datakind
    (*

    The value is an abstract memory chunk (description)

    *)

Reversed abstract value

type update =
  1. | Mstore of s_lval * Lang.F.term
    (*

    An update of the ACSL left-value with the given value

    *)

Reversed update

Memory Models

module type Chunk = sig ... end

Memory Chunks.

module type Sigma = sig ... end

Memory Environments.

module type Model = sig ... end

Memory Models.

C and ACSL Compilers

module type CodeSemantics = sig ... end

Compiler for C expressions

module type LogicSemantics = sig ... end

Compiler for ACSL expressions

module type LogicAssigns = sig ... end

Compiler for Performing Assigns

module type Compiler = sig ... end

All Compilers Together

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