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 (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.1-Cobalt.tar.gz

sha256=5b13574a16a58971c27909bee94ae7f37b17d897852b40c768a3d4e2e09e39d2

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

Module `Frama_c_kernel.Tr_offset`

Reduction of a location (expressed as an Ival.t and a size) by a base validity. Only the locations in the trimmed result are valid. All offsets are expressed in bits.

type t = private

| Invalid
(*
No location is valid
*)
| Set of Integer.t list
(*
Limited number of locations
*)
| Interval of Integer.t * Integer.t * Integer.t
(*
Interval(min, max, modulo)
*)
| Overlap of Integer.t * Integer.t * Origin.t
(*
Overlap(min, max, origin)
- origin: the location covers the entire range min..max, but consecutive offsets overlap
*)

val pretty : t Pretty_utils.formatter

val trim_by_validity : 
  ?origin:Origin.t ->
  Ival.t ->
  Integer.t ->
  Base.validity ->
  t

trim_by_validity ?origin offsets size validity reduces offsets so that all accesses to offsets+(0..size-1) are valid according to validity. For a size of 0, consider the offsets up to the validity past-one valid. If the valid offsets cannot be represented precisely, the Overlap constructor is returned. When specified, the origin argument is used as the source of this imprecision .

This is a more complete specification of this function, for a single offset o. We want to write size>0 bits, on a base possibly valid between min_valid..max_maybe_valid, and guaranteed to be valid between min_valid..max_sure_valid. The case max_sure_valid < min_valid is possible: in this case, no bit is guaranteed to be valid. For Valid and non-Empty bases, min_valid<max_maybe_valid holds. We write start_to==o and stop_to==start_to+size-1. Then

If start_to..stop_to is not included in min_valid..max_maybe_valid, then the write completely fails: at least one bit is outside the validity. This translates to start_to<min_valid || stop_to > max_maybe_valid

If start_to..stop_to is not included in min_valid..max_sure_valid, then we must emit an alarm. This translates to start_to<min_valid || stop_to > max_sure_valid. This convention works even when min_valid..max_sure_valid is not a real interval.