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.