Module type Store.S

Signature of stores

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