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
type
alarm =
| |
SureAlarm |
|||
| |
Alarm |
|||
| |
NoAlarm |
(* | Less ambiguous version of | *) |
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:
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:
See e.g.
module type Collapse =sig
..end
module Make_Lattice_Product:functor (
L1
:
Lattice_type.AI_Lattice_with_cardinal_one
) ->
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