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