module Locations:sig
..end
Memory locations.
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.
type
location = private {
|
loc : |
|
size : |
A Location_Bits.t
and a size in bits.
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
type
access =
| |
Read |
| |
Write |
| |
No_access |
Kind of memory access.
val base_access : size:Int_Base.t -> access -> Base.access
Conversion into a base access, with the size information. Accesses of unknown sizes are converted into empty accesses.
val is_valid : access -> location -> bool
Is the given location entirely valid, without any access or as a destination for a read or write access.
val valid_part : access ->
?bitfield: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
may not be reduced by valid_part
.
bitfield
indicates whether the location may be the one of a bitfield, and
is true by default. If it is set to false, the location is assumed to be
byte aligned, and its offset (expressed in bits) is reduced to be congruent
to 0 modulo 8.
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 overlaps : partial:bool -> location -> location -> bool
Is there a possibly non-empty intersection between two given locations?
If partial
is true, returns true if the two locations may be overlapping
without being equal. If partial
is false, also returns true if the two
locations may be equal. Returns false when the two locations cannot be
overlapping.
val pretty : Stdlib.Format.formatter -> location -> unit
val pretty_english : prefix:bool -> Stdlib.Format.formatter -> location -> unit
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 : access -> location -> Zone.t
val enumerate_valid_bits_under : access -> location -> Zone.t
val zone_of_varinfo : Cil_types.varinfo -> Zone.t
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