# Frama-C API - `S`

Datatype for the offsetmaps

`include Datatype.S`

`include Datatype.S_no_copy`

`include Datatype.Ty`

### Pretty-printing

`val pretty_generic : ?typ:Cil_types.typ -> ?pretty_v:(Cil_types.typ option -> Stdlib.Format.formatter -> v -> unit) -> ?skip_v:(v -> bool) -> ?sep:string -> unit -> Stdlib.Format.formatter -> t -> unit`

### Creating basic offsetmaps

`val create : size:Abstract_interp.Int.t -> v -> size_v:Abstract_interp.Int.t -> t`

`create ~size v ~size_v`

creates an offsetmap of size `size`

in which the intervals `k*size_v .. (k+1)*size_v-1`

with `0<= k <= size/size_v`

are all mapped to `v`

.

`val create_isotropic : size:Abstract_interp.Int.t -> v -> t`

Same as `create`

, but for values that are isotropic. In this case, `size_v`

is automatically computed.

`from_list fold c size`

creates an offsetmap by applying the iterator `fold`

to the container `c`

, the elements of `c`

being supposed to be of size `size`

. `c`

must be such that `fold`

is called at least once.

`val empty : t`

offsetmap containing no interval.

`val size_from_validity : Base.validity -> Integer.t Lattice_bounds.or_bottom`

`size_from_validity v`

returns the size to be used when creating a new offsetmap for a base with validity `v`

. This is a convention that must be shared by all modules that create offsetmaps, because operations such as `join`

or `is_included`

