Frama-C:
Plug-ins:
Libraries:

Frama-C API - Multidim

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.

include Frama_c_kernel.Datatype.S with type t = index
include Frama_c_kernel.Datatype.S_no_copy with type t = index
include Frama_c_kernel.Datatype.Ty with type t = index
type t = index
val datatype_name : string

Unique name of the datatype.

val datatype_descr : t Frama_c_kernel.Descr.t

Datatype descriptor.

Packed version of the descriptor.

val reprs : t list

List of representants of the descriptor.

val equal : t -> t -> bool

Equality: same spec than Stdlib.(=).

val compare : t -> t -> int

Comparison: same spec than Stdlib.compare.

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 : (Frama_c_kernel.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 copy : t -> t

Deep copy: no possible sharing between x and copy x.

val zero : t
val of_int : int -> t
val of_integer : Frama_c_kernel.Z.t -> t
val of_ival : Frama_c_kernel.Ival.t -> t
val is_zero : t -> bool
val is_singleton : t -> bool
val first_dimension : t -> (Frama_c_kernel.Z.t * t) option
val add : t -> t -> t
val add_int : t -> int -> t
val add_integer : t -> Frama_c_kernel.Z.t -> t
val sub_int : t -> int -> t
val sub_integer : t -> Frama_c_kernel.Z.t -> t
val mul : t -> t -> t
val mul_int : t -> int -> t
val mul_integer : t -> Frama_c_kernel.Z.t -> t
val mod_int : t -> int -> t
val mod_integer : t -> Frama_c_kernel.Z.t -> t