module Memory:sig
..end
include Lmap_bitwise.Location_map_bitwise
val pretty_ind_data : Format.formatter -> t -> unit
Prints the detail of address and data dependencies, as opposed to pretty
that prints the backwards-compatible union of them
val find : t -> Locations.Zone.t -> Locations.Zone.t
Imprecise version of find, in which data and indirect dependencies are not distinguished
val find_precise : t -> Locations.Zone.t -> Function_Froms.Deps.t
Precise version of find
Collecting dependencies on a given zone.
val add_binding : exact:bool -> t -> Locations.Zone.t -> Function_Froms.Deps.t -> t
val add_binding_loc : exact:bool -> t -> Locations.location -> Function_Froms.Deps.t -> t
val add_binding_precise_loc : exact:bool ->
t -> Precise_locs.precise_location -> Function_Froms.Deps.t -> t
val bind_var : Cil_types.varinfo -> Function_Froms.Deps.t -> t -> t
val unbind_var : Cil_types.varinfo -> t -> t
val map : (Function_Froms.DepsOrUnassigned.t -> Function_Froms.DepsOrUnassigned.t) ->
t -> t
val compose : t -> t -> t
Sequential composition. See Function_Froms.DepsOrUnassigned.compose
.
val substitute : t -> Function_Froms.Deps.t -> Function_Froms.Deps.t
substitute m d
applies m
to d
so that any dependency in d
is
expressed using the dependencies already present in m
. For example,
substitute 'x From y' 'x'
returns 'y'
.
Dependencies for \result
.
typereturn =
Function_Froms.Deps.t
val default_return : return
Default value to use for storing the dependencies of \result
val top_return : return
Completely imprecise return
val top_return_size : Int_Base.t -> return
Completely imprecise return of the given size
val add_to_return : ?start:int ->
size:Int_Base.t ->
?m:return ->
Function_Froms.Deps.t -> return
Add some dependencies to \result
, between bits start
and
start+size-1
, to the Deps.t
value; default value for start
is 0.
If m
is specified, the dependencies are added to it. Otherwise,
Function_Froms.Memory.default_return
is used.
val collapse_return : return -> Function_Froms.Deps.t