require offsetmaps of the same . Returns ``Bottom`

iff `v`

is `Base.validity.Invalid`

.

### Iterators

`val iter : ((Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> unit) -> t -> unit`

`iter f m`

calls `f`

on all the intervals bound in `m`

, in increasing order. The arguments of `f (min, max) (v, size, offset)`

are as follows:

`(start, stop)`

are the bounds of the interval, inclusive.`v`

is the value bound to the interval, and`size`

its size; if`size`

is less than`stop-start+1`

,`v`

repeats itself until`stop`

.`offset`

is the offset at which`v`

starts in the interval; it ranges over`0..size-1`

. If`offset`

is`0`

,`v`

starts at the beginning of the interval. Otherwise, it starts at`offset-size`

.

`val fold : ((Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> 'a -> 'a) -> t -> 'a -> 'a`

Same as `iter`

, but with an accumulator.

`val fold_between : ?direction:[ `LTR | `RTL ] -> entire:bool -> (Abstract_interp.Int.t * Abstract_interp.Int.t) -> ((Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> 'a -> 'a) -> t -> 'a -> 'a`

`fold_between ~direction:`LTR ~entire (start, stop) m acc`

is similar to `fold f m acc`

, except that only the intervals that intersect `start..stop`

(inclusive) are presented. If `entire`

is true, intersecting intervals are presented whole (ie. they may be bigger than `start..stop`

). If `entire`

is `false`

, only the intersection with `ib..ie`

is presented. `fold_between ~direction:`RTL`

reverses the iteration order: interval are passed in decreasing order. Default is ``LTR`

.

### Interval-unaware iterators

`iter_on_values f m`

iterates on the entire contents of `m`

, but `f`

receives only the value bound to each interval. Interval bounds, the alignment of the value and its size are not computed.

`map_on_values f m `

creates the map derived from `m`

by applying `f`

to each interval. For each interval, the size of the new value and its offset relative to the beginning of the interval is kept unchanged.

`type map2_decide = `

`| ReturnLeft`

`| ReturnRight`

`| ReturnConstant of v`

`| Recurse`

(*This type describes different possibilities to accelerate a simultaneous iteration on two offsetmaps.

`ReturnLeft`

(resp.`ReturnRight`

) means 'return the left (resp. right) operand unchanged, and stop the recursive descent'.`ReturnConstant v`

means 'return a constant offsetmap of the good size and that contains`v`

everywhere'. It is always correct to return`Recurse`

, which will force the recursion until the maps have been fully decomposed.Typical usage include functions that verify

*)`f v v = v`

, maps`m`

such that`f m m' = m'`

, etc.

`val map2_on_values : Hptmap_sig.cache_type -> (t -> t -> map2_decide) -> (v -> v -> v) -> t -> t -> t`

`map2_on_values cache decide join m1 m2`

applies `join`

pointwise to all the elements of `m1`

and `m2`

and builds the resulting map. This function can only be called if `m1`

and `m2`

contain isotropic values. `decide`

is called during the iteration, and can be used to return early; it is always correct to return `Recurse`

. Depending on `cache`

, the results of the partially applied function `map2_on_values cache decide join`

will be cached between different calls.

### Join and inclusion testing

`include Lattice_type.Join_Semi_Lattice with type t := t`

datatype of element of the lattice

`include Datatype.S with type t := t`

`include Datatype.S_no_copy with type t := t`

`include Datatype.Ty with type t := t`

`val packed_descr : Structural_descr.pack`

Packed version of the descriptor.

`val reprs : t list`

List of representants of the descriptor.

`val hash : t -> int`

Hash function: same spec than `Hashtbl.hash`

.

`val pretty : Stdlib.Format.formatter -> t -> unit`

Pretty print each value in an user-friendly way.

`val mem_project : (Project_skeleton.t -> bool) -> t -> bool`

`mem_project f x`

must return `true`

iff there is a value `p`

of type `Project.t`

in `x`

such that `f p`

returns `true`

.

`val widen : ?hint:widen_hint -> t -> t -> t`

`widen m1 m2`

performs a widening step on `m2`

, assuming that `m1`

was the previous state. The relation `is_included m1 m2`

must hold

### Narrowing

`module Make_Narrow (_ : sig ... end) : sig ... end`

### Searching values

`val find : validity:Base.validity -> ?conflate_bottom:bool -> offsets:Ival.t -> size:Integer.t -> t -> v`

Find the value bound to a set of intervals, expressed as an ival, in the given rangemap.

`val find_imprecise : validity:Base.validity -> t -> v`

`find_imprecise ~validity m`

returns an imprecise join of the values bound in `m`

, in the range described by `validity`

.

Returns an imprecise join of all the values bound in the offsetmap.

`val copy_slice : validity:Base.validity -> offsets:Ival.t -> size:Integer.t -> t -> t Lattice_bounds.or_bottom`

`copy_slice ~validity ~offsets ~size m`

copies and merges the slices of `m`

starting at offsets `offsets`

and of size `size`

. Offsets invalid according to `validity`

are removed. `size`

must be strictly greater than zero.

### Adding values

`val add : ?exact:bool -> (Abstract_interp.Int.t * Abstract_interp.Int.t) -> (v * Abstract_interp.Int.t * Abstract_interp.Rel.t) -> t -> t`

`add (min, max) (v, size, offset) m`

maps the interval `min..max`

(inclusive) to the value `v`

in `m`

. `v`

is assumed as having size `size`

. If `stop-start+1`

is greater than `size`

, `v`

repeats itself until the entire interval is filled. `offset`

is the offset at which `v`

starts in the interval, interpreted as for `iter`

. Offsetmaps cannot contain holes, so `m`

must already bind at least the intervals `0..start-1`

.

`val update : ?origin:Origin.t -> validity:Base.validity -> exact:bool -> offsets:Ival.t -> size:Abstract_interp.Int.t -> v -> t -> t Lattice_bounds.or_bottom`

`update ?origin ~validity ~exact ~offsets ~size v m`

writes `v`

, of size `size`

, each `offsets`

in `m`

; `m`

must be of the size implied by `validity`

. `~exact=true`

results in a strong update, while `~exact=false`

performs a weak update. If `offsets`

contains too many offsets, or if `offsets`

and `size`

are not compatible, `offsets`

and/or `v`

are over-approximated. In this case, `origin`

is used as the source of the resulting imprecision. Returns ``Bottom`

when all offsets are invalid.

`val update_under : validity:Base.validity -> exact:bool -> offsets:Ival.t -> size:Abstract_interp.Int.t -> v -> t -> t Lattice_bounds.or_bottom`

Same as `update`

, except that no over-approximation on the set of offsets or on the value written occurs. In case of imprecision, `m`

is not updated.

`val update_imprecise_everywhere : validity:Base.validity -> Origin.t -> v -> t -> t Lattice_bounds.or_bottom`

`update_everywhere ~validity o v m`

computes the offsetmap resulting from imprecisely writing `v`

potentially anywhere where `m`

is valid according to `validity`

. If a value becomes too imprecise, `o`

is used as origin.

`val paste_slice : validity:Base.validity -> exact:bool -> from:t -> size:Abstract_interp.Int.t -> offsets:Ival.t -> t -> t Lattice_bounds.or_bottom`

### Shape

`val cardinal_zero_or_one : t -> bool`

Returns `true`

if and only if all the interval bound in the offsetmap are mapped to values with cardinal at most 1.

`val is_single_interval : t -> bool`

`is_single_interval o`

is true if the offsetmap `o`

contains a single binding.

`single_interval_value o`

returns `Some v`

if `o`

contains a single interval, to which `v`

is bound, and `None`

otherwise.

`is_same_value o v`

is true if the offsetmap `o`

contains a single binding to `v`

, or is the empty offsetmap.