package goblint

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

Module MapDomain.JoinedSource

Map abstracted by a single (joined) key.

Parameters

module E : Lattice.S
module R : Lattice.S

Signature

include PS with type key = E.t with type value = R.t
include Printable.S
Sourcetype t
Sourcetype key = E.t

The type of the map keys.

Sourcetype value = R.t

The type of the values.

Sourceval add : key -> value -> t -> t
Sourceval remove : key -> t -> t
Sourceval find : key -> t -> value
Sourceval find_opt : key -> t -> value option
Sourceval mem : key -> t -> bool
Sourceval iter : (key -> value -> unit) -> t -> unit
Sourceval map : (value -> value) -> t -> t
Sourceval filter : (key -> value -> bool) -> t -> t
Sourceval mapi : (key -> value -> value) -> t -> t
Sourceval fold : (key -> value -> 'a -> 'a) -> t -> 'a -> 'a
Sourceval add_list : (key * value) list -> t -> t
Sourceval add_list_set : key list -> value -> t -> t
Sourceval add_list_fun : key list -> (key -> value) -> t -> t
Sourceval for_all : (key -> value -> bool) -> t -> bool
Sourceval map2 : (value -> value -> value) -> t -> t -> t
Sourceval long_map2 : (value -> value -> value) -> t -> t -> t
Sourceval merge : (key -> value option -> value option -> value option) -> t -> t -> t
Sourceval cardinal : t -> int
Sourceval choose : t -> key * value
Sourceval singleton : key -> value -> t
Sourceval empty : unit -> t
Sourceval is_empty : t -> bool
Sourceval exists : (key -> value -> bool) -> t -> bool
Sourceval bindings : t -> (key * value) list
include Lattice.S with type t := t
include Lattice.PO with type t := t
include Printable.S with type t := t
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
val show : t -> string
val pretty : unit -> t -> Printable.Pretty.doc
val printXml : 'a BatInnerIO.output -> t -> unit
val name : unit -> string
val to_yojson : t -> Yojson.Safe.t
val tag : t -> int

Unique ID, given by HConsed, for context identification in witness

val arbitrary : unit -> t QCheck.arbitrary
val relift : t -> t
Sourceval leq : t -> t -> bool
Sourceval join : t -> t -> t
Sourceval meet : t -> t -> t
Sourceval widen : t -> t -> t

widen x y assumes leq x y. Solvers guarantee this by calling widen old (join old new).

Sourceval narrow : t -> t -> t
Sourceval pretty_diff : unit -> (t * t) -> Lattice.Pretty.doc

If leq x y = false, then pretty_diff () (x, y) should explain why.

Sourceval bot : unit -> t
Sourceval is_bot : t -> bool
Sourceval top : unit -> t
Sourceval is_top : t -> bool
Sourceval widen_with_fct : (value -> value -> value) -> t -> t -> t
Sourceval join_with_fct : (value -> value -> value) -> t -> t -> t
Sourceval leq_with_fct : (value -> value -> bool) -> t -> t -> bool
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