diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-06-19 21:46:32 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-06-19 21:46:32 -0700 |
| commit | 617307d709e3714d27866ae2c34949406cda470e (patch) | |
| tree | 682f2b6af371837f867463421333c09b026889ec /Source/BoogieDriver/BoogieDriver.cs | |
| parent | c947a2b16c007c36ffc55c003672142df5538cfd (diff) | |
integrating predication
Diffstat (limited to 'Source/BoogieDriver/BoogieDriver.cs')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 9 |
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)
{
|