Frama-C API - `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 t

type value = value

Abstract value.

type origin = origin

Origin of values.

type loc = location

Abstract memory location.

val empty : t

val find : t -> Eval.exp -> (value, origin) Eval.record_val Eval.or_top

val add : t -> Eval.exp -> (value, origin) Eval.record_val -> t

val fold : (Eval.exp -> (value, origin) Eval.record_val -> 'a -> 'a) -> t -> 'a -> 'a

val find_loc : t -> Eval.lval -> loc Eval.record_loc Eval.or_top

val find_loc_def : t -> Eval.lval -> loc

val remove : t -> Eval.exp -> t

val remove_loc : t -> Eval.lval -> t

Frama-C API - Valuation

Frama-C API - `Valuation`