module type Value = sig
.. end
Abstraction of the values variables are mapped to.
include Datatype.S
Lattice structure.
val top : t
val join : t -> t -> t
val widen : t -> t -> t
val narrow : t -> t -> t Eval.or_bottom
val is_included : t -> t -> bool
val track_variable : Cil_types.varinfo -> bool
This function must return true
if the given variable should be
tracked by the domain. All untracked variables are implicitely
mapped to V.top
.
val pretty_debug : t Pretty_utils.formatter
Can be equal to pretty