package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c.kernel/Frama_c_kernel/Locations/index.html

Module `Frama_c_kernel.Locations`

Memory locations.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

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;

}

A Location_Bits.t and a size in bits.

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

module Location : Datatype.S with type t = location

val loc_top : 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 : 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 : access -> location -> Zone.t

see https://frama-c.com/download/frama-c-plugin-development-guide.pdf

val enumerate_valid_bits_under : access -> 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

On This Page

Locations
Conversion functions