Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression

14 files changed, 197 insertions, 90 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index d168e519..045f879a 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1294,6 +1294,7 @@ namespace Microsoft.Dafny {
   public abstract class AssignmentRhs {

     internal AssignmentRhs() {

     }

+    public abstract bool CanAffectPreviouslyKnownExpressions { get; }

   }

 

   public abstract class DeterminedAssignmentRhs : AssignmentRhs {

@@ -1312,6 +1313,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(expr != null);

       Expr = expr;

     }

+    public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }

   }

 

   public class TypeRhs : DeterminedAssignmentRhs {

@@ -1341,9 +1343,22 @@ namespace Microsoft.Dafny {
       EType = type;

       ArrayDimensions = arrayDimensions;

     }

+    public override bool CanAffectPreviouslyKnownExpressions {

+      get {

+        if (InitCall != null) {

+          foreach (var mod in InitCall.Method.Mod) {

+            if (!(mod.E is ThisExpr)) {

+              return true;

+            }

+          }

+        }

+        return false;

+      }

+    }

   }

 

   public class HavocRhs : AssignmentRhs {

+    public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }

   }

 

   public class AssignStmt : Statement {

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 8a6fdd21..6fe3a3c1 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1169,27 +1169,22 @@ namespace Microsoft.Dafny {
             }

           }

         } else if (s.Lhs is FieldSelectExpr) {

-          // LHS is fine, but restrict the RHS to ExprRhs

-          if (!(s.Rhs is ExprRhs)) {

-            Error(stmt, "Assignment to field must have an expression RHS; try using a temporary local variable");

-          } else {

-            FieldSelectExpr fse = (FieldSelectExpr)s.Lhs;

-            if (fse.Field != null) {  // otherwise, an error was reported above

-              lvalueIsGhost = fse.Field.IsGhost;

-              if (!lvalueIsGhost) {

-                if (specContextOnly) {

-                  Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

-                } else {

-                  // It is now that we wish we would have resolved s.Lhs to not allow ghosts.  Too late, so we do

-                  // the next best thing.

-                  if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {

-                    Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");

-                  }

+          FieldSelectExpr fse = (FieldSelectExpr)s.Lhs;

+          if (fse.Field != null) {  // otherwise, an error was reported above

+            lvalueIsGhost = fse.Field.IsGhost;

+            if (!lvalueIsGhost) {

+              if (specContextOnly) {

+                Error(stmt, "Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

+              } else {

+                // It is now that we wish we would have resolved s.Lhs to not allow ghosts.  Too late, so we do

+                // the next best thing.

+                if (lhsResolvedSuccessfully && UsesSpecFeatures(fse.Obj)) {

+                  Error(stmt, "Assignment to non-ghost field is not allowed to use specification-only expressions in the receiver");

                 }

               }

-              if (!fse.Field.IsMutable) {

-                Error(stmt, "LHS of assignment does not denote a mutable field");

-              }

+            }

+            if (!fse.Field.IsMutable) {

+              Error(stmt, "LHS of assignment does not denote a mutable field");

             }

           }

         } else if (s.Lhs is SeqSelectExpr) {

@@ -1204,40 +1199,37 @@ namespace Microsoft.Dafny {
             if (specContextOnly) {

               Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

             }

-          }

-          if (!(s.Rhs is ExprRhs)) {

-            Error(stmt, "Assignment to array element must have an expression RHS; try using a temporary local variable");

+            if (!lhs.SelectOne && !(s.Rhs is ExprRhs)) {

+              Error(stmt, "Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable");

+            }

           }

 

         } else if (s.Lhs is MultiSelectExpr) {

           if (specContextOnly) {

             Error(stmt, "Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");

           }

-          if (!(s.Rhs is ExprRhs)) {

-            Error(stmt, "Assignment to array element must have an expression RHS; try using a temporary local variable");

-          }

 

         } else {

           Error(stmt, "LHS of assignment must denote a mutable variable or field");

         }

         

         s.IsGhost = lvalueIsGhost;

+        Type lhsType = s.Lhs.Type;

+        if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {

+          Contract.Assert(lhsType.IsArrayType);

+          lhsType = UserDefinedType.ArrayElementType(lhsType);

+        }

         if (s.Rhs is ExprRhs) {

           ExprRhs rr = (ExprRhs)s.Rhs;

           ResolveExpression(rr.Expr, true, lvalueIsGhost);

           Contract.Assert(rr.Expr.Type != null);  // follows from postcondition of ResolveExpression

-          Type lhsType = s.Lhs.Type;

-          if (s.Lhs is SeqSelectExpr && !((SeqSelectExpr)s.Lhs).SelectOne) {

-            Contract.Assert(lhsType.IsArrayType);

-            lhsType = UserDefinedType.ArrayElementType(lhsType);

-          }

           if (!UnifyTypes(lhsType, rr.Expr.Type)) {

             Error(stmt, "RHS (of type {0}) not assignable to LHS (of type {1})", rr.Expr.Type, s.Lhs.Type);

           }

         } else if (s.Rhs is TypeRhs) {

           TypeRhs rr = (TypeRhs)s.Rhs;

           Type t = ResolveTypeRhs(rr, stmt, lvalueIsGhost, method);

-          if (!UnifyTypes(s.Lhs.Type, t)) {

+          if (!UnifyTypes(lhsType, t)) {

             Error(stmt, "type {0} is not assignable to LHS (of type {1})", t, s.Lhs.Type);

           }

         } else if (s.Rhs is HavocRhs) {

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index ab9616b9..708c4c06 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -869,35 +869,68 @@ namespace Microsoft.Dafny {
     Method currentMethod = null;  // the method whose implementation is currently being translated

     int loopHeapVarCount = 0;

     int otherTmpVarCount = 0;

-    Bpl.IdentifierExpr _phvie = null;

+    Dictionary<string, Bpl.IdentifierExpr> _tmpIEs = new Dictionary<string, Bpl.IdentifierExpr>();

+    Bpl.IdentifierExpr GetTmpVar_IdExpr(IToken tok, string name, Bpl.Type ty, Bpl.VariableSeq locals)  // local variable that's shared between statements that need it

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(name != null);

+      Contract.Requires(ty != null);

+      Contract.Requires(locals != null);

+      Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);

+

+      Bpl.IdentifierExpr ie;

+      if (_tmpIEs.TryGetValue(name, out ie)) {

+        Contract.Assume(ie.Type.Equals(ty));

+      } else {

+        // the "tok" and "ty" of the first request for this variable is the one we use

+        var v = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name, ty));  // important for the "$nw" client: no where clause (see GetNewVar_IdExpr)

+        locals.Add(v);

+        ie = new Bpl.IdentifierExpr(tok, v);

+        _tmpIEs.Add(name, ie);

+      }

+      return ie;

+    }

+

     Bpl.IdentifierExpr GetPrevHeapVar_IdExpr(IToken tok, Bpl.VariableSeq locals) {  // local variable that's shared between statements that need it

       Contract.Requires(tok != null);

       Contract.Requires(locals != null); Contract.Requires(predef != null);

       Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);

 

-      if (_phvie == null) {

-        // the "tok" of the first request for this variable is the one we use

-        Bpl.LocalVariable prevHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$prevHeap", predef.HeapType));

-        locals.Add(prevHeapVar);

-        _phvie = new Bpl.IdentifierExpr(tok, prevHeapVar);

-      }

-      return _phvie;

+      return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals);

     }

-    Bpl.IdentifierExpr _nwie = null;

+    

     Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Bpl.VariableSeq locals)  // local variable that's shared between statements that need it

     {

       Contract.Requires(tok != null);

       Contract.Requires(locals != null);

       Contract.Requires(predef != null);

       Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);

-    

-      if (_nwie == null) {

-        // the "tok" of the first request for this variable is the one we use

-        Bpl.LocalVariable nwVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, "$nw", predef.RefType));  // important: no where clause (that's why we're going through the trouble of setting of this variable in the first place)

