summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/Absy.cs2
-rw-r--r--Source/Core/AbsyCmd.cs2
-rw-r--r--Source/Core/AbsyExpr.cs2
-rw-r--r--Source/Core/AbsyType.cs2
-rw-r--r--Source/Core/Inline.cs4
-rw-r--r--Source/Core/LambdaHelper.cs2
-rw-r--r--Source/Core/ResolutionContext.cs4
-rw-r--r--Source/Core/Util.cs10
-rw-r--r--Source/Houdini/AbstractHoudini.cs6
-rw-r--r--Source/Houdini/Houdini.cs2
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs2
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.cs2
-rw-r--r--Source/VCGeneration/ConditionGeneration.cs12
-rw-r--r--Source/VCGeneration/FixedpointVC.cs4
-rw-r--r--Source/VCGeneration/VC.cs6
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();
}
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 12:28:54 +0000