summaryrefslogtreecommitdiff
path: root/Source/BoogieDriver
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2012-06-19 21:46:32 -0700
committerGravatar qadeer <qadeer@microsoft.com>2012-06-19 21:46:32 -0700
commit617307d709e3714d27866ae2c34949406cda470e (patch)
tree682f2b6af371837f867463421333c09b026889ec /Source/BoogieDriver
parentc947a2b16c007c36ffc55c003672142df5538cfd (diff)
integrating predication
Diffstat (limited to 'Source/BoogieDriver')
-rw-r--r--Source/BoogieDriver/BoogieDriver.cs9
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index ae26d8db..746504b3 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -594,6 +594,15 @@ namespace Microsoft.Boogie {
program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);
}
+ if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {
+ BlockPredicator.Predicate(program, false, false);
+ if (CommandLineOptions.Clo.PrintInstrumented) {
+ using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {
+ program.Emit(writer);
+ }
+ }
+ }
+
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;
if (CommandLineOptions.Clo.ExtractLoops)
{