module Precise_locs: sig
.. end
This module provides 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.
Precise offsets
type
precise_offset
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 imprecise_offset : precise_offset -> Ival.t
val shift_offset_by_singleton : Integer.t -> precise_offset -> precise_offset
val shift_offset : Ival.t -> precise_offset -> precise_offset
Precise location_bits
type
precise_location_bits
val pretty_loc_bits : Format.formatter -> precise_location_bits -> unit
val bottom_location_bits : precise_location_bits
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
Precise locations
type
precise_location
val loc_size : precise_location -> Int_Base.t
val make_precise_loc : precise_location_bits ->
size:Int_Base.t -> precise_location
val imprecise_location : precise_location -> Locations.location
val loc_bottom : precise_location
val is_bottom_loc : precise_location -> bool
val fold : (Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a
val enumerate_valid_bits : for_writing:bool -> precise_location -> Locations.Zone.t
val valid_cardinal_zero_or_one : for_writing:bool -> precise_location -> bool
Is the restriction of the given location to its valid part precise enough
to perform a strong read, or a strong update.
val cardinal_zero_or_one : precise_location -> bool
val pretty_loc : precise_location Pretty_utils.formatter