Fix nasty bug introduced by commit 61a94f409975.

There were many calls in the code to

``` new TokenTextWriter("<buffer>", buffer, false) ```

Prior to 61a94f409975 this was a call to the following constructor

```
TokenTextWriter(string filename, TextWriter writer, bool setTokens)
```

After that commit these then became calls to

```
TokenTextWriter(string filename, TextWriter writer, bool pretty)
```

An example of where this would cause issues was if ToString() was called on an
AbsyCmd then the its token would be modified because the setTokens parameter
was effectively set to True when the original intention was for it to be set
to false!

To fix this I've

* Removed the default parameter value for pretty and fixed all
uses so that we pass false where it was implicitly being set before

* Where the intention was to set setTokens to false this has been fixed so
  it is actually set to false!

Unfortunately I couldn't find a way of observing this bug from the Boogie
executable so I couldn't create a test case. I could only observe it when I was
using Boogie's APIs.

15 files changed, 31 insertions, 31 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index e256c7d9..d6ac8754 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -3259,7 +3259,7 @@ namespace Microsoft.Boogie {
 

         if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

           Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name);

-          using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, false)) {

+          using (TokenTextWriter stream = new TokenTextWriter("<console>", Console.Out, /*setTokens=*/false, /*pretty=*/ false)) {

             foreach (var e in map) {

               Console.Write("  ");

               cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0);

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index cd017e5e..b16fb1ba 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -1170,7 +1170,7 @@ namespace Microsoft.Boogie {
     {

       Contract.Ensures(Contract.Result<string>() != null);

       System.IO.StringWriter buffer = new System.IO.StringWriter();

-      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false , /*pretty=*/ false)) {

         this.Emit(stream, 0);

       }

       return buffer.ToString();

diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index d928e536..bc603ea5 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Boogie {
     public override string ToString() {

       Contract.Ensures(Contract.Result<string>() != null);

       System.IO.StringWriter buffer = new System.IO.StringWriter();

-      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false, /*pretty=*/ false)) {

         this.Emit(stream, 0, false);

       }

       return buffer.ToString();

diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs
index a1240c30..446621af 100644
--- a/Source/Core/AbsyType.cs
+++ b/Source/Core/AbsyType.cs
@@ -59,7 +59,7 @@ namespace Microsoft.Boogie {
     public override string ToString() {

       Contract.Ensures(Contract.Result<string>() != null);

       System.IO.StringWriter buffer = new System.IO.StringWriter();

-      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+      using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/false, /*pretty=*/ false)) {

         this.Emit(stream);

       }

       return buffer.ToString();

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index b25071a6..9af18158 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -143,8 +143,8 @@ namespace Microsoft.Boogie {
       Contract.Requires(impl != null);

       Contract.Requires(impl.Proc != null);

       Console.WriteLine("after inlining procedure calls");

-      impl.Proc.Emit(new TokenTextWriter("<console>", Console.Out), 0);

-      impl.Emit(new TokenTextWriter("<console>", Console.Out), 0);

+      impl.Proc.Emit(new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false), 0);

+      impl.Emit(new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false), 0);

     }

 

     private sealed class DummyErrorSink : IErrorSink {

diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs
index 2230db91..c884be3c 100644
--- a/Source/Core/LambdaHelper.cs
+++ b/Source/Core/LambdaHelper.cs
@@ -25,7 +25,7 @@ namespace Microsoft.Boogie {
       functions = v.lambdaFunctions;

       if (CommandLineOptions.Clo.TraceVerify) {

         Console.WriteLine("Desugaring of lambda expressions produced {0} functions and {1} axioms:", functions.Count, axioms.Count);

-        TokenTextWriter wr = new TokenTextWriter("<console>", Console.Out);

+        TokenTextWriter wr = new TokenTextWriter("<console>", Console.Out, /*pretty=*/ false);

         foreach (Function f in functions) {

           f.Emit(wr, 0);

         }

diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs
index 741d2ac5..bf1a5629 100644
--- a/Source/Core/ResolutionContext.cs
+++ b/Source/Core/ResolutionContext.cs
@@ -81,13 +81,13 @@ namespace Microsoft.Boogie {
             fixedArgs[i] = cce.NonNull((NamedDeclaration)args[i]).Name;

           } else if (args[i] is Type) {

             System.IO.StringWriter buffer = new System.IO.StringWriter();

-            using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+            using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false, /*pretty=*/ false)) {

               cce.NonNull((Type)args[i]).Emit(stream);

             }

             fixedArgs[i] = buffer.ToString();

           } else if (args[i] is Expr) {

             System.IO.StringWriter buffer = new System.IO.StringWriter();

-            using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+            using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false, /*pretty=*/ false)) {

               cce.NonNull((Expr/*!*/)args[i]).Emit(stream, 0, false);

             }

             fixedArgs[i] = buffer.ToString();

diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs
index 6aafec7f..75cb25aa 100644
--- a/Source/Core/Util.cs
+++ b/Source/Core/Util.cs
@@ -252,7 +252,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public TokenTextWriter(string filename, bool pretty = false)

+    public TokenTextWriter(string filename, bool pretty)

       : base() {

       Contract.Requires(filename != null);

       this.pretty = pretty;

@@ -260,7 +260,7 @@ namespace Microsoft.Boogie {
       this.writer = new StreamWriter(filename);

     }

 

-    public TokenTextWriter(string filename, bool setTokens, bool pretty = false)

+    public TokenTextWriter(string filename, bool setTokens, bool pretty)

       : base() {

       Contract.Requires(filename != null);

       this.pretty = pretty;

@@ -269,7 +269,7 @@ namespace Microsoft.Boogie {
       this.setTokens = setTokens;

     }

 

-    public TokenTextWriter(string filename, TextWriter writer, bool setTokens, bool pretty = false)

+    public TokenTextWriter(string filename, TextWriter writer, bool setTokens, bool pretty)

       : base() {

       Contract.Requires(writer != null);

       Contract.Requires(filename != null);

@@ -279,7 +279,7 @@ namespace Microsoft.Boogie {
       this.setTokens = setTokens;

     }

 

-    public TokenTextWriter(string filename, TextWriter writer, bool pretty = false)

+    public TokenTextWriter(string filename, TextWriter writer, bool pretty)

       : base() {

       Contract.Requires(writer != null);

       Contract.Requires(filename != null);

@@ -288,7 +288,7 @@ namespace Microsoft.Boogie {
       this.writer = writer;

     }

 

-    public TokenTextWriter(TextWriter writer, bool pretty = false)

+    public TokenTextWriter(TextWriter writer, bool pretty)

       : base() {

       Contract.Requires(writer != null);

       this.pretty = pretty;

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index 8b038554..716456ea 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -283,7 +283,7 @@ namespace Microsoft.Boogie.Houdini {
 

         private void PrintFunction(Function function)

         {

-            var tt = new TokenTextWriter(Console.Out);

+            var tt = new TokenTextWriter(Console.Out, /*pretty=*/ false);

             var invars = new List<Expr>(function.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));

             function.Body = function2Value[function.Name].Gamma(invars);

             function.Emit(tt, 0);

@@ -2436,7 +2436,7 @@ namespace Microsoft.Boogie.Houdini {
                 }

             }

 

-            using (var wt = new TokenTextWriter(WitnessFile))

+            using (var wt = new TokenTextWriter(WitnessFile, /*pretty=*/ false))

             {

                 program.Emit(wt);

             }

@@ -2489,7 +2489,7 @@ namespace Microsoft.Boogie.Houdini {
                 }

             }

 

-            using (var wt = new TokenTextWriter(WitnessFile))

+            using (var wt = new TokenTextWriter(WitnessFile, /*pretty=*/ false))

             {

                 program.Emit(wt);

             }

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index adb86598..af1bd8ad 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -747,7 +747,7 @@ namespace Microsoft.Boogie.Houdini {
                     cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);

                     cexWriter.Write(error.ToString());

                     cexWriter.WriteLine();

-                    using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))

+                    using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter, /*pretty=*/ false))

                       foreach (Microsoft.Boogie.Block blk in error.Trace)

                         blk.Emit(writer, 15);

                     //cexWriter.WriteLine(); 

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 1ccec455..7c6a3a9a 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -120,7 +120,7 @@ namespace Microsoft.Boogie.SMTLib
           sb.Append(TypeToString(t));

         } else {

           System.IO.StringWriter buffer = new System.IO.StringWriter();

-          using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+          using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/false, /*pretty=*/false)) {

             t.Emit(stream);

           }

           sb.Append(buffer.ToString());

diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index 02e3adda..e0a4b4c6 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -271,7 +271,7 @@ namespace Microsoft.Boogie.VCExprAST {
           sb.Append(TypeToString(t));

         } else {

           System.IO.StringWriter buffer = new System.IO.StringWriter();

-          using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {

+          using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, /*setTokens=*/ false, /*pretty=*/ false)) {

             t.Emit(stream);

           }

           sb.Append(buffer.ToString());

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 5304a789..90e2a9c1 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -755,7 +755,7 @@ namespace VC {
 

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

-        debugWriter = new TokenTextWriter("<console>", Console.Out, false);

+        debugWriter = new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false);

         debugWriter.WriteLine("Effective precondition:");

       }

 

@@ -809,7 +809,7 @@ namespace VC {
 

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

-        debugWriter = new TokenTextWriter("<console>", Console.Out, false);

+        debugWriter = new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false);

         debugWriter.WriteLine("Effective postcondition:");

       }

 

@@ -876,7 +876,7 @@ namespace VC {
 

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

-        debugWriter = new TokenTextWriter("<console>", Console.Out, false);

+        debugWriter = new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false);

         debugWriter.WriteLine("Effective precondition:");

       }

 

@@ -933,7 +933,7 @@ namespace VC {
           post.Add(c);

 

           if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

-            c.Emit(new TokenTextWriter("<console>", Console.Out, false), 1);

+            c.Emit(new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 1);

           }

         }

       }

@@ -957,7 +957,7 @@ namespace VC {
       Contract.Ensures(Contract.Result<List<Cmd>>() != null);

       TokenTextWriter debugWriter = null;

       if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {

-        debugWriter = new TokenTextWriter("<console>", Console.Out, false);

+        debugWriter = new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false);

         debugWriter.WriteLine("Effective precondition from where-clauses:");

       }

 

@@ -1125,7 +1125,7 @@ namespace VC {
       CommandLineOptions.Clo.PrintUnstructured = 2;  // print only the unstructured program

       bool oldPrintDesugaringSetting = CommandLineOptions.Clo.PrintDesugarings;

       CommandLineOptions.Clo.PrintDesugarings = printDesugarings;

-      impl.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

+      impl.Emit(new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 0);

       CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;

       CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

     }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 0dc81b0c..9f39e46c 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -748,7 +748,7 @@ namespace Microsoft.Boogie
 			if(mode != Mode.Corral || CommandLineOptions.Clo.PrintFixedPoint == null)

 				return; // not implemented for other annotation modes yet

 			

-			var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintFixedPoint);

+            var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintFixedPoint, /*pretty=*/ false);

 			Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node> ();

 

 			foreach (var node in rpfp.nodes)

@@ -823,7 +823,7 @@ namespace Microsoft.Boogie
             if (mode != Mode.Corral || CommandLineOptions.Clo.PrintConjectures == null)

                 return; // not implemented for other annotation modes yet

 

-            var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintConjectures + "." + ConjectureFileCounter.ToString());

+            var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintConjectures + "." + ConjectureFileCounter.ToString(), /*pretty=*/ false);

             ConjectureFileCounter++;

 

             foreach (var c in rpfp.conjectures)

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 18e47ac1..5a618b1d 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -618,7 +618,7 @@ namespace VC {
           List<Block> backup = impl.Blocks;

           Contract.Assert(backup != null);

           impl.Blocks = blocks;

-          impl.Emit(new TokenTextWriter(filename, sw, false), 0);

+          impl.Emit(new TokenTextWriter(filename, sw, /*setTokens=*/ false, /*pretty=*/ false), 0);

           impl.Blocks = backup;

           CommandLineOptions.Clo.PrintDesugarings = oldPrintDesugaringSetting;

           CommandLineOptions.Clo.PrintUnstructured = oldPrintUnstructured;

@@ -3737,9 +3737,9 @@ namespace VC {
         Expr e = (Expr)de.Value;

         Contract.Assert(e != null);

         Console.Write("  ");

-        v.Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

+        v.Emit(new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false), 0);

         Console.Write("  --> ");

-        e.Emit(new TokenTextWriter("<console>", Console.Out, false));

+        e.Emit(new TokenTextWriter("<console>", Console.Out, /*setTokens=*/ false, /*pretty=*/ false));

         Console.WriteLine();

       }

     }