diff options
Diffstat (limited to 'Test/dafny0/Array.dfy')
-rw-r--r-- | Test/dafny0/Array.dfy | 21 |
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;
+}
|