Module type Simple_memory.Value

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.