module Memory:sig
..end
include Lmap_bitwise.Location_map_bitwise
val pretty_ind_data : Format.formatter -> t -> unit
pretty
that prints the backwards-compatible union of themval find : t -> Locations.Zone.t -> Locations.Zone.t
val find_precise : t -> Locations.Zone.t -> Function_Froms.Deps.t
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 ->
Locations.access ->
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
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'
.\result
.typereturn =
Function_Froms.Deps.t
val default_return : return
\result
val top_return : return
val top_return_size : Int_Base.t -> return
val add_to_return : ?start:int ->
size:Int_Base.t ->
?m:return ->
Function_Froms.Deps.t -> return
\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