package frama-c

  1. Overview
  2. Docs

Module Wp.MatrixSource

Sourcetype t

Matrix dimensions. Encodes the number of dimensions and their kind

Sourceval of_dims : int option list -> t
Sourceval compare : t -> t -> int
Sourceval pretty : Format.formatter -> t -> unit
Sourceval pp_suffix_id : Format.formatter -> t -> unit
Sourceval merge : int option list -> int option list -> int option list option
Sourcetype env = {
  1. size_var : Lang.F.var list;
    (*

    size variables

    *)
  2. size_val : Lang.F.term list;
    (*

    size values

    *)
  3. index_var : Lang.F.var list;
    (*

    index variables

    *)
  4. index_val : Lang.F.term list;
    (*

    index values

    *)
  5. index_range : Lang.F.pred list;
    (*

    indices are in range of size variables

    *)
  6. index_offset : Lang.F.term list;
    (*

    polynomial of indices

    *)
  7. length : Lang.F.term option;
    (*

    number of cells (None is infinite)

    *)
}
Sourceval cc_tau : Lang.F.tau -> t -> Lang.F.tau

Type of matrix

Sourceval cc_env : t -> env

Dimension environment

Sourceval cc_dims : int option list -> Lang.F.term list

Value of size variables