Module Abstract_interp

module Abstract_interp: sig .. end

Functors for generic lattices implementations.

Consult the Plugin Development Guide

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