diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-28 18:51:27 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-28 18:51:27 -0700 |
| commit | 7b8adafdc184fd812fbb26d4d4ca4aaf5f0d134a (patch) | |
| tree | 727566ae9586fa19d32c71b3872a57392ce9cd0f /Test/dafny0/TypeTests.dfy | |
| parent | 7cf0e87a3c9cbc769a9248604e8943a7faddd914 (diff) | |
Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"
Diffstat (limited to 'Test/dafny0/TypeTests.dfy')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 9df11a67..2208051d 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -76,7 +76,7 @@ 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
+ a[1..4] := *; // this is not allowed
}
// --------------------- tests of restrictions on subranges (nat)
|