Module Multidim

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.


type index = 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