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/CongruenceClosure/MRMap/index.html

Module CongruenceClosure.MRMap

Minimal representatives map. It maps each representative term of an equivalence class to the minimal term of this representative class. rep -> (t, z) means that t = rep + z

type t = (T.t * Z.t) TMap.t
val equal : t -> t -> Ppx_deriving_runtime.bool
val compare : t -> t -> Ppx_deriving_runtime.int
val hash : t -> int
val bindings : 'a TMap.t -> (TMap.key * 'a) list
val find : TMap.key -> 'a TMap.t -> 'a
val find_opt : TMap.key -> 'a TMap.t -> 'a option
val add : TMap.key -> 'a -> 'a TMap.t -> 'a TMap.t
val remove : TMap.key -> 'a TMap.t -> 'a TMap.t
val mem : TMap.key -> 'a TMap.t -> bool
val empty : 'a TMap.t
val show_min_rep : (T.t * Z.t) TMap.t -> string
val update_min_repr : (((Goblint_lib__UnionFind.term * Z.t) * 'a) TUF.ValMap.t * TSet.t * LMap.t) -> (term * Z.t) TMap.t -> TUF.ValMap.key list -> (term * Z.t) TMap.t

Uses dijkstra algorithm to update the minimal representatives of the successor nodes of all edges in the queue and if necessary it recursively updates the minimal representatives of the successor nodes. The states in the queue must already have an updated min_repr. This function visits only the successor nodes of the nodes in queue, not the nodes themselves. Before visiting the nodes, it sorts the queue by the size of the current mininmal representative.

parameters:

  • `(uf, set, map)` represent the union find data structure and the corresponding term set and lookup map.
  • `min_representatives` maps each representative of the union find data structure to the minimal representative of the equivalence class.
  • `queue` contains the states that need to be processed. The states of the automata are the equivalence classes and each state of the automata is represented by the representative term. Therefore the queue is a list of representative terms.

Returns:

  • The updated `min_representatives` map with the minimal representatives
val compute_minimal_representatives : (((Goblint_lib__UnionFind.term * Z.t) * 'a) TUF.ValMap.t * TSet.t * LMap.t) -> (term * Z.t) TMap.t
val initial_minimal_representatives : TSet.t -> (TMap.key * Z.t) TMap.t

Computes the initial map of minimal representatives. It maps each element `e` in the set to `(e, 0)`.