package goblint
Install
Dune Dependency
Authors
Maintainers
Sources
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.
module Token = Basetype.RawStrings
Widening token.
module TS : sig ... end
Widening token set.
val add_ref : (Token.t -> unit) Stdlib.ref
val add : Token.t -> unit
Add widening token to local state.
val side_tokens : TS.t Stdlib.ref
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
.
with_local_side_tokens f
adds all widening tokens from local state to all side effects in f
.
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.