diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-12 17:28:19 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-12 17:28:19 -0700 |
| commit | 81acbf9b3d4cc0662df9e42cf0a4eaeb99c760d3 (patch) | |
| tree | a57d53165043fc2c718eb095a775b146e6a9b3e1 /Test/dafny0 | |
| parent | a1affe2114ae22816cf72d14fb4ae357a64fe7f2 (diff) | |
Dafny: forbid "decreases *" on ghost loops
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 18 | ||||
| -rw-r--r-- | Test/dafny0/runtest.bat | 4 |
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
|