AbstractDomain (infer.Absint.AbstractDomain)

Abstract domains and domain combinators

module Types : sig ... end

module type Comparable = sig ... end

module type Disjunct = sig ... end

module type S = sig ... end

include sig ... end

type empty = |

module Empty : S with type t = empty

module Unit : 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 type WithBottomTop = sig ... end

A domain with an explicit bottom and top values

module BottomLifted (Domain : S) : sig ... end

Create a domain with Bottom element from a pre-domain

module BottomLiftedUtils : sig ... end

module TopLifted (Domain : S) : sig ... end

Create a domain with Top element from a pre-domain

module TopLiftedUtils : sig ... end

module BottomTopLifted (Domain : S) : WithBottomTop

Create a domain with Bottom and Top elements from a pre-domain

module Pair (Domain1 : S) (Domain2 : S) : S with type t = Domain1.t * Domain2.t

Cartesian product of two domains.

module PairWithBottom
  (Domain1 : WithBottom)
  (Domain2 : WithBottom) : 
  WithBottom with type t = Domain1.t * Domain2.t

module PairWithTop
  (Domain1 : WithTop)
  (Domain2 : WithTop) : 
  WithTop with type t = Domain1.t * Domain2.t

module PairDisjunct
  (Domain1 : Disjunct)
  (Domain2 : Disjunct) : 
  Disjunct with type t = Domain1.t * Domain2.t

module Flat (V : IStdlib.PrettyPrintable.PrintableEquatableType) : sig ... end

Flat abstract domain: Bottom, Top, and non-comparable elements in between

include sig ... end

module Stacked
  (Below : S)
  (Val : S)
  (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
  (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
  (PPSet : IStdlib.PrettyPrintable.PPSet) : 
  FiniteSetS with type t = PPSet.t with type 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
  (Element : IStdlib.PrettyPrintable.PrintableOrderedType) : 
  FiniteSetS with type 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
  (Element : IStdlib.PrettyPrintable.PrintableOrderedType) : 
  InvertedSetS with type 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
  (PPMap : IStdlib.PrettyPrintable.PPMap)
  (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
  (Key : IStdlib.PrettyPrintable.PrintableOrderedType)
  (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
  (Key : IStdlib.PrettyPrintable.PrintableOrderedType)
  (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
  (Key : IStdlib.PrettyPrintable.PrintableOrderedType)
  (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
  (Key : IStdlib.PrettyPrintable.PrintableOrderedType)
  (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 (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 (MaxCount : MaxCount) : sig ... end

Domain keeping a non-negative count with a bounded maximum value. join is minimum and top is zero.