Module Function_Froms.Memory

module Memory: sig .. end

include Lmap_bitwise.Location_map_bitwise

val pretty_ind_data : Stdlib.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 ->
       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

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.

type return = 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