diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-12-05 11:57:01 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-12-05 11:57:01 -0800 |
| commit | 70caaefc912aeaab556c7bfee6c1a9b7e8fe75a3 (patch) | |
| tree | ae34f5eb9d1f97f9aea2c00b18e963e4f69afa4c /Source/BoogieDriver | |
| parent | 7b8a0e0a4e75f28a1721bee9179f65bd405301c2 (diff) | |
added more instrumentation to Houdini
when vcgen fails, instead of stopping houdini, the failing vc is added to a list of blacklisted vcs
fixed bug in the call graph generation when inlining is used
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 58731f10..eab8bc36 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -390,6 +390,8 @@ namespace Microsoft.Boogie { // Coalesce blocks
if (CommandLineOptions.Clo.CoalesceBlocks) {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
}
|