Added the option /extractLoops to extract loops as procedure calls. If either lazyInline or stratifiedInline is greater than 1, the extracted procedure is decorated with the attribute "{:inline 1}". The implementation involved moving the procedure GraphFromImpl from VC.cs to Absy.ssc.

1 files changed, 5 insertions, 0 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index aeb0f627..0e99ad9b 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -529,6 +529,11 @@ namespace Microsoft.Boogie {
         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

 

+      if (CommandLineOptions.Clo.ExtractLoops)

+      {

+          program.ExtractLoops();

+      }

+

       if (CommandLineOptions.Clo.PrintInstrumented) {

         program.Emit(new TokenTextWriter(Console.Out));

       }