Dafny: allow parallel assignments to assign to the same LHS if the RHS match.

2 files changed, 76 insertions, 11 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 8866491e..bc653bd3 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -808,14 +808,7 @@ Basics.dfy(100,16): Error: assertion violation
 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

-Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location

-Execution trace:

-    (0,0): anon0

-    (0,0): anon3

-    (0,0): anon11_Else

-    (0,0): anon6

-    (0,0): anon12_Then

-Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(119,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -824,7 +817,7 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

-Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location

+Basics.dfy(133,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

 Execution trace:

     (0,0): anon0

 Basics.dfy(145,19): Error: assertion violation

@@ -855,8 +848,14 @@ Execution trace:
     (0,0): anon13_Then

     (0,0): anon8

     (0,0): anon14_Then

+Basics.dfy(226,10): Error: when left-hand sides 0 and 1 refer to the same location, they must have the same value

+Execution trace:

+    (0,0): anon0

+Basics.dfy(251,6): Error: left-hand sides 0 and 1 refer to the same location

+Execution trace:

+    (0,0): anon0

 

-Dafny program verifier finished with 19 verified, 11 errors

+Dafny program verifier finished with 35 verified, 12 errors

 

 -------------------- ControlStructures.dfy --------------------

 ControlStructures.dfy(5,3): Error: missing case in case statement: Blue

diff --git a/Test/dafny0/Basics.dfy b/Test/dafny0/Basics.dfy
index 6aa1e34d..87a984a3 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -110,7 +110,7 @@ method TestMulti(m: Multi, p: Multi)
   assert p.x == 300;

   if (*) {

     p.x, m.y := 10, 10;

-    p.x, m.x := 8, 8;  // error: duplicate assignment (since m and p may be the same)

+    p.x, m.x := 8, 8;

   }

 

   var a, b := new int[20], new int[30];

@@ -184,4 +184,70 @@ method EuclideanTest(a: int, b: int)
    assert 0 <= r < abs(b);

    assert a == b * q + r;

    assert (a/b) * b + a % b == a;

+}

+

+method havocInMultiassignment()

+{

+   var i: nat, j: nat;

+   i, j := *, 3;

+   assert 0 <= i;

+}

+

+method m()

+{

+  var i: int, j: int;

+  i, j := 3, 6;

+  i, i := 3, 3;

+}

+

+method swap(a: array<int>, i: nat, j: nat)

+  requires a != null && 0 <= i < a.Length && 0 <= j < a.Length;

+  modifies a;

+{

+  a[i], a[j] := a[j], a[i];

+}

+

+class CC {

+  var x : int;

+  var y : int;

+}

+

+method notQuiteSwap(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := c.x, c.x;

+}

+

+method notQuiteSwap2(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := d.x, c.y; // BAD: c and d could be the same.

+}

+

+method OKNowIt'sSwapAgain(c: CC, d: CC)

+  requires c != null && d != null;

+  modifies c,d;

+{

+  c.x, d.x := d.x, c.x;

+}

+

+method notQuiteSwap3(c: CC, d: CC)

+  requires c != null && d != null && c != d;

+  modifies c,d;

+{

+  c.x, d.x := 4, c.y;

+  c.x, c.y := 3, c.y;

+}

+

+method M() returns (a: int, b: int) {

+  return 4, 6;

+}

+method otherChecks()

+{

+  var x: int, y: int;

+  x, y :| x + y == 5; // fine

+  x, x :| x + y == 5; // BAD, must give different variables.

+  //x, x := M(); // <-- this is caught early, so it suppresses other errors.

 }
\ No newline at end of file