-        locals.Add(nwVar);

-        _nwie = new Bpl.IdentifierExpr(tok, nwVar);

+

+      // important: the following declaration produces no where clause (that's why we're going through the trouble of setting of this variable in the first place)

+      return GetTmpVar_IdExpr(tok, "$nw", predef.RefType, locals);

+    }

+

+    /// <summary>

+    /// Returns an expression whose value is the same as "expr", but that is guaranteed to preserve the its value passed

+    /// the evaluation of "rhs".  If necessary, a new local variable called "name" with type "ty" is added to "locals" and

+    /// assigned in "builder" to be used to hold the value of "expr".  It is assumed that all requests for a given "name"

+    /// have the same type "ty" and that these variables can be shared.

+    /// </summary>

+    Bpl.Expr SaveInTemp(Bpl.Expr expr, AssignmentRhs rhs, string name, Bpl.Type ty, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals) {

+      Contract.Requires(expr != null);

+      Contract.Requires(rhs != null);

+      Contract.Requires(name != null);

+      Contract.Requires(ty != null);

+      Contract.Requires(locals != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      if (rhs.CanAffectPreviouslyKnownExpressions) {

+        var save = GetTmpVar_IdExpr(expr.tok, name, ty, locals);

+        builder.Add(Bpl.Cmd.SimpleAssign(expr.tok, save, expr));

+        return save;

+      } else {

+        return expr;

       }

-      return _nwie;

     }

 

     void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc)

