Module `Absint.AbstractDomain`

Abstract domains and domain combinators

module Types : sig ... end

module type NoJoin = sig ... end

module type S = sig ... end

include sig ... end

module Empty : S with type t = unit: a trivial domain

module type WithBottom = sig ... end: A domain with an explicit bottom value

module type WithTop = sig ... end: A domain with an explicit top value

module BottomLifted : functor (Domain : S) -> sig ... end: Create a domain with Bottom element from a pre-domain

module BottomLiftedUtils : sig ... end

module TopLifted : functor (Domain : S) -> WithTop with type t = Domain.t Types.top_lifted: Create a domain with Top element from a pre-domain

module TopLiftedUtils : sig ... end

module Pair : functor (Domain1 : S) -> functor (Domain2 : S) -> S with type t = Domain1.t * Domain2.t: Cartesian product of two domains.

module Flat : functor (V : IStdlib.PrettyPrintable.PrintableEquatableType) -> sig ... end: Flat abstract domain: Bottom, Top, and non-comparable elements in between

include sig ... end

module Stacked : functor (Below : S) -> functor (Val : S) -> functor (Above : S) -> S with type t = (Below.t, Val.t, Above.t) Types.below_above: Stacked abstract domain: tagged union of Below, Val, and Above domains where all elements of Below are strictly smaller than all elements of Val which are strictly smaller than all elements of Above

module StackedUtils : sig ... end

module MinReprSet : functor (Element : IStdlib.PrettyPrintable.PrintableOrderedType) -> sig ... end: Abstracts a set of Elements by keeping its smallest representative only. The widening is terminating only if the order fulfills the descending chain condition.

module type FiniteSetS = sig ... end

include sig ... end

module FiniteSetOfPPSet : functor (PPSet : IStdlib.PrettyPrintable.PPSet) -> FiniteSetS with type FiniteSetOfPPSet.elt = PPSet.elt: Lift a PPSet to a powerset domain ordered by subset. The elements of the set should be drawn from a *finite* collection of possible values, since the widening operator here is just union.

module FiniteSet : functor (Element : IStdlib.PrettyPrintable.PrintableOrderedType) -> FiniteSetS with type FiniteSet.elt = Element.t: Lift a set to a powerset domain ordered by subset. The elements of the set should be drawn from a *finite* collection of possible values, since the widening operator here is just union.

module type InvertedSetS = sig ... end

module InvertedSet : functor (Element : IStdlib.PrettyPrintable.PrintableOrderedType) -> InvertedSetS with type InvertedSet.elt = Element.t: Lift a set to a powerset domain ordered by superset, so the join operator is intersection

module type MapS = sig ... end

include sig ... end

module MapOfPPMap : functor (PPMap : IStdlib.PrettyPrintable.PPMap) -> functor (ValueDomain : S) -> MapS with type key = PPMap.key and type value = ValueDomain.t and type t = ValueDomain.t PPMap.t: Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else. Uses PPMap as the underlying map

module Map : functor (Key : IStdlib.PrettyPrintable.PrintableOrderedType) -> functor (ValueDomain : S) -> MapS with type key = Key.t and type value = ValueDomain.t: Map domain ordered by union over the set of bindings, so the bottom element is the empty map. Every element implicitly maps to bottom unless it is explicitly bound to something else

module type InvertedMapS = sig ... end

module InvertedMap : functor (Key : IStdlib.PrettyPrintable.PrintableOrderedType) -> functor (ValueDomain : S) -> InvertedMapS with type key = Key.t and type value = ValueDomain.t: Map domain ordered by intersection over the set of bindings, so the top element is the empty map. Every element implictly maps to top unless it is explicitly bound to something else

module SafeInvertedMap : functor (Key : IStdlib.PrettyPrintable.PrintableOrderedType) -> functor (ValueDomain : WithTop) -> InvertedMapS with type key = Key.t and type value = ValueDomain.t: Similar to InvertedMap but it guarantees that it has a canonical form. For example, both {a -> top_v} and empty represent the same abstract value top in InvertedMap, but in this implementation, top is always implemented as empty by not adding the top_v explicitly.

include sig ... end

module FiniteMultiMap : functor (Key : IStdlib.PrettyPrintable.PrintableOrderedType) -> functor (Value : IStdlib.PrettyPrintable.PrintableOrderedType) -> sig ... end

module BooleanAnd : S with type t = bool: Boolean domain ordered by p || ~q. Useful when you want a boolean that's true only when it's true in both conditional branches.

module BooleanOr : WithBottom with type t = bool: Boolean domain ordered by ~p || q. Useful when you want a boolean that's true only when it's true in one conditional branch.

module type MaxCount = sig ... end

module CountDomain : functor (MaxCount : MaxCount) -> sig ... end: Domain keeping a non-negative count with a bounded maximum value. The count can be only incremented and decremented.

module DownwardIntDomain : functor (MaxCount : MaxCount) -> sig ... end: Domain keeping a non-negative count with a bounded maximum value. join is minimum and top is zero.