Frama-C API - Bottom
module Make_Datatype (Domain : Datatype.S) : Datatype.S with type t = Domain.t or_bottom
Datatype constructor
module Bound_Lattice (Lattice : Lattice_type.Join_Semi_Lattice) : Lattice_type.Bounded_Join_Semi_Lattice with type t = Lattice.t or_bottom
Bounds a semi-lattice
val is_bottom : 'a t -> bool
Access
val non_bottom : 'a t -> 'a
val value : bottom:'a -> 'a t -> 'a
val hash : ('a -> int) -> 'a t -> int
Datatype
val pretty : (Stdlib.Format.formatter -> 'a -> unit) -> Stdlib.Format.formatter -> 'a t -> unit
val iter : ('a -> unit) -> 'a t -> unit
Iterator.
In a lattice where the elements are lists of non-bottom values, the empty list is the bottom case.
val to_option : 'a t -> 'a option
Conversion from Bottom to None.
val of_option : 'a option -> 'a t
val of_list : join:('a -> 'a -> 'a) -> 'a list -> 'a t
Joins all elements of a list. Returns Bottom if the list is empty.
val to_list : 'a t -> 'a list
Returns an empty list on Bottom, and a list of one element otherwise.
val list_values : 'a t list -> 'a list
Filters the given list to remove Bottom elements.
val add_to_list : 'a t -> 'a list -> 'a list
add_to_list elt list
adds elt
to the list
if it is not bottom.