diff options
| author |  Rustan Leino <unknown> | 2013-01-23 18:13:36 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-01-23 18:13:36 -0800 |
| commit | 1005adb004baf133b265eda5bfdc53022437e6ef (patch) | |
| tree | b2fd13051b5f484a79a9b2303404aafc2da5858f /Test | |
| parent | 967bd4d7a4223d710f8f10659cdced173b249eac (diff) | |
Fixed bug in translation of method termination checks, and also fixed a (previously undetected) specification bug in the test suite.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Termination.dfy | 16 | ||||
| -rw-r--r-- | Test/dafny1/ExtensibleArray.dfy | 2 |
3 files changed, 18 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e3e513a4..cd5529fe 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1093,7 +1093,7 @@ Execution trace: Termination.dfy(291,3): anon12_Else
(0,0): anon13_Else
-Dafny program verifier finished with 57 verified, 7 errors
+Dafny program verifier finished with 59 verified, 7 errors
-------------------- DTypes.dfy --------------------
DTypes.dfy(15,14): Error: assertion violation
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 83baade1..45520b4a 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -410,3 +410,19 @@ module MapTests { {
}
}
+
+// --------------------- The following regression test case relies on the previous rank
+// --------------------- really being evaluated in the initial state
+
+class C {
+ var v: nat;
+ method Terminate()
+ modifies this;
+ decreases v;
+ {
+ if (v != 0) {
+ v := v - 1;
+ Terminate();
+ }
+ }
+}
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy index 405f3e15..a16cf603 100644 --- a/Test/dafny1/ExtensibleArray.dfy +++ b/Test/dafny1/ExtensibleArray.dfy @@ -83,7 +83,7 @@ class ExtensibleArray<T> { modifies Repr;
ensures Valid() && fresh(Repr - old(Repr));
ensures Contents == old(Contents) + [t];
- decreases Repr;
+ decreases Contents;
{
if (length == 0 || length % 256 != 0) {
// there is room in "elements"
|