package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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
  1. | Invalid
    (*

    No location is valid

    *)
  2. | Set of Integer.t list
    (*

    Limited number of locations

    *)
  3. | Interval of Integer.t * Integer.t * Integer.t
    (*

    Interval(min, max, modulo)

    *)
  4. | Overlap of Integer.t * Integer.t * Origin.t option
    (*

    Overlap(min, max, origin)

    • origin: the location covers the entire range min..max, but consecutive offsets overlap
    *)
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.
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct