summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/FixedpointVC.cs
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-07-15 20:25:37 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2014-07-15 20:25:37 +0100
commit2212c8ea826dfbbc65beef73c7ee50814175c176 (patch)
treefc27acb5b0c795e5d6444f7f313667903bf5356e /Source/VCGeneration/FixedpointVC.cs
parent74090e6fc892db326c6f98b8adb790f1f09fba41 (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/FixedpointVC.cs')
-rw-r--r--Source/VCGeneration/FixedpointVC.cs4
1 files changed, 2 insertions, 2 deletions
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)