module Access_path: sig
.. end
reciprocal_image b m
is the set of bits in the offsetmap m
that may lead to Top(b
) and the set of offsets in m
where one can read an address b
+_
val pretty : Format.formatter -> Db.Access_path.t -> unit
val reciprocal_image_offsm : Base.t ->
Cvalue.V_Offsetmap.t -> Lattice_Interval_Set.Int_Intervals.t * Ival.t
reciprocal_image b m
is the set of bits in the offsetmap m
that may lead to Top(b
) and the set of offsets in m
where one can read an address b
+_
reciprocal_image m b
is the set of bits in the map m
that may lead
to Top(b
) and the location in m
where one may read an address b
+_
val reciprocal_image : Base.t -> Cvalue.Model.t -> Locations.Zone.t * Locations.Location_Bits.t
val compute : Cvalue.Model.t -> Base.Set.t -> Db.Access_path.t
val filter : (Locations.Zone.t * Locations.Location_Bits.t) Base.Map.t ->
Locations.Zone.t -> (Locations.Zone.t * Locations.Location_Bits.t) Base.Map.t
val main : unit -> unit