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

1 files changed, 15 insertions, 0 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index d168e519..045f879a 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/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 {