Frama-C:
Plug-ins:
Libraries:

Frama-C API - Locations

Memory locations.

Locations

type t = private {
  1. addr : Addresses.Bits.t;
  2. size : Z_or_top.t;
}

A Addresses.Bits.t and a size in bits.

include Datatype.S with type t := t
include Datatype.S_no_copy with type t := t
include Datatype.Ty with type t := t
val ty : t Type.t
val datatype_name : string

Unique name of the datatype.

val datatype_descr : t Descr.t

Datatype descriptor.

val packed_descr : Structural_descr.pack

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

val hash : t -> int

Hash function: same spec than Hashtbl.hash.

val mem_project : (Project_skeleton.t -> bool) -> t -> bool

mem_project f x must return true iff there is a value p of type Project.t in x such that f p returns true.

val copy : t -> t

Deep copy: no possible sharing between x and copy x.

val top : t
val bottom : t
val is_bottom : t -> bool
val make : Addresses.Bits.t -> Z_or_top.t -> t
val addr_bytes : t -> Addresses.Bytes.t

addr_bytes l returns the address set corresponding to the given location, i.e. the location without the size information.

  • before 33.0-Arsenic

    was named loc_to_loc_without_size

val size : t -> Z_or_top.t
val is_volatile : t -> bool

is_volatile loc returns false if none of the concrete locations represented by loc are volatile. It returns true if at least one of the represented locations may be volatile.

type access =
  1. | Read
  2. | Write
  3. | Object_pointer
  4. | Any_pointer

Kind of memory access.

val base_access : size:Z_or_top.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 -> t -> 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 -> t -> t

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 : t -> t

Overapproximation of the invalid part of a location

val cardinal_zero_or_one : t -> bool

Is the location bottom or a singleton?

val valid_cardinal_zero_or_one : for_writing:bool -> t -> bool

Is the valid part of the location bottom or a singleton?

val filter_base : (Base.t -> bool) -> t -> t
val overlaps : partial:bool -> t -> t -> 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 -> t -> unit
val pretty_english : prefix:bool -> Stdlib.Format.formatter -> t -> unit

Conversion functions

val enumerate_bits : t -> Memory_zone.t
val enumerate_bits_under : t -> Memory_zone.t
val enumerate_valid_bits : access -> t -> Memory_zone.t
val enumerate_valid_bits_under : access -> t -> Memory_zone.t
val zone_of_varinfo : Cil_types.varinfo -> Memory_zone.t
  • since Carbon-20101201
val of_varinfo : Cil_types.varinfo -> t
val of_base : Base.t -> t
val of_type_offset : Base.t -> Cil_types.typ -> Cil_types.offset -> t

Deprecated

type location = t
  • deprecated Use Locations.t instead
module Location_Bytes = Addresses.Bytes
module Location_Bits = Addresses.Bits
module Zone = Memory_zone
val loc_to_loc_without_size : t -> Addresses.Bytes.t
  • deprecated Use addr_bytes instead
val loc_bytes_to_loc_bits : Addresses.Bytes.t -> Addresses.Bits.t
  • deprecated Use Addresses.Bits.of_bytes instead
val loc_bits_to_loc_bytes : Addresses.Bits.t -> Addresses.Bytes.t
  • deprecated Use Addresses.Bits.to_bytes instead
val loc_bits_to_loc_bytes_under : Addresses.Bits.t -> Addresses.Bytes.t
  • deprecated Use Addresses.Bits.to_bytes_under instead
val loc_top : t
  • deprecated Use top instead
val loc_bottom : t
  • deprecated Use bottom instead
val is_bottom_loc : t -> bool
  • deprecated Use is_bottom instead
val make_loc : Addresses.Bits.t -> Z_or_top.t -> t
  • deprecated Use make instead
val loc_size : t -> Z_or_top.t
  • deprecated Use size instead
val loc_equal : t -> t -> bool
  • deprecated Use equal instead
val loc_of_varinfo : Cil_types.varinfo -> t
  • deprecated Use of_varinfo instead
val loc_of_base : Base.t -> t
  • deprecated Use of_base instead
val loc_of_typoffset : Base.t -> Cil_types.typ -> Cil_types.offset -> t
  • deprecated Use of_type_offset instead