Dafny: fixed bug in translator when LHS of a call was an array element or a nat

3 files changed, 50 insertions, 2 deletions

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 3ec3c291..1e400599 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -3652,7 +3652,22 @@ namespace Microsoft.Dafny {
       }

       ProcessCallStmt(s.Tok, s.Receiver, actualReceiver, s.Method, s.Args, bLhss, lhsTypes, builder, locals, etran);

       for (int i = 0; i < lhsBuilders.Count; i++) {

-        lhsBuilders[i](bLhss[i], builder, etran);

+        var lhs = s.Lhs[i];

+        Type lhsType = null;

+        if (lhs is IdentifierExpr) {

+          lhsType = lhs.Type;

+        } else if (lhs is FieldSelectExpr) {

+          var fse = (FieldSelectExpr)lhs;

+          lhsType = fse.Field.Type;

+        }

+

+        Bpl.Expr bRhs = bLhss[i];  // the RHS (bRhs) of the assignment to the actual call-LHS (lhs) was a LHS (bLhss[i]) in the Boogie call statement

+        if (lhsType != null) {

+          CheckSubrange(lhs.tok, bRhs, lhsType, builder);

+        }

+        bRhs = etran.CondApplyBox(lhs.tok, bRhs, lhs.Type, lhsType);

+

+        lhsBuilders[i](bRhs, builder, etran);

       }

       builder.Add(CaptureState(s.Tok));

     }

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0c2e487a..a3e5e11f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -541,8 +541,20 @@ Array.dfy(183,1): Error BP5003: A postcondition might not hold on this return pa
 Array.dfy(182,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

+Array.dfy(198,10): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

+Array.dfy(199,5): Error: value assigned to a nat must be non-negative

+Execution trace:

+    (0,0): anon0

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

 

-Dafny program verifier finished with 30 verified, 13 errors

+Dafny program verifier finished with 31 verified, 15 errors

 

 -------------------- MultiDimArray.dfy --------------------

 MultiDimArray.dfy(53,21): Error: assertion violation

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index 6699e648..613cdd83 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -182,3 +182,24 @@ ghost method Fill_None(s: seq<int>)
   ensures forall i,j :: 0 <= i < j < |s| ==> s[i] <= s[j];

 {  // error: cannot prove postcondition

 }

+

+// -------------- some regression tests; there was a time when array-element LHSs of calls were not translated correctly

+

+method Test_ArrayElementLhsOfCall(a: array<int>, i: int, c: Cdefg<int>) returns (x: int)

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

+  modifies a, c;

+{

+  if (0 <= i < a.Length) {

+    a[i] := x;

+    a[i] := Test_ArrayElementLhsOfCall(a, i-1, c);  // this line used to crash Dafny

+    c.t := x;

+    c.t := Test_ArrayElementLhsOfCall(a, i-1, c);  // this line used to crash Dafny

+    var n: nat;

+    n := x;  // error: subrange check is applied and it cannot be verified

+    n := Test_ArrayElementLhsOfCall(a, i-1, c);  // error: subrange check is applied and it cannot be verified

+  }

+}

+

+class Cdefg<T> {

+  var t: T;

+}