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 | 343f29bee9cad726c2de33d4ef6cdb49caa965d2 (patch) | |
| tree | bc40127c4275c0a91c42620f5b4a6d96b5f61871 /Test/dafny0/TypeTests.dfy | |
| parent | 2b09756f836307f75a36c5a982784dc620fda657 (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
+}
|