Module Abstract_interp

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

exception Not_less_than
Raised by Lattice.cardinal_less_than.
exception Can_not_subdiv
Used by other modules e.g. Fval.subdiv_float_interval.
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 : Lattice_type.Lattice_Value) -> Lattice_Set with type O.elt=V.t
module Make_Hashconsed_Lattice_Set: 
functor (V : Hptmap.Id_Datatype) ->
functor (O : Hptset.S with type elt = V.t) -> Lattice_Hashconsed_Set with module O = O
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