Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eva_lattice_type

Lattice signatures using the Bottom type: these lattices do not include a bottom element, and return `Bottom instead when needed. Except that, they are identical to the module signatures in Lattice_type.

module type Join_Semi_Lattice = Lattice_type.Join_Semi_Lattice
module type With_Top = Lattice_type.With_Top
module type With_Intersects = Lattice_type.With_Intersects
module type With_Enumeration = Lattice_type.With_Enumeration
module type With_Cardinal_One = Lattice_type.With_Cardinal_One
module type With_Narrow = sig ... end
module type With_Under_Approximation = sig ... end
module type With_Diff = sig ... end
module type With_Diff_One = 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_AI_Lattice_with_cardinality = sig ... end

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