From 69f54c327bcc5a41a143bce88b5ba2327d7246a7 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:06:17 -0700 Subject: Fix: multi-dimensional OOB errors were sometimes reported on incorrect locations. --- Test/dafny0/Matrix-OOB.dfy | 13 +++++++++++++ Test/dafny0/Matrix-OOB.dfy.expect | 12 ++++++++++++ 2 files changed, 25 insertions(+) create mode 100644 Test/dafny0/Matrix-OOB.dfy create mode 100644 Test/dafny0/Matrix-OOB.dfy.expect (limited to 'Test/dafny0') diff --git a/Test/dafny0/Matrix-OOB.dfy b/Test/dafny0/Matrix-OOB.dfy new file mode 100644 index 00000000..2e5c0366 --- /dev/null +++ b/Test/dafny0/Matrix-OOB.dfy @@ -0,0 +1,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) + requires m != null + ensures forall i, j :: m[i, j] == 0 +{ } diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect new file mode 100644 index 00000000..94e77aa4 --- /dev/null +++ b/Test/dafny0/Matrix-OOB.dfy.expect @@ -0,0 +1,12 @@ +Matrix-OOB.dfy(12,26): Error: index 0 out of range +Execution trace: + (0,0): anon0 +Matrix-OOB.dfy(12,26): Error: index 1 out of range +Execution trace: + (0,0): anon0 +Matrix-OOB.dfy(13,0): Error BP5003: A postcondition might not hold on this return path. +Matrix-OOB.dfy(12,10): Related location: This is the postcondition that might not hold. +Execution trace: + (0,0): anon0 + +Dafny program verifier finished with 0 verified, 3 errors -- cgit v1.2.3