From f6fe9adfa18b3b6f4d0c2c92f3f91e06160c503c Mon Sep 17 00:00:00 2001 From: leino Date: Sun, 20 Sep 2015 22:00:41 -0700 Subject: Removed tabs from test file --- Test/dafny0/ResolutionErrors.dfy | 122 ++++++++++++++++---------------- Test/dafny0/ResolutionErrors.dfy.expect | 26 +++---- 2 files changed, 74 insertions(+), 74 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 5f0b22a2..d34fd8a5 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -91,9 +91,9 @@ class EE { var b3 := Benny; var d0 := David(20); // error: constructor name David is ambiguous var d1 := David; // error: constructor name David is ambiguous (never mind that the signature does - // not match either of them) + // not match either of them) var d2 := David(20, 40); // error: constructor name Davis is ambiguous (never mind that the given - // parameters match the signature of only one of those constructors) + // parameters match the signature of only one of those constructors) var d3 := Abc.David(20, 40); // error: wrong number of parameters var d4 := Rst.David(20, 40); var e := Eleanor; // this resolves to the field, not the Abc datatype constructor @@ -412,8 +412,8 @@ class SideEffectChecks { { x := 1; } // updates to locals defined outside of the hint are not allowed x; { - var x: int; - x := 1; // this is OK + var x: int; + x := 1; // this is OK } 1; } @@ -676,42 +676,42 @@ module StatementsInExpressions { modifies this; { calc { - 5; - { SideEffect(); } // error: cannot call method with side effects - 5; + 5; + { SideEffect(); } // error: cannot call method with side effects + 5; } } function F(): int { calc { - 6; - { assert 6 < 8; } - { NonGhostMethod(); } // error: cannot call non-ghost method - { var x := 8; - while x != 0 - decreases *; // error: cannot use 'decreases *' in a ghost context - { - x := x - 1; - } - } - { var x := 8; - while x != 0 - { - x := x - 1; - } - } - { MyField := 12; } // error: cannot assign to a field - { MyGhostField := 12; } // error: cannot assign to any field - { SideEffect(); } // error: cannot call (ghost) method with a modifies clause - { var x := 8; - while x != 0 - modifies this; // error: cannot use a modifies clause on a loop - { - x := x - 1; - } - } - 6; + 6; + { assert 6 < 8; } + { NonGhostMethod(); } // error: cannot call non-ghost method + { var x := 8; + while x != 0 + decreases *; // error: cannot use 'decreases *' in a ghost context + { + x := x - 1; + } + } + { var x := 8; + while x != 0 + { + x := x - 1; + } + } + { MyField := 12; } // error: cannot assign to a field + { MyGhostField := 12; } // error: cannot assign to any field + { SideEffect(); } // error: cannot call (ghost) method with a modifies clause + { var x := 8; + while x != 0 + modifies this; // error: cannot use a modifies clause on a loop + { + x := x - 1; + } + } + 6; } 5 } @@ -723,33 +723,33 @@ module StatementsInExpressions { { var y := calc { - 6; - { assert 6 < 8; } - { NonGhostMethod(); } // error: cannot call non-ghost method - { var x := 8; - while x != 0 - decreases *; // error: cannot use 'decreases *' in a ghost context - { - x := x - 1; - } - } - { MyField := 12; } // error: cannot assign to a field - { MyGhostField := 12; } // error: cannot assign to any field - { M(); } // error: cannot call (ghost) method with a modifies clause - { var x := 8; - while x != 0 - modifies this; // error: cannot use a modifies clause on a loop - { - x := x - 1; - } - } - { var x := 8; - while x != 0 - { - x := x - 1; - } - } - 6; + 6; + { assert 6 < 8; } + { NonGhostMethod(); } // error: cannot call non-ghost method + { var x := 8; + while x != 0 + decreases *; // error: cannot use 'decreases *' in a ghost context + { + x := x - 1; + } + } + { MyField := 12; } // error: cannot assign to a field + { MyGhostField := 12; } // error: cannot assign to any field + { M(); } // error: cannot call (ghost) method with a modifies clause + { var x := 8; + while x != 0 + modifies this; // error: cannot use a modifies clause on a loop + { + x := x - 1; + } + } + { var x := 8; + while x != 0 + { + x := x - 1; + } + } + 6; } 5; } diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 8debdbf9..04913cf5 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -18,19 +18,19 @@ ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified -ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(704,11): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(736,11): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(741,14): Error: a while statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(680,20): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(690,24): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(693,22): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors.dfy(704,18): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(705,23): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(706,20): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(709,21): Error: a while statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(728,24): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(731,22): Error: 'decreases *' is not allowed on ghost loops +ResolutionErrors.dfy(736,18): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(737,23): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(738,11): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(741,21): Error: a while statement used inside a hint is not allowed to have a modifies clause ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1) -- cgit v1.2.3