package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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

Sourcemodule type Representative = sig ... end

Buckets defined by projection. The module is the image (representative) of the projection function of_elt.

Sourcemodule ProjectiveSet (E : Printable.S) (B : SetDomain.S with type elt = E.t) (R : Representative with type elt = E.t) : sig ... end

Set of elements E.t grouped into buckets by R, where each bucket is described by the set B.

Sourcemodule type MayEqualSetDomain = sig ... end
Sourcemodule ProjectiveSetPairwiseMeet (E : Printable.S) (B : MayEqualSetDomain with type elt = E.t) (R : Representative with type elt = E.t) : SetDomain.S with type elt = E.t

By congruence

Sourcemodule type Congruence = sig ... end

Buckets defined by congruence.

Sourcemodule 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.t

Set of elements E.t grouped into buckets by C, where each bucket is described by the set B.

Sourcemodule type RepresentativeCongruence = sig ... end

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).

Sourcemodule CombinedSet (E : Printable.S) (B : SetDomain.S with type elt = E.t) (RC : RepresentativeCongruence with type elt = E.t) : sig ... end

Set 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

Sourcemodule 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.value

Map of keys E.t grouped into buckets by R, where each bucket is described by the map B with values V.t.

By congruence

Sourcemodule 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.value

Map of keys E.t grouped into buckets by C, where each bucket is described by the map B with values R.t.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct