Eval.Valuation
Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached here. See Eval
for more details.
type value = value
Abstract value.
type origin = origin
Origin of values.
type loc = loc
Abstract memory location.
val empty : t
val find :
t ->
Frama_c_kernel.Cil_types.exp ->
(value, origin) Eva.Eval.record_val Eva.Eval.or_top
val add :
t ->
Frama_c_kernel.Cil_types.exp ->
(value, origin) Eva.Eval.record_val ->
t
val fold :
(Frama_c_kernel.Cil_types.exp ->
(value, origin) Eva.Eval.record_val ->
'a ->
'a) ->
t ->
'a ->
'a
val find_loc :
t ->
Frama_c_kernel.Cil_types.lval ->
loc Eva.Eval.record_loc Eva.Eval.or_top
val remove : t -> Frama_c_kernel.Cil_types.exp -> t
val remove_loc : t -> Frama_c_kernel.Cil_types.lval -> t