Frama-C:
Plug-ins:
Libraries:

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 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 -> exp -> (value, origin) record_val or_top
val add : t -> exp -> (value, origin) record_val -> t
val fold : (exp -> (value, origin) record_val -> 'a -> 'a) -> t -> 'a -> 'a
val find_loc : t -> lval -> loc record_loc or_top
val find_loc_def : t -> lval -> loc
val remove : t -> exp -> t
val remove_loc : t -> lval -> t