Module Lattice_type

module Lattice_type: sig .. end

Lattice signatures.
Consult the Plugin Development Guide for additional details.

module type Join_Semi_Lattice = sig .. end

module type Bounded_Join_Semi_Lattice = sig .. end

module type With_Top = sig .. end

module type With_Error_Top = sig .. end

module type With_Error_Bottom = sig .. end

module type With_Errors = 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 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.

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 Lattice_Set_Generic = sig .. end

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

module type Lattice_Set = sig .. end

module type Lattice_Hashconsed_Set = sig .. end

Module Lattice_type

Over- and under-approximations

Common signatures

Results of generic functors, in module Abstract_interp.

Results of generic functors, in module `Abstract_interp`.