blob: e29204452fbbf16a60f05300330c97ba8092b071 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
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
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.
Matrix-OOB.dfy(12,33): Related location
Execution trace:
(0,0): anon0
Dafny program verifier finished with 0 verified, 3 errors
|
