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

Module Goblint_lib.WideningTokenLifter

Widening tokens are a generic and dynamic mechanism for delaying widening.

All abstract elements carry a set of tokens, which analyses can add into. Lifted abstract elements are only widened if the token set does not increase, i.e. adding a widening token delays a widening.

module Token = WideningToken
module TS : sig ... end

Widening token set.

val add_ref : (Token.t -> unit) Domain.DLS.key

Reference to current add implementation. Maintained by Lifter.

val add : Token.t -> unit

Add widening token to local state.

val side_tokens : TS.t ref

Widening tokens added to side effects. Maintained by Lifter and MCP.

val with_side_token : TS.elt -> (unit -> 'a) -> 'a

with_side_token t f adds widening token t to all side effects in f.

val with_side_tokens : TS.t -> (unit -> 'a) -> 'a

with_side_tokens ts f adds widening tokens ts to all side effects in f.

val local_tokens : TS.t ref

Widening tokens in current local state. Maintained by Lifter.

val with_local_side_tokens : (unit -> 'a) -> 'a

with_local_side_tokens f adds all widening tokens from local state to all side effects in f.

module Dom (D : Lattice.S) : sig ... end

Lift D to carry widening tokens. All operations delegate to inner domain, except widening tokens are used to delay widenings.

Lift S to carry widening tokens with both local and global states.