@@ -906,8 +939,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(proc != null);

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(wellformednessProc || m.Body != null);

-      Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null);

-      Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _phvie == null && _nwie == null);

+      Contract.Requires(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);

+      Contract.Ensures(currentMethod == null && loopHeapVarCount == 0 && _tmpIEs.Count == 0);

     

       currentMethod = m;

 

@@ -974,8 +1007,7 @@ namespace Microsoft.Dafny {
       currentMethod = null;

       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

-      _phvie = null;

-      _nwie = null;

+      _tmpIEs.Clear();

     }

 

     void GenerateImplPrelude(Method m, Bpl.VariableSeq inParams, Bpl.VariableSeq outParams,

@@ -2436,8 +2468,7 @@ namespace Microsoft.Dafny {
       currentMethod = m;

       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

-      _phvie = null;

-      _nwie = null;

+      _tmpIEs.Clear();

             

       //  call inlined m;

       TrStmt(m.Body, builder, localVariables, etran);

@@ -2459,8 +2490,7 @@ namespace Microsoft.Dafny {
       currentMethod = null;

       loopHeapVarCount = 0;

       otherTmpVarCount = 0;

-      _phvie = null;

-      _nwie = null;

+      _tmpIEs.Clear();

       

       // assert output variables of r and m are pairwise equal

       Contract.Assert(outParams.Length % 2 == 0);

@@ -3659,7 +3689,7 @@ namespace Microsoft.Dafny {
       } else if (lhs is FieldSelectExpr) {

         var fse = (FieldSelectExpr)lhs;

         Contract.Assert(fse.Field != null);

-        var obj = etran.TrExpr(fse.Obj); // TODO: save this value in a variable, if needed

+        var obj = SaveInTemp(etran.TrExpr(fse.Obj), rhs, "$obj", predef.RefType, builder, locals);

         // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj]);

         builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, GetField(fse)), "assignment may update an object not in the enclosing method's modifies clause"));

 

@@ -3676,8 +3706,8 @@ namespace Microsoft.Dafny {
         Contract.Assert(sel.Seq.Type != null && sel.Seq.Type.IsArrayType);

         if (sel.SelectOne) {

           Contract.Assert(sel.E0 != null);

-          var obj = etran.TrExpr(sel.Seq); // TODO: save this value in a variable, if needed

-          Bpl.Expr fieldName = FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0)); // TODO: save this value in a variable, if needed

+          var obj = SaveInTemp(etran.TrExpr(sel.Seq), rhs, "$obj", predef.RefType, builder, locals);

+          var fieldName = SaveInTemp(FunctionCall(tok, BuiltinFunction.IndexField, null, etran.TrExpr(sel.E0)), rhs, "$index", predef.FieldName(tok, predef.BoxType), builder, locals);

           // check that the enclosing modifies clause allows this object to be written:  assert $_Frame[obj,index]);

           builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));

 

