package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
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_Diff_One with type t := KVMap.t
val diff_if_one : KVMap.t -> KVMap.t -> KVMap.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 := KVMap.t
val fold_enum : (KVMap.t -> 'a -> 'a) -> KVMap.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 : KVMap.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 : KVMap.t -> Key.t * Value.t

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 : KVMap.t -> Key.t * Value.t

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct