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

1 files changed, 21 insertions, 0 deletions

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;

+}