@@ -3690,9 +3720,9 @@ namespace Microsoft.Dafny {
           builder.Add(AssumeGoodHeap(tok, etran));

 

         } else {

-          var obj = etran.TrExpr(sel.Seq); // TODO: save this value in a variable, if needed

-          Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0); // TODO: save this value in a variable, if needed

-          Bpl.Expr high = sel.E1 == null ? ArrayLength(tok, obj, 1, 0) : etran.TrExpr(sel.E1); // TODO: save this value in a variable, if needed

+          var obj = etran.TrExpr(sel.Seq);

+          Bpl.Expr low = sel.E0 == null ? Bpl.Expr.Literal(0) : etran.TrExpr(sel.E0);

+          Bpl.Expr high = sel.E1 == null ? ArrayLength(tok, obj, 1, 0) : etran.TrExpr(sel.E1);

           // check frame:

           // assert (forall i: int :: low <= i && i < high ==> $_Frame[arr,i]);

           Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));

@@ -3714,8 +3744,8 @@ namespace Microsoft.Dafny {
         MultiSelectExpr mse = (MultiSelectExpr)lhs;

         Contract.Assert(mse.Array.Type != null && mse.Array.Type.IsArrayType);

 

-        var obj = etran.TrExpr(mse.Array); // TODO: save this value in a variable, if needed

-        Bpl.Expr fieldName = etran.GetArrayIndexFieldName(mse.tok, mse.Indices); // TODO: save this value in a variable, if needed

+        var obj = SaveInTemp(etran.TrExpr(mse.Array), rhs, "$obj", predef.RefType, builder, locals);

+        var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhs, "$index", predef.FieldName(mse.tok, predef.BoxType), builder, locals);

         builder.Add(Assert(tok, Bpl.Expr.SelectTok(tok, etran.TheFrame(tok), obj, fieldName), "assignment may update an array element not in the enclosing method's modifies clause"));

 

         Bpl.Expr bRhs = TrAssignmentRhs(tok, null, null, rhs, builder, locals, etran);

