module type S =sig
..end
Signature of a simple memory abstraction for scalar variables.
type
t
type
value
val add : Precise_locs.precise_location ->
Cil_types.typ ->
value -> t -> t
add loc typ v state
binds loc
to v
in state. If typ
does
not match the effective type of the location pointed, V.top
is
bound instead. This function automatically handles the case where
loc
abstracts multiple locations, or when some locations are not
tracked by the domain.
val find : Precise_locs.precise_location ->
Cil_types.typ -> t -> value
find loc typ state
returns the join of the abstract values stored
in the locations abstracted to by loc
in state
, assuming the
result has type typ
. When loc
includes untracked locations, or when
typ
does not match the type of the locations in loc
, the
result is approximated.
val remove : Precise_locs.precise_location -> t -> t
remove loc state
drops all information on the locations pointed to
by loc
from state
.
val remove_variables : Cil_types.varinfo list -> t -> t
remove_variables list state
drops all information about the variables
in list
from state.
val fold : (Base.t -> value -> 'a -> 'a) ->
t -> 'a -> 'a
Fold on base value pairs.