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 value = valueAbstract value.
type origin = originOrigin of values.
type loc = locAbstract memory location.
val empty : tval find : t -> Eva.Eval.exp -> (value, origin) Eva.Eval.record_val Eva.Eval.or_topval add : t -> Eva.Eval.exp -> (value, origin) Eva.Eval.record_val -> tval fold : (Eva.Eval.exp -> (value, origin) Eva.Eval.record_val -> 'a -> 'a) -> t -> 'a -> 'aval find_loc : t -> Eva.Eval.lval -> loc Eva.Eval.record_loc Eva.Eval.or_topval remove : t -> Eva.Eval.exp -> tval remove_loc : t -> Eva.Eval.lval -> t