Frama-C API - `Valuation`

type t

type value = Value.t

Abstract value.

type origin

Origin of values.

type loc = 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