blob: 2e5c0366ffc1c7d2a0acb5afd4ed505530d85170 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This is a regression test: OOB errors for matrices used to be reported on the
// quantifier that introduced the variables that constituted the invalid indices.
// WISH: It would be even better to report the error on the variables inside the
// array instead of the array itself.
method M(m: array2<int>)
requires m != null
ensures forall i, j :: m[i, j] == 0
{ }
|