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, 2 insertions, 31 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 8ea18f3b..4312a414 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -2989,7 +2989,7 @@ 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 = GraphFromImpl(impl);

+      Graph<Block> g = Program.GraphFromImpl(impl);

       #endregion

 

       g.ComputeLoops(); // this is the call that does all of the processing

@@ -4598,7 +4598,7 @@ namespace VC {
 

       VCExpressionGenerator gen = proverCtxt.ExprGen;

       Contract.Assert(gen != null);

-      Graph<Block> g = GraphFromImpl(impl);

+      Graph<Block> g = Program.GraphFromImpl(impl);

 

       Hashtable/* Block --> VCExprVar */ BlkCorrect = BlockVariableMap(impl.Blocks, "_correct", gen);

       Hashtable/* Block --> VCExprVar */ BlkReached = reach ? BlockVariableMap(impl.Blocks, "_reached", gen) : null;

@@ -4854,35 +4854,6 @@ namespace VC {
       }

     }

 

-    static Graph<Block> GraphFromImpl(Implementation impl) {

-      Contract.Requires(impl != null);

-

-      Contract.Ensures(Contract.Result<Graph<Block>>() != null);

-

-      return GraphFromBlocks(impl.Blocks);

-    }

-

-    static Graph<Block> GraphFromBlocks(List<Block> blocks) {

-      Contract.Requires(blocks != null);

-

-      Contract.Ensures(Contract.Result<Graph<Block>>() != null);

-

-      Graph<Block> g = new Graph<Block>();

-      g.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph

-      foreach (Block b in blocks) {

-        Contract.Assert(b != null);

-        GotoCmd gtc = b.TransferCmd as GotoCmd;

-        if (gtc != null) {

-          foreach (Block dest in cce.NonNull(gtc.labelTargets)) {

-            Contract.Assert(dest != null);

-            g.AddEdge(b, dest);

-          }

-        }

-      }

-      return g;

-    }

-

-

     static void DumpMap(Hashtable /*Variable->Expr*/ map) {

       Contract.Requires(map != null);

       foreach (DictionaryEntry de in map) {