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.3.0.tbz

sha256=b729c94adb383a39aea32eb005c988dfd44b92af22ee6a4eedf4239542ac6c26

sha512=643b98770e5fe5644324c95c9ae3a9f698f25c8b11b298f0751d524e0b20af368b2a465fc8200b75a73d48fc9a053fd90f5e8920d4db070927f93188bb8687e0

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.