Dafny: translate call statements with fancy LHSs

2 files changed, 86 insertions, 5 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 75025b2f..2edd1c51 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -598,18 +598,18 @@ Execution trace:
     (0,0): anon10

     Basics.dfy(66,95): anon18_Else

     (0,0): anon12

-Basics.dfy(86,16): Error: assertion violation

+Basics.dfy(100,16): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

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

+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(105,10): Error: left-hand sides 0 and 1 may refer to the same location

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

 Execution trace:

     (0,0): anon0

     (0,0): anon10_Then

@@ -618,11 +618,39 @@ Execution trace:
     (0,0): anon6

     (0,0): anon12_Then

     (0,0): anon9

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

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

+Execution trace:

+    (0,0): anon0

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+Basics.dfy(147,10): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3

+Basics.dfy(147,10): Error: assignment may update an object not in the enclosing method's modifies clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3

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

 Execution trace:

     (0,0): anon0

+    (0,0): anon11_Then

+    (0,0): anon3

+    (0,0): anon12_Then

+Basics.dfy(163,15): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon11_Then

+    (0,0): anon3

+    (0,0): anon12_Else

+    (0,0): anon6

+    (0,0): anon13_Then

+    (0,0): anon8

+    (0,0): anon14_Then

 

-Dafny program verifier finished with 9 verified, 6 errors

+Dafny program verifier finished with 16 verified, 11 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 b9ba5102..1ae5b9c4 100644
--- a/Test/dafny0/Basics.dfy
+++ b/Test/dafny0/Basics.dfy
@@ -71,6 +71,20 @@ method ChallengeTruth(j: int, k: int)
 class Multi {

   var x: int;

   var y: int;

+  var next: Multi;

+  method Mutate(z: int) returns (m: Multi)

+    requires 0 <= z;

+    modifies this;

+    ensures y == old(y);

+  {

+    x := x + z;

+  }

+  method IncX() returns (oldX: int)

+    modifies this;

+    ensures x == old(x) + 1 && oldX == old(x);

+  {

+    x, oldX := x + 1, x;

+  }

 }

 

 method TestMulti(m: Multi, p: Multi)

@@ -117,4 +131,43 @@ method TestBoxAssignment<T>(x: MyBoxyClass<int>, y: MyBoxyClass<T>, t: T)
   x.f := 15;

   // all together now:

   y.f, x.f := t, 15;  // error: duplicate assignment (if T==int and x==y)

+  var k: int := x.f;

+}

+

+method TestCallsWithFancyLhss(m: Multi)

+  requires m != null && m.next != null;

+  modifies m, m.next;

+{

+  m.x := 10;

+  var p := m.next;

+  m.next.next := m.Mutate(m.x);  // fine

+  if (*) {

+    assert m.next == old(m.next);  // error: the call to Mutate may have changed m.next

+  }

+  m.next.next := m.Mutate(20);  // error: LHS may not be well defined (m.next may be null)

+  m.x, m.next := 12, p;

+  m.x, m.y := SwapEm(m.x, m.y);

+  assert m.y == 12;

+  if (*) {

+    m.x, m.x := SwapEm(m.x, m.y);  // error: duplicate among LHSs

+  }

+  m.x := 30;

+  var xx := m.IncX();

+  assert xx == 30;

+  m.y := m.IncX();

+  assert m.y == 31 && m.x == 32;

+  m.x := m.IncX();

+  assert m.x == 32;

+  xx := m.IncX();

+  if (*) {

+    assert xx == 33;  // error: xx will in fact be 32

+  } else {

+    assert xx == 32;  // see!

+  }

+}

+

+method SwapEm(a: int, b: int) returns (x: int, y: int)

+  ensures x == b && y == a;

+{

+  x, y := b, a;

 }