summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2011-05-12 17:28:19 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2011-05-12 17:28:19 -0700
commit81acbf9b3d4cc0662df9e42cf0a4eaeb99c760d3 (patch)
treea57d53165043fc2c718eb095a775b146e6a9b3e1 /Test/dafny0
parenta1affe2114ae22816cf72d14fb4ae357a64fe7f2 (diff)
Dafny: forbid "decreases *" on ghost loops
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/Answer4
-rw-r--r--Test/dafny0/ResolutionErrors.dfy18
-rw-r--r--Test/dafny0/runtest.bat4
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