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

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