package goblint

  1. Overview
  2. Docs
Static analysis framework for C

Install 

dune-project
 Dependency

goblint.in.tum.de Readme Changelog Edit opam file Versions (9)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. R
    Ralf Vogler
  6. K
    Kalmer Apinis
  7. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>

Sources

goblint-2.3.0.tbz
sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26
sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

doc/goblint.lib/Goblint_lib/DisjointDomain/index.html

Module Goblint_lib.DisjointDomain

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

module type Representative = sig ... end

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

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

module type MayEqualSetDomain = sig ... end
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.t

By congruence

module type Congruence = sig ... end

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

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

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

module 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

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

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

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