Module Precise_locs

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 = {
   loc : precise_location_bits;
   size : Int_Base.t;
}
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