Module Abstract_interp

module Abstract_interp: sig .. end

Functors for generic lattices implementations.


exception Error_Top

Raised by some functions when encountering a top value.

exception Error_Bottom

Raised by Lattice_Base.project.

exception Not_less_than

Raised by Lattice.cardinal_less_than.

exception Can_not_subdiv

Used by other modules e.g. Fval.subdiv_float_interval.

type truth = 
| True
| False
| Unknown (*

Truth values with a possibility for 'Unknown'

*)
val inv_truth : truth -> truth
module Comp: sig .. end

Signatures for comparison operators ==, !=, <, >, <=, >=.

module Int: sig .. end
module Rel: sig .. end

"Relative" integers.

module Bool: sig .. end
module Make_Lattice_Base: 
functor (V : Lattice_type.Lattice_Value-> Lattice_Base with type l = V.t
module Make_Lattice_Set: 
functor (V : Datatype.S-> 
functor (Set : Lattice_type.Hptset with type elt = V.t-> Lattice_type.Lattice_Set with module O = Set
module Make_Hashconsed_Lattice_Set: 
functor (V : Hptmap.Id_Datatype-> 
functor (Set : Hptset.S with type elt = V.t-> Lattice_type.Lattice_Set with module O = Set

See e.g.

module type Collapse = sig .. end
module Make_Lattice_Product: 
functor (L1 : Lattice_type.AI_Lattice_with_cardinal_one-> 
functor (L2 : Lattice_type.AI_Lattice_with_cardinal_one-> 
functor (C : Collapse-> Lattice_Product with type t1 = L1.t and type t2 = L2.t

If C.collapse then L1.bottom,_ = _,L2.bottom = bottom

module Make_Lattice_UProduct: 
functor (L1 : Lattice_type.AI_Lattice_with_cardinal_one-> 
functor (L2 : Lattice_type.AI_Lattice_with_cardinal_one-> Lattice_UProduct with type t1 = L1.t and type t2 = L2.t

Uncollapsed product.

module Make_Lattice_Sum: 
functor (L1 : Lattice_type.AI_Lattice_with_cardinal_one-> 
functor (L2 : Lattice_type.AI_Lattice_with_cardinal_one-> Lattice_Sum with type t1 = L1.t and type t2 = L2.t