Frama_c_kernel.Tr_offsetReduction 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 | (*
|
| Overlap of Integer.t * Integer.t * Origin.t | (*
|
val pretty : t Pretty_utils.formatterval trim_by_validity :
?origin:Origin.t ->
Ival.t ->
Integer.t ->
Base.validity ->
ttrim_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
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_validstart_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.