package goblint

You can search for identifiers within the package.

in-package search v0.2.0

Static analysis framework for C

Install

Dune Dependency

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

Authors

Maintainers

Sources

goblint-2.4.0.tbz

sha256=99b78e6def71534d195eef9084baa26d8334b36084e120aa6afb300c9bf8afa6

sha512=f3162bd95a03c00358a2991f6152fc6169205bfb4c55e2c483e98cc3935673df9656d025b6f1ea0fa5f1bd0aee037d4f483966b0d2907e3fa9bf11a93a3392af

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

Module `Goblint_lib.WideningTokens`

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.

see http://www2.in.tum.de/bib/files/mihaila13widening.pdf
Mihaila, B., Sepp, A. & Simon, A. Widening as Abstract Domain.

module Token = Basetype.RawStrings

Widening token.

module TS : sig ... end

Widening token set.

val add_ref : (Token.t -> unit) Stdlib.ref

Reference to current add implementation. Maintained by Lifter.

val add : Token.t -> unit

Add widening token to local state.

val side_tokens : TS.t Stdlib.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 Stdlib.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.

module Lifter (S : Analyses.Spec) : Analyses.Spec

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