module Precise_locs: sig
.. end
This module provide transient datastructures that may be more precise
than an
Ival.t
,
Locations.Location_Bits.t
and
Locations.location
respectively, typically for l-values such as
t[i][j]
,
p->t[i]
, etc.
Those structures do not have a lattice structure, and cannot be stored
as an abstract domain. However, they can be use to model more precisely
read or write accesses to semi-imprecise l-values.
type
precise_offset =
| |
POBottom |
| |
POZero |
| |
POSingleton of Abstract_interp.Int.t |
| |
POPrecise of Ival.t * Abstract_interp.Int.t |
| |
POImprecise of Ival.t |
| |
POShift of Ival.t * precise_offset * Abstract_interp.Int.t |
val pretty_offset : Format.formatter -> precise_offset -> unit
val offset_zero : precise_offset
val offset_bottom : precise_offset
val offset_top : precise_offset
val is_bottom_offset : precise_offset -> bool
val cardinal_zero_or_one_offset : precise_offset -> bool
val small_cardinal : Abstract_interp.Int.t -> bool
val _cardinal_offset : precise_offset -> Abstract_interp.Int.t option
val imprecise_offset : precise_offset -> Ival.t
val _scale_offset : Abstract_interp.Int.t ->
precise_offset -> precise_offset
val shift_offset_by_singleton : Abstract_interp.Int.t ->
precise_offset -> precise_offset
val shift_offset : Ival.t -> precise_offset -> precise_offset
type
precise_location_bits =
| |
PLBottom |
| |
PLLoc of Locations.Location_Bits.t |
| |
PLVarOffset of Base.t * precise_offset |
| |
PLLocOffset of Locations.Location_Bits.t * precise_offset |
val pretty_loc : Format.formatter -> precise_location_bits -> unit
val bottom_location_bits : precise_location_bits
val cardinal_zero_or_one_location_bits : precise_location_bits -> bool
val inject_location_bits : Locations.Location_Bits.t -> precise_location_bits
val combine_base_precise_offset : Base.t -> precise_offset -> precise_location_bits
val combine_loc_precise_offset : Locations.Location_Bits.t ->
precise_offset -> precise_location_bits
val imprecise_location_bits : precise_location_bits -> Locations.Location_Bits.t
type
precise_location = {
}
val imprecise_location : precise_location -> Locations.location
val make_precise_loc : precise_location_bits ->
size:Int_Base.t -> precise_location
val loc_size : precise_location -> Int_Base.t
val loc_bottom : precise_location
val is_bottom_loc : precise_location -> bool
val fold_offset : (Ival.t -> 'a -> 'a) -> precise_offset -> 'a -> 'a
val fold : (Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a
val enumerate_valid_bits : for_writing:bool -> precise_location -> Locations.Zone.t
val cardinal_zero_or_one : for_writing:bool -> precise_location -> bool