Module Abstract_interp

module Abstract_interp: sig .. end
Functors for generic lattices implementations.
Consult the Plugin Development Guide for additional details.

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.Set 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