diff options
| author |  Unknown <leino@LEINO4.redmond.corp.microsoft.com> | 2011-04-05 17:03:28 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO4.redmond.corp.microsoft.com> | 2011-04-05 17:03:28 -0700 |
| commit | 2918a80203d42a51c45872dd6900eb3677d130eb (patch) | |
| tree | 253e0ad470fd6581305f88edf61f00b7a074e5f0 /Test/dafny0/TypeTests.dfy | |
| parent | 6e93acd001f5d23c08b02c162dc2111e531f3d5d (diff) | |
Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression
Diffstat (limited to 'Test/dafny0/TypeTests.dfy')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index cbab53bf..93c4aec4 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -80,3 +80,12 @@ method InitCalls() { var d := new C.M(8); // error: M has out parameters
var e := new C.Caller();
}
+
+// ---------------------
+
+method ArrayRangeAssignments(a: array<C>)
+ requires a != null && 10 <= a.Length;
+{
+ a[0..5] := new C; // this is not allowed
+ havoc a[1..4]; // this is not allowed
+}
|