diff options
author | qadeer <unknown> | 2010-09-01 15:25:06 +0000 |
---|---|---|
committer | qadeer <unknown> | 2010-09-01 15:25:06 +0000 |
commit | 6a71d5d0c7347da955f2c5e526bd9f2dcf908429 (patch) | |
tree | 1bcca91fb5fd968ba23f55424541162ff843bffb /Source/Core/Absy.cs | |
parent | ca50aef90076b154b2748d1bf5a8f046452a2aa3 (diff) |
fixed bug in extract loops by ensuring that loop extraction is done in nesting order
Diffstat (limited to 'Source/Core/Absy.cs')
-rw-r--r-- | Source/Core/Absy.cs | 6 |
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.");
|