package frama-c

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

Lattice signatures.

module type Join_Semi_Lattice = sig ... end
module type Bounded_Join_Semi_Lattice = sig ... end
module type With_Top = sig ... end
module type With_Top_Opt = sig ... end
module type With_Narrow = sig ... end
module type With_Under_Approximation = sig ... end

Over- and under-approximations

Nearly all abstract operations implemented in the lattices of Frama-C are *over-approximations*: the (abstract) operation assumes that its operands are already over-approximations, and returns a result that over-approximates (abstracts) the results that would have been given by the concrete operation on the concretization of the arguments.

Conversely, some functions, suffixed by _under assumes that their arguments are under-approximations, and returns a result that under-approximates the concrete operation. The functions link and meet in With_Under_Approximation are exceptions, that are not suffixed by _under.

Finally, some functions are *exact*, in the sense that they preserve the concretization of the concrete function. Hence, they implement over-approximations when given over-approximated arguments, and under-approximations when given under-approximated ones. This 'exact' property is usually mentioned in the comments for the function.

module type With_Intersects = sig ... end
module type With_Enumeration = sig ... end
module type With_Diff = sig ... end
module type With_Diff_One = sig ... end
module type With_Cardinal_One = sig ... end
module type With_Widening = sig ... end

Common signatures

module type AI_Lattice_with_cardinal_one = sig ... end

Signature shared by some functors of module Abstract_interp.

module type Full_Lattice = sig ... end

Lattice with over- and under-approximation of join and meet, and intersection and difference.

module type Full_AI_Lattice_with_cardinality = sig ... end

Most complete lattices: all operations plus widening, notion of cardinal (including enumeration) and difference.

Results of generic functors, in module Abstract_interp.

module type Lattice_Value = Datatype.S_with_collections

Generic signature for the base elements of a lattice

module type Lattice_Product = sig ... end

Signature for a product lattice in which Bottom is handled especially. (see Abstract_interp.Make_Lattice_Product).

module type Lattice_UProduct = sig ... end

Signature for a product lattice (see Abstract_interp.Make_Lattice_UProduct).

module type Lattice_Sum = sig ... end

Signature for a lattice over a sum type (see Abstract_interp.Make_Lattice_Sum).

module type Lattice_Base = sig ... end
module type Hptset = sig ... end
module type Lattice_Set = sig ... end

Signatures for a lattice over a set (see Abstract_interp.Make_Lattice_Set or Abstract_interp.Make_Hashconsed_Lattice_Set).