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

1 files changed, 59 insertions, 0 deletions

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;

+  }

+}