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/Precise_locs/index.html

Module `Frama_c_kernel.Precise_locs`

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 equal_offset : precise_offset -> precise_offset -> bool

val offset_zero : precise_offset

val offset_bottom : precise_offset

val offset_top : precise_offset

val inject_ival : Ival.t -> 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 equal_loc : precise_location -> precise_location -> bool

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 loc_top : precise_location

val is_top_loc : precise_location -> bool

val replace_base : Base.substitution -> precise_location -> precise_location

val fold : (Locations.location -> 'a -> 'a) -> precise_location -> 'a -> 'a

val enumerate_valid_bits : 
  Locations.access ->
  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, valid_cardinal_zero_or_one is almost always more useful

val pretty_loc : precise_location Pretty_utils.formatter

val valid_part : 
  Locations.access ->
  bitfield:bool ->
  precise_location ->
  precise_location

Overapproximation of the valid part of the given location (without any access, or for a read or write access). 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.

On This Page

Precise offsets
Precise location_bits
Precise locations