module Multidim:sig
..end
offset
is an abstraction for array indexes when these
arrays are used as a representation of multidimensional arrays or
structures. They have the form :
o + d₁×0,b₁
+ ... + dₙ×0,bₙ
or, more formally
{ o + Σ dᵢ×xᵢ | ∀i 1≤i≤n ⇒ xᵢ ∊ 0, bᵢ
}
This is a generalisation of integers intervals with modulo implemented in
Ival : o + d×0, b
The list of dᵢ is sorted in descending order and we may add the constraint
dᵢ×bᵢ < dᵢ₋₁
which is verified for normal multidimensional arrays handling.
typeindex =
Integer.t * (Integer.t * Integer.t) list
include Datatype.S
val zero : t
val of_int : int -> t
val of_integer : Integer.t -> t
val of_ival : Ival.t -> t
val is_zero : t -> bool
val is_singleton : t -> bool
val hull : t -> Integer.t * Integer.t
val first_dimension : t -> (Integer.t * t) option
val add : t -> t -> t
val add_int : t -> int -> t
val add_integer : t -> Integer.t -> t
val sub_int : t -> int -> t
val sub_integer : t -> Integer.t -> t
val mul : t -> t -> t
val mul_int : t -> int -> t
val mul_integer : t -> Integer.t -> t
val mod_int : t -> int -> t
val mod_integer : t -> Integer.t -> t
val of_exp : (Cil_types.exp -> t) -> Cil_types.exp -> t
val of_offset : (Cil_types.exp -> t) -> Cil_types.typ -> Cil_types.offset -> t