package goblint

  1. Overview
  2. Docs
package goblint
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct