Module Store.Make

Functor that builds an non-relational abstract domain for stores, given implementations for keys, maps of keys, and abstract values that should be associated to keys.

Parameters

module Key : sig ... end
module _ : sig ... end

Signature

include S with type key = Key.t and type value = X.t
include Sigs.ABSTRACT_DOMAIN
type t

Type of abstract values

val bot : t

The bottom element \bot (most precise element)

val is_bot : t -> bool

Tests whether an element is \bot

val top : t

The top element \top (less precise element)

val leq : t -> t -> bool

Inclusion test between abstract values. Smaller elements are more precise; larger elements are less precise. This might not be a total order, and might not be anti-symmetric either.

val join : t -> t -> t

Abstract union of abstract values. This need not be the least upper bound for leq, nor an upper bound at all.

val widen : t -> t -> t

Widening operator, i.e., an approximation of the concrete union, that is used the ensure the convergence of Kleene-based iterations.

val meet : t -> t -> t

Abstract intersection of abstract values. This need not be the greatest lower bound for leq, nor a lower bound at all.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer for abstract values

type key = Key.t
type value = X.t
val empty : t

Abstract value that represents the empty store

val get : t -> key -> value

Queries the value of a key in a store

val remove : t -> key -> t

Removes the entry of a key in a store

val set : t -> key -> value -> t

Adds or replaces the entry of a key in a store. If an entry was present for that key, the new entry is the join of the former value and the provided value.

val set_strong : t -> key -> value -> t

Adds or replaces the entry of a key in a store. If an entry was present for that key, the former entry is discarded and the new entry the provided value (strong update).

val is_top : t -> bool