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
val builtins : (string * t Simple_memory.builtin) list
A list of builtins for the domain: each builtin is associated with the name of the C function it interprets.