Frama-C API - MapSet_Lattice_with_cardinality
A notion of cardinality for mapset lattice.
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.