diff --git a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
index cf109c1a..df8cb1b7 100644
--- a/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
+++ b/Test/VSComp2010/Problem5-DoubleEndedQueue.dfy
@@ -30,10 +30,8 @@ class AmortizedQueue<T> {
     modifies this;

     ensures Valid() && List == [];

   {

-    var tmp := new LinkedList<T>.Init();

-    front := tmp;

-    tmp := new LinkedList<T>.Init();

-    rear := tmp;

+    front := new LinkedList<T>.Init();

+    rear := new LinkedList<T>.Init();

     Repr := {this};

     Repr := Repr + front.Repr + rear.Repr;

     List := [];

@@ -52,8 +50,7 @@ class AmortizedQueue<T> {
       call ff := f.Concat(rr);

       front := ff;

 

-      var tmp := new LinkedList<T>.Init();

-      rear := tmp;

+      rear := new LinkedList<T>.Init();

     }

     Repr := {this};

     Repr := Repr + front.Repr + rear.Repr;

@@ -79,8 +76,7 @@ class AmortizedQueue<T> {
     ensures r != null && r.Valid() && r.List == List + [item];

   {

     call rr := rear.Cons(item);

-    var tmp := new AmortizedQueue<T>.InitFromPieces(front, rr);

-    r := tmp;

+    r := new AmortizedQueue<T>.InitFromPieces(front, rr);

   }

 }

 

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 02c1a63a..3438d6e0 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -48,7 +48,7 @@ class Glossary {
     var rs:= new ReaderStream;

     call rs.Open();

     var glossary := new Map<Word,seq<Word>>.Init();

-    var q:= new Queue<Word>.Init();

+    var q := new Queue<Word>.Init();

     

     while (true)

       invariant rs.Valid() && fresh(rs.footprint);

diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy
new file mode 100644
index 00000000..b73af758
--- /dev/null
+++ b/Test/dafny0/AdvancedLHS.dfy
@@ -0,0 +1,59 @@
+class C {

+  var x: C;

+

+  method M(S: set<C>, a: array<C>, b: array2<C>)

+    requires S != {};

+    modifies this, a, b;

+  {

+    x := new C;

+    x := new C.Init();

+    havoc x;

+    x := choose(S);

+

+    // test evaluation order

+    var c := x;

+    x := null;

+    x := new C.InitOther(x);  // since the parameter is evaluated before the LHS is set, the precondition is met

+    assert x != c;

+

+    // test evaluation order and modification

+    if (*) {

+      var k := this.x;

+      var kx := this.x.x;

+      this.x.x := new C.InitAndMutate(this);

+      assert this.x == null;

+      assert this.x != k;

+      assert k.x != kx;  // because it was set to a new object

+      assert fresh(k.x);

+    } else {

+      var k := this.x;

+      var kx := this.x.x;

+      this.x.x := new C.InitAndMutate(this);

+      var t := this.x.x;  // error: null dereference (because InitAndMutate set this.x to null)

+    }

+

+    if (a != null && 10 <= a.Length) {

+      a[2] := new C;

+      a[4..8] := null;

+      havoc a[3];

+    }

+    if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {

+      b[2,14] := new C;

+      havoc b[3,11];

+    }

+  }

+

+  method Init() { }

+  method InitOther(c: C)

+    requires c == null;

+  {

+    var d := new int[if c == null then 10 else -3];  // run-time error if c were non-null, but it ain't

+  }

+  method InitAndMutate(c: C)

+    requires c != null;

+    modifies c;

+    ensures c.x == null;

+  {

+    c.x := null;

+  }

+}

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index f57c6ead..eb85403e 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -81,7 +81,9 @@ TypeTests.dfy(69,8): Error: Duplicate local-variable name: x
 TypeTests.dfy(72,6): Error: Duplicate local-variable name: y

 TypeTests.dfy(79,17): Error: member F in class C does not refer to a method

 TypeTests.dfy(80,17): Error: a method called as an initialization method must not have any result arguments

-16 resolution/type errors detected in TypeTests.dfy

+TypeTests.dfy(89,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+TypeTests.dfy(90,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable

+18 resolution/type errors detected in TypeTests.dfy

 

 -------------------- SmallTests.dfy --------------------

 SmallTests.dfy(30,11): Error: index out of range

@@ -418,6 +420,14 @@ NonGhostQuantifiers.dfy(103,8): Error: quantifiers in non-ghost contexts must be
 NonGhostQuantifiers.dfy(120,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

 8 resolution/type errors detected in NonGhostQuantifiers.dfy

 

+-------------------- AdvancedLHS.dfy --------------------

+AdvancedLHS.dfy(32,23): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon15_Else

+

+Dafny program verifier finished with 7 verified, 1 error

+

 -------------------- Modules0.dfy --------------------

 Modules0.dfy(7,8): Error: Duplicate name of top-level declaration: T

 Modules0.dfy(13,7): Error: module T named among imports does not exist

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 048ecd7a..60854f63 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -37,10 +37,10 @@ class A {
   method O() {

     var zz2 := new A[25];

     assert zz2 != zz0;  // holds because zz2 is newly allocated

-    /******  These would be good things to be able to verify, but the current encoding is not up to the task

     var o: object := zz0;

     assert this != o;  // holds because zz0 has a different type

-    if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) {

+    /******  This would be a good thing to be able to verify, but the current encoding is not up to the task

+    if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) {

       o := zz1[1];

       assert zz0[1] == o ==> o == null;  // holds because zz0 and zz1 have different element types

     }

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index cbab53bf..93c4aec4 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -80,3 +80,12 @@ method InitCalls() {
   var d := new C.M(8);  // error: M has out parameters

   var e := new C.Caller();

 }

+

+// ---------------------

+

+method ArrayRangeAssignments(a: array<C>)

+  requires a != null && 10 <= a.Length;

+{

+  a[0..5] := new C;  // this is not allowed

+  havoc a[1..4];  // this is not allowed

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2c55a6b9..6a2f2cb5 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -12,7 +12,7 @@ for %%f in (Simple.dfy) do (
 )

 

 for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.dfy

-            Array.dfy MultiDimArray.dfy NonGhostQuantifiers.dfy

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

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

             TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index b790eea5..4ceca552 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -39,7 +39,7 @@ class ExtensibleArray<T> {
     ensures Valid() && fresh(Repr - {this});

     ensures Contents == [];

   {

-    var arr := new T[256];  elements := arr;

+    elements := new T[256];

     more := null;

     length := 0;

     M := 0;

@@ -90,15 +90,14 @@ class ExtensibleArray<T> {
       elements[length - M] := t;

     } else {

       if (more == null) {

-        var mr := new ExtensibleArray<array<T>>.Init();

-        more := mr;

-        Repr := Repr + {mr} + mr.Repr;

+        more := new ExtensibleArray<array<T>>.Init();

+        Repr := Repr + {more} + more.Repr;

       }

       // "elements" is full, so move it into "more" and allocate a new array

       call more.Append(elements);

       Repr := Repr + more.Repr;

       M := M + 256;

-      var arr := new T[256];  elements := arr;

+      elements := new T[256];

       Repr := Repr + {elements};

       elements[0] := t;

     }

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 957eb7cb..db1c60fa 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -27,8 +27,7 @@ class PriorityQueue {
     ensures N == capacity;

   {

     N := capacity;

-    var arr := new int[N+1];

-    a := arr;

+    a := new int[N+1];

     n := 0;

     Repr := {this};

     Repr := Repr + {a};

@@ -143,8 +142,7 @@ class PriorityQueue_Alternative {
     ensures N == capacity;

   {

     N := capacity;

-    var arr := new int[N+1];

-    a := arr;

+    a := new int[N+1];

     n := 0;

     Repr := {this};

     Repr := Repr + {a};

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 940e1a0a..dfc10327 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
     ensures IsUnboundedStack();

     ensures content == [val] + old(content);

   {

-    var tmp := new Node<T>.InitNode(val,top);

-    top := tmp;

+    top := new Node<T>.InitNode(val,top);

     representation := representation + top.footprint;

     content := [val] + content;

   }

diff --git a/Test/vacid0/LazyInitArray.dfy b/Test/vacid0/LazyInitArray.dfy
index fc4d687d..e56a8317 100644
--- a/Test/vacid0/LazyInitArray.dfy
+++ b/Test/vacid0/LazyInitArray.dfy
@@ -41,9 +41,9 @@ class LazyInitArray<T> {
     ensures |Contents| == N && Zero == zero;

     ensures (forall x :: x in Contents ==> x == zero);

   {

-    var aa := new T[N+1];  a := aa;

-    var ii := new int[N];  b := ii;

-    ii := new int[N];      c := ii;

+    a := new T[N+1];

+    b := new int[N];

+    c := new int[N];

     n := 0;

 

     // initialize ghost variable Contents to a sequence of length N containing only zero's,