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. K
    Karoliine Holter
  6. R
    Ralf Vogler
  7. K
    Kalmer Apinis
  8. 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.6.0.tbz
sha256=20d5b7332a9f6072ab9ba86c4a53b898eaf681286c56a8805c41850bbf3ddf41
sha512=7c7685cfcd9aa866bc40e813df2bfcb3c79b3d40e615d8d6d0939c5798b9d70dd7f2ba87a741f5ba0ce891e9d254627207fb28057f1f2f6611e4e0d128fd6a71

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

Module Goblint_lib.UnionFind

The Union Find is used by the C-2PO Analysis. This file contains the code for a quantitative union find and the quantitative finite automata. They will be necessary in order to construct the congruence closure of terms.

module M = Messages
module Tuple3 = Batteries.Tuple3
module Tuple2 = Batteries.Tuple2
exception Unsat
val compare_exp : 'a -> 'b -> int
val equal_exp : 'a -> 'b -> bool
val hash_exp : 'a -> int
type term =
  1. | Addr of DuplicateVars.Var.t
  2. | Aux of DuplicateVars.Var.t * GoblintCil.exp
  3. | Deref of term * Z.t * GoblintCil.exp
val equal_term : term -> term -> Ppx_deriving_runtime.bool
val hash_term : term -> int
val compare_term : term -> term -> Ppx_deriving_runtime.int
val normal_form_tuple_3 : (term * term * Z.t) -> term * term * Z.t
val normal_form_tuple_2 : (term * term) -> term * term
val tuple3_equal : (term * term * Z.t) -> (term * term * Z.t) -> bool

Two propositions are equal if they are syntactically equal or if one is t_1 = z + t_2 and the other t_2 = - z + t_1.

val tuple3_cmp : (term * term * Z.t) -> (term * term * Z.t) -> int
val tuple3_hash : (term * term * Z.t) -> int
val tuple2_equal : (term * term) -> (term * term) -> bool
val tuple2_cmp : (term * term) -> (term * term) -> int
val tuple2_hash : (term * term) -> int
type term_offset_relation = term * term * Z.t
val hash_term_offset_relation : term_offset_relation -> int
val compare_term_offset_relation : term_offset_relation -> term_offset_relation -> Ppx_deriving_runtime.int
type block_relation = term * term
val hash_block_relation : block_relation -> int
val compare_block_relation : block_relation -> block_relation -> Ppx_deriving_runtime.int
type prop =
  1. | Equal of term_offset_relation
  2. | Nequal of term_offset_relation
  3. | BlNequal of block_relation
val equal_prop : prop -> prop -> Ppx_deriving_runtime.bool
val hash_prop : prop -> int
val compare_prop : prop -> prop -> Ppx_deriving_runtime.int
module T : sig ... end

The terms consist of address constants and dereferencing function with sum of an integer. The dereferencing function is parametrized by the size of the element in the memory. We store the CIL expression of the term in the data type, such that it it easier to find the types of the dereferenced elements. Also so that we can easily convert back from term to Cil expression.

module TMap : sig ... end
module TSet : sig ... end
module UnionFind : sig ... end

Quantitative union find

module ZMap : sig ... end
module LookupMap : sig ... end

For each representative t' of an equivalence class, the LookupMap maps t' to a map that maps z to a term in the data structure that is equal to *(z + t').