module Locations: sig
.. end
module Location_Bytes: sig
.. end
Association between bases and offsets in byte.
module Location_Bits: module type of Location_Bytes
Association between bases and offsets in bits.
module Zone: sig
.. end
Association between bases and ranges of bits.
Locations
type
location = private {
|
loc : Location_Bits.t ; |
|
size : Int_Base.t ; |
}
module Location: Datatype.S
with type t = location
val loc_bottom : location
val is_bottom_loc : location -> bool
val make_loc : Location_Bits.t -> Int_Base.t -> location
val loc_equal : location -> location -> bool
val loc_size : location -> Int_Base.t
val is_valid : for_writing:bool -> location -> bool
Is the given location entirely valid, as the destination of a write
operation if for_writing
is true, as the destination of a read
otherwise.
val is_valid_or_function : location -> bool
Is the location entirely valid for reading, or is it a valid function
pointer.
val valid_part : for_writing:bool -> location -> location
Overapproximation of the valid part of the given location. Beware that
is_valid (valid_part loc)
does not necessarily hold, as garbled mix
are not reduced by valid_part
.
val invalid_part : location -> location
Overapproximation of the invalid part of a location
val cardinal_zero_or_one : location -> bool
Is the location bottom or a singleton?
val valid_cardinal_zero_or_one : for_writing:bool -> location -> bool
Is the valid part of the location bottom or a singleton?
val filter_base : (Base.t -> bool) -> location -> location
val filter_loc : location -> Zone.t -> location
val pretty : Format.formatter -> location -> unit
val pretty_english : prefix:bool -> Format.formatter -> location -> unit
Conversion functions
val loc_to_loc_without_size : location -> Location_Bytes.t
val loc_bytes_to_loc_bits : Location_Bytes.t -> Location_Bits.t
val loc_bits_to_loc_bytes : Location_Bits.t -> Location_Bytes.t
val loc_bits_to_loc_bytes_under : Location_Bits.t -> Location_Bytes.t
val enumerate_bits : location -> Zone.t
val enumerate_bits_under : location -> Zone.t
val enumerate_valid_bits : for_writing:bool -> location -> Zone.t
val enumerate_valid_bits_under : for_writing:bool -> location -> Zone.t
val zone_of_varinfo : Cil_types.varinfo -> Zone.t
Since Carbon-20101201
val loc_of_varinfo : Cil_types.varinfo -> location
val loc_of_base : Base.t -> location
val loc_of_typoffset : Base.t -> Cil_types.typ -> Cil_types.offset -> location