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 | |
| parent | 7cf0e87a3c9cbc769a9248604e8943a7faddd914 (diff) | |
Dafny: changed syntax of havoc statements from "havoc X;" to "X := *;"
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/AdvancedLHS.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Definedness.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 2 |
4 files changed, 6 insertions, 6 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] := *;
}
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0eab5c50..c82d3803 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -75,7 +75,7 @@ TypeTests.dfy(61,6): Error: Duplicate local-variable name: y TypeTests.dfy(68,17): Error: member F in class C does not refer to a method
TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments
TypeTests.dfy(78,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
-TypeTests.dfy(79,2): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
+TypeTests.dfy(79,10): Error: Assignment to range of array elements must have a simple expression RHS; try using a temporary local variable
TypeTests.dfy(85,9): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(86,8): Error: sorry, cannot instantiate 'array' type with a subrange type
TypeTests.dfy(87,8): Error: sorry, cannot instantiate 'array' type with a subrange type
diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy index 92ac0793..8df1a7c5 100644 --- a/Test/dafny0/Definedness.dfy +++ b/Test/dafny0/Definedness.dfy @@ -151,7 +151,7 @@ class StatementTwoShoes { while (20 / k == 5 && j < 100) // error: guard may not be well defined (div by zero)
decreases 100 - j;
{
- havoc k;
+ k := *;
j := j + 1;
}
}
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)
|