Dafny: forbid "decreases *" on ghost loops

3 files changed, 24 insertions, 2 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 1ac8fc1c..cd531472 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -391,6 +391,10 @@ Execution trace:
 

 Dafny program verifier finished with 3 verified, 3 errors

 

+-------------------- ResolutionErrors.dfy --------------------

+ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

+1 resolution/type errors detected in ResolutionErrors.dfy

+

 -------------------- Array.dfy --------------------

 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
new file mode 100644
index 00000000..b105a5c0
--- /dev/null
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -0,0 +1,18 @@
+method UmmThisIsntGoingToWork()

+{

+   var a := new int [2];

+   var b := new int [1];

+   a[0] := 1;

+   a[1] := -1;

+

+   ghost var i := 0;

+   while (i < 2)

+      decreases *;  // error: not allowed on a ghost loop

+      invariant i <= 2;

+      invariant forall j :: 0 <= j && j < i ==> a[j] > 0;

+   {

+      i := 0;

+   }

+   assert a[1] == -1;  // ...for then this would incorrectly verify

+   b[a[1]] := 0;

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 491b7b75..12d9bcf4 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -11,8 +11,8 @@ for %%f in (Simple.dfy) do (
   %DAFNY_EXE% %* /dprint:- /env:0 /noVerify %%f

 )

 

-for %%f in (TypeTests.dfy NatTypes.dfy  SmallTests.dfy Definedness.dfy

-            FunctionSpecifications.dfy

+for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy

+            FunctionSpecifications.dfy ResolutionErrors.dfy

             Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy AdvancedLHS.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy