Frama-C API - Map_Lattice_with_cardinality
A notion of cardinality for maps with a complete lattice structure.
include Lattice_with_cardinality
include Lattice_type.With_Enumeration with type t := 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 : 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).