diff options
| author |  qadeer <qadeer@microsoft.com> | 2011-08-21 08:31:12 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2011-08-21 08:31:12 -0700 |
| commit | 28d46f807724f88d77b113200cfb769cb76fa28b (patch) | |
| tree | f74b932bd5117b3aeda3b09f87a4b6b410478acf /Source/VCGeneration | |
| parent | b30e5d4b11b1558d93e1cf348069bb1b3bf739cd (diff) | |
| parent | 1a0b9358000b346b75487cd117fe41c5df36bd2a (diff) | |
reverting irreducible handling temporarily
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/VC.cs | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 8ee2a6f6..c76df8ef 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2090,16 +2090,19 @@ namespace VC { #region Use the graph library to figure out where the (natural) loops are
+
#region Create the graph by adding the source node and each edge
Graph<Block> g = Program.GraphFromImpl(impl);
#endregion
-
+
+ //Graph<Block> g = program.ProcessLoops(impl);
+
g.ComputeLoops(); // this is the call that does all of the processing
if (!g.Reducible)
{
throw new VCGenException("Irreducible flow graphs are unsupported.");
}
-
+
#endregion
#region Cut the backedges, push assert/assume statements from loop header into predecessors, change them all into assume statements at top of loop, introduce havoc statements
|