Frama-C API - MapSet_Lattice
A lattice structure on top of maps from keys to values and sets of keys. The maps and the sets have their own lattice structure (see abstract_interp.ml for the lattice of sets). The sets are implicitly considered as maps binding all their keys to top. Any map is included in the set of its keys (and in any larger set).
include Datatype.S_with_collections with type t := t
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
module Set : Datatype.Set with type elt = t
module Map : Datatype.Map with type key = t
module Hashtbl : Datatype.Hashtbl with type key = t
include Lattice with type t := t
include Lattice_type.Bounded_Join_Semi_Lattice with type t := t
include Lattice_type.Join_Semi_Lattice with type t := t
datatype of element of the lattice
include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val packed_descr : Structural_descr.pack
Packed version of the descriptor.
val reprs : t list
List of representants of the descriptor.
val hash : t -> int
Hash function: same spec than Hashtbl.hash
.
val pretty : Stdlib.Format.formatter -> t -> unit
Pretty print each value in an user-friendly way.
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
mem_project f x
must return true
iff there is a value p
of type Project.t
in x
such that f p
returns true
.
include Lattice_type.With_Intersects with type t := t
val bottom : t
val top : t
add key v t
binds the value v
to key
in t
. If t
is a set, it adds key
to the set. If v
is bottom, then it removes the key
from t
instead.
find key t
returns the value bound to key
in t
. It returns Value.top if t
is a set that contains key
. It returns Value.bottom if key
does not belong to t
.
If t
is a singleton map binding k
to v
, then returns the pair (k,v).
for_all p t
checks if all binding of t
satisfy p
. Always false if t
is top.
exists p t
checks if one binding of t
satisfies p
. Always true if t
is top.
val pretty_debug : Stdlib.Format.formatter -> t -> unit