Frama-C API - _
include Lattice_with_cardinality with type t := KVMap.t
include Lattice_type.With_Cardinal_One with type t := KVMap.t
val cardinal_zero_or_one : KVMap.t -> bool
include Lattice_type.With_Enumeration with type t := KVMap.t
Fold on the elements of the value one by one if possible. Raises Abstract_interp.Not_less_than
when there is an infinite number of elements to enumerate.
val cardinal_less_than : KVMap.t -> int -> int
Raises Abstract_interp.Not_less_than
whenever the cardinal of the given lattice is strictly higher than the given integer.
If t
is a singleton map binding k
to v
and t
is not a summary key, then returns the pair (k,v).