Module type Eval.Valuation

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 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 or_top
val remove : t -> Cil_types.exp -> t
val remove_loc : t -> Cil_types.lval -> t