diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-07-15 20:25:37 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2014-07-15 20:25:37 +0100 |
commit | 2212c8ea826dfbbc65beef73c7ee50814175c176 (patch) | |
tree | fc27acb5b0c795e5d6444f7f313667903bf5356e /Source/VCGeneration/ConditionGeneration.cs | |
parent | 74090e6fc892db326c6f98b8adb790f1f09fba41 (diff) |
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.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 12 |
1 files changed, 6 insertions, 6 deletions
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;
}
|