diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-07 07:55:01 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-07 07:55:01 -0800 |
| commit | d8d1996a574c972b24216f9bfd922cc215df2668 (patch) | |
| tree | 6491c87cf916be40d9fbeb4836416e91203c5943 /Test | |
| parent | 714f99d776c21d8a1b50e0020eb678414a0cf67d (diff) | |
| parent | a1fa34eaba18abe4d6c7e610d939806332930ead (diff) | |
Merge
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 12 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 20 |
2 files changed, 29 insertions, 3 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index aab1990d..fdfdf823 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
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index d4a0ad9a..2074e484 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -359,6 +359,16 @@ method {:verify false} test1() assert false;
}
+function test2() : bool
+{
+ !test2() // error
+}
+
+function {:verify false} test3() : bool
+{
+ !test3()
+}
+
class Test {
method test0()
@@ -381,4 +391,14 @@ class Test { assert false;
}
+ function test2() : bool
+ {
+ !test2() // error
+ }
+
+ function {:verify false} test3() : bool
+ {
+ !test3()
+ }
+
}
|