Started fixing a number of LL(1) warnings

Disallow empty modifies/reads clauses (this eliminates some LL(1) warnings)
Require modify statement to take a nonempty list of frame expressions

1 files changed, 5 insertions, 5 deletions

diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy
index 5c258fde..7cf62e32 100644
--- a/Test/dafny0/LoopModifies.dfy
+++ b/Test/dafny0/LoopModifies.dfy
@@ -43,7 +43,7 @@ method Testing3(a: array<int>)
    var i := 0;

    while(i < 10) 

       invariant 0 <= i <= 10;

-      modifies;

+      modifies {};

    {

       a[0] := i; // ERROR

       i := i + 1;

@@ -58,7 +58,7 @@ method Testing4(a: array<int>)
    var i := 0;

    while(i < 10) 

       invariant 0 <= i <= 10;

-      modifies;

+      modifies {};

    {

       a[0] := i; // ERROR

       i := i + 1;

@@ -70,7 +70,7 @@ method Testing4(a: array<int>)
 // modifies not a subset:

 method Testing5(a: array<int>)

    requires a != null && a.Length > 0;

-   modifies;

+   modifies {};

 {

    var i := 0;

    while(i < 10) // ERROR

@@ -249,14 +249,14 @@ method Testing11()
    var arr := new int[1];

    while(i < 10) 

       invariant 0 <= i <= 10;

-      modifies;

+      modifies {};

    {

       arr := new int[1];

       arr[0] := 1;

       var j := 0;

       while(j < 10) 

          invariant 0 <= j <= 10;

-         modifies;

+         modifies {};

       {

          // can't touch arr in here.

          j := j + 1;