diff options
| author |  wuestholz <unknown> | 2011-12-07 09:54:01 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2011-12-07 09:54:01 +0100 |
| commit | a1fa34eaba18abe4d6c7e610d939806332930ead (patch) | |
| tree | a1035659063ea335ad786f074f76482f55ec75f1 /Test/dafny0/Answer | |
| parent | 8e692b4f59635eae79c83aa13fbf510416ec13b4 (diff) | |
Dafny: Forward attributes on Dafny functions to Boogie (e.g., to disable wellformedness checks).
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 15cec24f..0128f2ae 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -213,12 +213,15 @@ Execution trace: (0,0): anon0
SmallTests.dfy(266,19): anon3_Else
(0,0): anon2
-SmallTests.dfy(366,12): Error: assertion violation
+SmallTests.dfy(376,12): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(376,12): Error: assertion violation
+SmallTests.dfy(386,12): Error: assertion violation
Execution trace:
(0,0): anon0
+SmallTests.dfy(396,6): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
SmallTests.dfy(306,3): Error BP5003: A postcondition might not hold on this return path.
SmallTests.dfy(300,11): Related location: This is the postcondition that might not hold.
Execution trace:
@@ -237,8 +240,11 @@ Execution trace: SmallTests.dfy(354,10): Error: assertion violation
Execution trace:
(0,0): anon0
+SmallTests.dfy(364,4): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon3_Else
-Dafny program verifier finished with 47 verified, 18 errors
+Dafny program verifier finished with 47 verified, 20 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
|