Removed tabs from test file

2 files changed, 74 insertions, 74 deletions

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)