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 (10)

Authors

  1. S
    Simmo Saan
  2. M
    Michael Schwarz
  3. J
    Julian Erhard
  4. S
    Sarah Tilscher
  5. K
    Karoliine Holter
  6. M
    Michael Petter
  7. A
    Ali Rasim Kocal
  8. R
    Ralf Vogler
  9. K
    Kalmer Apinis
  10. V
    Vesal Vojdani

Maintainers

  1. S
    Simmo Saan <simmo.saan@gmail.com>
  2. M
    Michael Schwarz <michael.schwarz93@gmail.com>
  3. K
    Karoliine Holter <karoliine.holter@ut.ee>

Sources

goblint-2.7.1.tbz
sha256=af01aac256229f33a90a9fcbfed04b01e3097f154d4d124f006476d6387c6a66
sha512=2a93bfe16881adbc2d8dcbfe38c1e19cd24ca105d8e1eda13d02440f3002874ffe2957dfd937510765233a054a40568b0052db92e31d382a5bd215d1ec12565c

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

Module UnionFind.UnionFind

Quantitative union find

module ValMap = TMap
type 'v node = ('v * Z.t) * int

(value * offset) ref * size of equivalence class

val equal_node : 'v. ('v -> 'v -> Ppx_deriving_runtime.bool) -> 'v node -> 'v node -> Ppx_deriving_runtime.bool
val compare_node : 'v. ('v -> 'v -> Ppx_deriving_runtime.int) -> 'v node -> 'v node -> Ppx_deriving_runtime.int
val hash_node : ('v -> int) -> 'v node -> int
type t = T.t node ValMap.t

Union Find Map: maps value to a node type

val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
exception UnknownValue of T.t
exception InvalidUnionFind of string
val empty : 'a ValMap.t
val parent : ('a * 'b) ValMap.t -> ValMap.key -> 'a

`parent uf v` returns (p, z) where p is the parent element of v in the union find tree and z is the offset.

Throws "Unknown value" if v is not present in the data structure.

val parent_opt : ('a * 'b) ValMap.t -> ValMap.key -> 'a option

`parent_opt uf v` returns Some (p, z) where p is the parent element of v in the union find tree and z is the offset. It returns None if v is not present in the data structure.

val parent_term : (('a * 'b) * 'c) ValMap.t -> ValMap.key -> 'a
val parent_offset : (('a * 'b) * 'c) ValMap.t -> ValMap.key -> 'b
val subtree_size : ('a * 'b) ValMap.t -> ValMap.key -> 'b
val modify_size : ValMap.key -> ((T.t * 'a) * 'b) ValMap.t -> ('b -> 'b) -> ((T.t * 'a) * 'b) ValMap.t

Modifies the size of the equivalence class for the current element and for the whole path to the root of this element.

The third parameter `modification` is the function to apply to the sizes.

val modify_parent : (('a * 'b) * 'c) ValMap.t -> ValMap.key -> ('a * 'b) -> (('a * 'b) * 'c) ValMap.t
val modify_offset : (('a * 'b) * 'c) ValMap.t -> ValMap.key -> ('b -> 'b) -> (('a * 'b) * 'c) ValMap.t
val is_empty : ((T.t * 'a) * 'b) ValMap.t -> bool

Returns true if each equivalence class in the data structure contains only one element, i.e. every node is a root.

val is_root : ((T.t * 'a) * 'b) ValMap.t -> ValMap.key -> Ppx_deriving_runtime.bool

Returns true if v is the representative value of its equivalence class.

Throws "Unknown value" if v is not present in the data structure.

val find : ((T.t * Z.t) * int) ValMap.t -> ValMap.key -> T.t * Z.t * ((T.t * Z.t) * int) ValMap.t

For a variable v it returns the reference variable v' and the offset r'. This find performs path compression. It returns als the updated union-find tree after the path compression.

Throws "Unknown value" if v is not present in the data structure. Throws "Invalid Union Find" if it finds an element in the data structure that is a root but it has a non-zero distance to itself.

val find_no_pc : ((T.t * Z.t) * 'a) ValMap.t -> ValMap.key -> T.t * Z.t

For a variable v it returns the reference variable v' and the offset r'. This find DOES NOT perform path compression.

Throws "Unknown value" if t is not present in the data structure. Throws "Invalid Union Find" if it finds an element in the data structure that is a root but it has a non-zero distance to itself.

val compare_repr : (T.t * Z.t) -> (T.t * Z.t) -> int
val compare_repr_v : (T.t * 'a) -> (T.t * 'b) -> Ppx_deriving_runtime.int

Compare only first element of the tuples (= the parent term). It ignores the offset.

val union : ((T.t * Z.t) * int) ValMap.t -> ValMap.key -> ValMap.key -> Z.t -> T.t * ((T.t * Z.t) * int) ValMap.t * bool

Parameters: uf v1 v2 r

changes the union find data structure `uf` such that the equivalence classes of `v1` and `v2` are merged and `v1 = v2 + r`

returns v,uf,b where

  • `v` is the new reference term of the merged equivalence class. It is either the old reference term of v1 or of v2, depending on which equivalence class is bigger.
  • `uf` is the new union find data structure
  • `b` is true iff v = find v1
val get_eq_classes : ((T.t * Z.t) * 'a) ValMap.t -> (ValMap.key * ((T.t * Z.t) * 'a)) list list

Returns a list of equivalence classes.

val show_uf : ((T.t * Z.t) * int) ValMap.t -> string

Throws "Unknown value" if the data structure is invalid.

val get_representatives : ((T.t * 'a) * 'b) ValMap.t -> ValMap.key list

Returns a list of representative elements.