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/AdvancedLHS.dfy | |
| parent | 7cf0e87a3c9cbc769a9248604e8943a7faddd914 (diff) | |
Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"
Diffstat (limited to 'Test/dafny0/AdvancedLHS.dfy')
| -rw-r--r-- | Test/dafny0/AdvancedLHS.dfy | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy index 4f80eade..cc07cbb5 100644 --- a/Test/dafny0/AdvancedLHS.dfy +++ b/Test/dafny0/AdvancedLHS.dfy @@ -7,7 +7,7 @@ class C { {
x := new C;
x := new C.Init();
- havoc x;
+ x := *;
x := choose S;
// test evaluation order
@@ -35,11 +35,11 @@ class C { if (a != null && 10 <= a.Length) {
a[2] := new C;
a[4..8] := null;
- havoc a[3];
+ a[3] := *;
}
if (b != null && 10 <= b.Length0 && 20 <= b.Length1) {
b[2,14] := new C;
- havoc b[3,11];
+ b[3,11] := *;
}
}
|