Module Offsetmap_sig

module Offsetmap_sig: sig .. end

Signature for Offsetmap module, that implement efficient maps from intervals to arbitrary values.

type v

Type of the values stored in the offsetmap

type widen_hint

include Datatype.S

Datatype for the offsetmaps

Pretty-printing

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

val pretty_typ : Cil_types.typ option -> 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 Offsetmap_sig.create, but for values that are isotropic. In this case, size_v is automatically computed.

val of_list : ((t -> v -> t) -> t -> 'l -> t) ->
       'l -> Abstract_interp.Int.t -> t

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.

Empty offsetmap

val empty : t

val is_empty : t -> bool

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 follow:

(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 : 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 ~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.

val iter_on_values : (v -> Abstract_interp.Int.t -> unit) -> t -> unit

iter_on_values f m iterates on the entire contents of m, but f receives only the value bound to each interval and the size of this value. Interval bounds and the offset of the value are not computed.

val fold_on_values : (v -> Abstract_interp.Int.t -> 'a -> 'a) -> t -> 'a -> 'a

Same as iter_on_values but with an accumulator

Join and inclusion testing

val join : t -> t -> t

val is_included : t -> t -> bool

is_included m1 m2 tests whether m1 is included in m2.

val widen : widen_hint -> t -> t -> t

widen wh m1 m2 performs a widening step on m2, assuming that m1 was the previous state. The relation is_included m1 m2 must hold

Searching values

val find : with_alarms:CilE.warn_mode ->
       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.

val find_imprecise_everywhere : t -> v

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

val copy_slice : with_alarms:CilE.warn_mode ->
       validity:Base.validity -> offsets:Ival.t -> size:Integer.t -> t -> t

copy_slice ~with_alarms ~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.

Adding values

val add : 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 Offsetmap_sig.iter. Offsetmaps cannot contain holes, so m must already bind at least the intervals 0..start-1.

exception Result_is_bottom

val update : with_alarms:CilE.warn_mode ->
       validity:Base.validity ->
       exact:bool ->
       offsets:Ival.t -> size:Abstract_interp.Int.t -> v -> t -> t

Can raise Result_is_bottom

val update_imprecise_everywhere : validity:Base.validity -> Origin.t -> v -> t -> t

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 : with_alarms:CilE.warn_mode ->
       validity:Base.validity ->
       exact:bool ->
       t * Abstract_interp.Int.t ->
       size:Abstract_interp.Int.t -> offsets:Ival.t -> t -> t

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 : ?f:(v -> bool) -> t -> bool

is_single_interval ?f o is true if (1) the offsetmap o contains a single binding (2) either f is None, or the bound value v verifies f v.

val single_interval_value : t -> v option

single_interval_value o returns Some v if o contains a single interval, to which v is bound, and None otherwise.

Misc

val clear_caches : unit -> unit

Clear the caches local to this module. Beware that they are not project-aware, and that you must call them at every project switch.