module Lattice_type:sig
..end
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
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
module type AI_Lattice_with_cardinal_one =sig
..end
Abstract_interp
.
module type Full_Lattice =sig
..end
module type Full_AI_Lattice_with_cardinality =sig
..end
Abstract_interp
. module type Lattice_Value = Datatype.S_with_collections
module type Lattice_Product =sig
..end
Bottom
is handled especially.
module type Lattice_UProduct =sig
..end
Abstract_interp.Make_Lattice_UProduct
).
module type Lattice_Sum =sig
..end
Abstract_interp.Make_Lattice_Sum
).
module type Lattice_Base =sig
..end
module type Lattice_Set_Generic =sig
..end
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