package goblint
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6
sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af
doc/goblint.domain/DisjointDomain/index.html
Module DisjointDomainSource
Abstract domains for collections of elements from disjoint unions of domains. Formally, the elements form a cofibered domain from a discrete category.
Elements are grouped into disjoint buckets by a congruence or/and a projection. All operations on elements are performed bucket-wise and must be bucket-closed.
Examples of such domains are path-sensitivity and address sets.
Sets
By projection
Buckets defined by projection. The module is the image (representative) of the projection function of_elt.
module ProjectiveSet
(E : Printable.S)
(B : SetDomain.S with type elt = E.t)
(R : Representative with type elt = E.t) :
sig ... endSet of elements E.t grouped into buckets by R, where each bucket is described by the set B.
module ProjectiveSetPairwiseMeet
(E : Printable.S)
(B : MayEqualSetDomain with type elt = E.t)
(R : Representative with type elt = E.t) :
SetDomain.S with type elt = E.tBy congruence
Buckets defined by congruence.
module PairwiseSet
(E : Printable.S)
(B : SetDomain.S with type elt = E.t)
(C : Congruence with type elt = E.t) :
SetDomain.S with type elt = E.tSet of elements E.t grouped into buckets by C, where each bucket is described by the set B.
Buckets defined by a coarse projection and a fine congruence. Congruent elements must have the same representative, but not vice versa (Representative would then suffice).
module CombinedSet
(E : Printable.S)
(B : SetDomain.S with type elt = E.t)
(RC : RepresentativeCongruence with type elt = E.t) :
sig ... endSet of elements E.t grouped into buckets by RC, where each bucket is described by the set B.
Maps
Generalization of above sets into maps, whose key set behaves like above sets, but each element can also be associated with a value.
By projection
module ProjectiveMap
(E : Printable.S)
(V : Printable.S)
(B : MapDomain.S with type key = E.t and type value = V.t)
(R : Representative with type elt = E.t) :
MapDomain.S with type key = E.t and type value = B.valueMap of keys E.t grouped into buckets by R, where each bucket is described by the map B with values V.t.
By congruence
module PairwiseMap
(E : Printable.S)
(R : Printable.S)
(B : MapDomain.S with type key = E.t and type value = R.t)
(C : Congruence with type elt = E.t) :
MapDomain.S with type key = E.t and type value = B.valueMap of keys E.t grouped into buckets by C, where each bucket is described by the map B with values R.t.