Module Precise_locs

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
Should not be used, Precise_locs.valid_cardinal_zero_or_one is almost always more useful
val pretty_loc : precise_location Pretty_utils.formatter