fixed bug in extract loops by ensuring that loop extraction is done in nesting order

1 files changed, 3 insertions, 3 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c2ef05f9..52b802a8 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -362,7 +362,6 @@ namespace Microsoft.Boogie {
     void CreateProceduresForLoops(Implementation impl, Graph<Block/*!*/>/*!*/ g, List<Implementation/*!*/>/*!*/ loopImpls) {

       Contract.Requires(impl != null);

       Contract.Requires(cce.NonNullElements(loopImpls));

-      Contract.Requires(cce.NonNullElements(g.TopologicalSort()));

       // Enumerate the headers 

       // for each header h:

       //   create implementation p_h with 

@@ -454,7 +453,9 @@ namespace Microsoft.Boogie {
         loopHeaderToCallCmd[header] = callCmd;

       }

 

-      foreach (Block/*!*/ header in g.Headers) {

+      IEnumerable<Block> sortedHeaders = g.SortHeadersByDominance();

+      foreach (Block/*!*/ header in sortedHeaders)

+      {

         Contract.Assert(header != null);

         LoopProcedure loopProc = loopHeaderToLoopProc[header];

         Dictionary<Block, Block> blockMap = new Dictionary<Block, Block>();

@@ -608,7 +609,6 @@ namespace Microsoft.Boogie {
         Implementation impl = d as Implementation;

         if (impl != null && impl.Blocks != null && impl.Blocks.Count > 0) {

           Graph<Block/*!*/>/*!*/ g = GraphFromImpl(impl);

-          Contract.Assert(cce.NonNullElements(g.TopologicalSort()));

           g.ComputeLoops();

           if (!g.Reducible) {

             throw new Exception("Irreducible flow graphs are unsupported.");