Frama-C:
Plug-ins:
Libraries:

Frama-C API - With_Cardinality

Adds cardinality functions for maps, according to a notion of cardinality on the values. It also requires a function is_summary on keys, indicating whether a key represents a summary of possibly multiple keys; a binding to such a key has never a cardinality of one.

Parameters

module _ : sig ... end
module _ : Lattice_type.Full_AI_Lattice_with_cardinality with type t := Value.t

Signature

include Lattice_with_cardinality with type t := t
include Lattice_type.With_Cardinal_One with type t := t
val cardinal_zero_or_one : t -> bool
include Lattice_type.With_Diff_One with type t := t
val diff_if_one : t -> t -> t

diff_if_one t1 t2 is an over-approximation of t1-t2.

  • returns

    t1 if t2 is not a singleton.

include Lattice_type.With_Enumeration with type t := t
val fold_enum : (t -> 'a -> 'a) -> t -> 'a -> 'a

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.

val find_lonely_key : t -> key * v

If t is a singleton map binding k to v and t is not a summary key, then returns the pair (k,v).

  • raises Not_found

    otherwise.

val find_lonely_binding : t -> key * v

If t is a singleton map binding k to v, if t is not a summary key, and if cardinal_zero_or_one v holds, returns the pair (k,v).

  • raises Not_found

    otherwise.