module type Valuation = sig
.. end
Results of an evaluation: the results of all intermediate calculation (the
value of each expression and the location of each lvalue) are cached in a
map.
type
t
type
value
Abstract value.
type
origin
Origin of values.
type
loc
Abstract memory location.
val empty : t
val find : t ->
Cil_types.exp ->
(value, origin) Eval.record_val Eval.or_top
val add : t ->
Cil_types.exp ->
(value, origin) Eval.record_val ->
t
val fold : (Cil_types.exp ->
(value, origin) Eval.record_val -> 'a -> 'a) ->
t -> 'a -> 'a
val find_loc : t ->
Cil_types.lval -> loc Eval.record_loc Eval.or_top
val filter : (Cil_types.exp ->
(value, origin) Eval.record_val -> bool) ->
(Cil_types.lval -> loc Eval.record_loc -> bool) ->
t -> t