diff options
| author |  rustanleino <unknown> | 2010-09-14 20:09:39 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-09-14 20:09:39 +0000 |
| commit | b32f277e00ed5c3f90d01c17bcce0d8855eadfff (patch) | |
| tree | 1ad4937527994439ad707a4938b1492bf29da08b /Test/stratifiedinline | |
| parent | 90b3510c18c03531386e45bab091ecc943ef1005 (diff) | |
Dafny:
* Added internal support for multi-dimensional arrays (but not all surface syntax is there yet)
* Removed unused variables from Dafny.atg
Boogie and Dafny:
* Improved error message for postcondition violations
Diffstat (limited to 'Test/stratifiedinline')
| -rw-r--r-- | Test/stratifiedinline/Answer | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/stratifiedinline/Answer b/Test/stratifiedinline/Answer index aa83b37c..290059d6 100644 --- a/Test/stratifiedinline/Answer +++ b/Test/stratifiedinline/Answer @@ -1,5 +1,5 @@ ----- Running regression test bar1.bpl
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold at this return statement.
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar1.bpl(24,3): anon0
@@ -31,7 +31,7 @@ Execution trace: Boogie program verifier finished with 0 verified, 1 error
-----
----- Running regression test bar3.bpl
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold at this return statement.
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
Execution trace:
bar3.bpl(38,3): anon0
|