Module type Simple_memory.S

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.