diff options
Diffstat (limited to 'Test/dafny0/Matrix-OOB.dfy.expect')
| -rw-r--r-- | Test/dafny0/Matrix-OOB.dfy.expect | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/dafny0/Matrix-OOB.dfy.expect b/Test/dafny0/Matrix-OOB.dfy.expect index 94e77aa4..e2920445 100644 --- a/Test/dafny0/Matrix-OOB.dfy.expect +++ b/Test/dafny0/Matrix-OOB.dfy.expect @@ -1,3 +1,4 @@ +Matrix-OOB.dfy(12,10): Info: Selected triggers: {m[i, j]}
Matrix-OOB.dfy(12,26): Error: index 0 out of range
Execution trace:
(0,0): anon0
@@ -6,6 +7,7 @@ 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.
+Matrix-OOB.dfy(12,33): Related location
Execution trace:
(0,0): anon0
|