BlockSeq: farewell

4 files changed, 38 insertions, 38 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index b094f209..93de935d 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -75,7 +75,7 @@ namespace Microsoft.Boogie {
     }

 

     [Peer]

-    public BlockSeq Trace;

+    public List<Block> Trace;

     public Model Model;

     public VC.ModelViewInfo MvInfo;

     public ProverContext Context;

@@ -85,7 +85,7 @@ namespace Microsoft.Boogie {
 

     public Dictionary<TraceLocation, CalleeCounterexampleInfo> calleeCounterexamples;

 

-    internal Counterexample(BlockSeq trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {

+    internal Counterexample(List<Block> trace, Model model, VC.ModelViewInfo mvInfo, ProverContext context) {

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

       this.Trace = trace;

@@ -312,7 +312,7 @@ namespace Microsoft.Boogie {
 

   public class CounterexampleComparer : IComparer<Counterexample> {

 

-    private int Compare(BlockSeq bs1, BlockSeq bs2)

+    private int Compare(List<Block> bs1, List<Block> bs2)

     {

       if (bs1.Count < bs2.Count)

       {

@@ -383,7 +383,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public AssertCounterexample(BlockSeq trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public AssertCounterexample(List<Block> trace, AssertCmd failingAssert, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(trace != null);

       Contract.Requires(failingAssert != null);

@@ -413,7 +413,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public CallCounterexample(BlockSeq trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public CallCounterexample(List<Block> trace, CallCmd failingCall, Requires failingRequires, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(!failingRequires.Free);

       Contract.Requires(trace != null);

@@ -446,7 +446,7 @@ namespace Microsoft.Boogie {
     }

 

 

-    public ReturnCounterexample(BlockSeq trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

+    public ReturnCounterexample(List<Block> trace, TransferCmd failingReturn, Ensures failingEnsures, Model model, VC.ModelViewInfo mvInfo, ProverContext context)

       : base(trace, model, mvInfo, context) {

       Contract.Requires(trace != null);

       Contract.Requires(context != null);

@@ -679,7 +679,7 @@ namespace VC {
           }

           b.TransferCmd = new GotoCmd(Token.NoToken,

             new List<String> { targetBlock.Label },

-            new BlockSeq(targetBlock));

+            new List<Block> { targetBlock });

           targetBlock.Predecessors.Add(b);

         }

         impl.Blocks.Add(b);

@@ -724,7 +724,7 @@ namespace VC {
       Block origStartBlock = impl.Blocks[0];

       Block insertionPoint = new Block(

         new Token(-17, -4), blockLabel, startCmds,

-        new GotoCmd(Token.NoToken, new List<String> { origStartBlock.Label }, new BlockSeq(origStartBlock)));

+        new GotoCmd(Token.NoToken, new List<String> { origStartBlock.Label }, new List<Block> { origStartBlock }));

 

       impl.Blocks[0] = insertionPoint;  // make insertionPoint the start block

       impl.Blocks.Add(origStartBlock);  // and put the previous start block at the end of the list

@@ -808,7 +808,7 @@ namespace VC {
             ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);

             // Third, make the old insertion-point block goto the entry block of the CodeExpr

             Block beEntry = cce.NonNull(be.Blocks[0]);

-            insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { beEntry.Label }, new BlockSeq(beEntry));

+            insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { beEntry.Label }, new List<Block> { beEntry });

             beEntry.Predecessors.Add(insertionPoint);

             // Fourth, update the insertion point

             insertionPoint = nextIP;

@@ -1110,7 +1110,7 @@ namespace VC {
             if (b.TransferCmd is ReturnCmd) {

               List<String> labels = new List<String>();

               labels.Add(unifiedExitLabel);

-              BlockSeq bs = new BlockSeq();

+              List<Block> bs = new List<Block>();

               bs.Add(unifiedExit);

               GotoCmd go = new GotoCmd(Token.NoToken, labels, bs);

               gotoCmdOrigins[go] = (ReturnCmd)b.TransferCmd;

@@ -1132,7 +1132,7 @@ namespace VC {
       Contract.Requires(blocks != null);

       foreach (Block b in blocks) {

         Contract.Assert(b != null);

-        b.Predecessors = new BlockSeq();

+        b.Predecessors = new List<Block>();

       }

       foreach (Block b in blocks) {

         Contract.Assert(b != null);

@@ -1621,7 +1621,7 @@ namespace VC {
       // successor of newBlock list

       List<String> ls = new List<String>();

       ls.Add(succ.Label);

-      BlockSeq bs = new BlockSeq();

+      List<Block> bs = new List<Block>();

       bs.Add(succ);

 

       Block newBlock = new Block(

@@ -1632,7 +1632,7 @@ namespace VC {
           );

 

       // predecessors of newBlock

-      BlockSeq ps = new BlockSeq();

+      List<Block> ps = new List<Block>();

       ps.Add(pred);

       newBlock.Predecessors = ps;

 

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 5a6ae6d3..3fe3910e 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -1585,7 +1585,7 @@ namespace Microsoft.Boogie
             Block entryBlock = cce.NonNull(procImpl.Blocks[0]);

             Contract.Assert(entryBlock != null);

            

-            BlockSeq trace = new BlockSeq(); 

+            List<Block> trace = new List<Block>(); 

             trace.Add(entryBlock);

 

             var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

@@ -1621,7 +1621,7 @@ namespace Microsoft.Boogie
         private Counterexample GenerateTraceRec(

                               RPFP rpfp, RPFP.Node root,

                               List<StateId> orderedStateIds,

-                              Block/*!*/ b, BlockSeq/*!*/ trace,

+                              Block/*!*/ b, List<Block>/*!*/ trace,

                               Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples,

                               StratifiedInliningInfo info,

                               bool toplevel)

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index f29a1b80..ef2cd1d1 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -2558,7 +2558,7 @@ namespace VC {
             traceNodes.Add(absy, null);

         }

 

-        BlockSeq trace = new BlockSeq();

+        List<Block> trace = new List<Block>();

         Block entryBlock = cce.NonNull(procImpl.Blocks[0]);

         Contract.Assert(entryBlock != null);

         Contract.Assert(traceNodes.Contains(entryBlock));

@@ -2573,7 +2573,7 @@ namespace VC {
       private Counterexample GenerateTraceRec(

                             IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,

                             int candidateId,

-                            Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,

+                            Block/*!*/ b, Hashtable/*!*/ traceNodes, List<Block>/*!*/ trace,

                             Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples) {

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

         Contract.Requires(b != null);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 6599515d..92d1fd14 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -194,7 +194,7 @@ namespace VC {
             res.Add(kv.Value);

           }

           if (go != null) {

-            GotoCmd copy = new GotoCmd(go.tok, new List<String>(), new BlockSeq());

+            GotoCmd copy = new GotoCmd(go.tok, new List<String>(), new List<Block>());

             kv.Value.TransferCmd = copy;

             foreach (Block b in cce.NonNull(go.labelTargets)) {

               Contract.Assert(b != null);

@@ -744,7 +744,7 @@ namespace VC {
           GotoCmd gt = b.TransferCmd as GotoCmd;

           if (gt == null)

             continue;

-          BlockSeq targ = cce.NonNull(gt.labelTargets);

+          List<Block> targ = cce.NonNull(gt.labelTargets);

           if (targ.Count < 2)

             continue;

           // caution, we only consider two first exits

@@ -950,7 +950,7 @@ namespace VC {
         GotoCmd gt = b.TransferCmd as GotoCmd;

         copies[b] = res;

         if (gt != null) {

-          GotoCmd newGoto = new GotoCmd(gt.tok, new List<String>(), new BlockSeq());

+          GotoCmd newGoto = new GotoCmd(gt.tok, new List<String>(), new List<Block>());

           res.TransferCmd = newGoto;

           int pos = 0;

           foreach (Block ch in cce.NonNull(gt.labelTargets)) {

@@ -1038,7 +1038,7 @@ namespace VC {
         Contract.Requires(context != null);

         Contract.Ensures(Contract.Result<Counterexample>() != null);

 

-        BlockSeq trace = new BlockSeq();

+        List<Block> trace = new List<Block>();

         foreach (Block b in blocks) {

           Contract.Assert(b != null);

           trace.Add(b);

@@ -1735,7 +1735,7 @@ namespace VC {
             traceNodes.Add(absy, null);

         }

 

-        BlockSeq trace = new BlockSeq();

+        List<Block> trace = new List<Block>();

         Block entryBlock = cce.NonNull(this.blocks[0]);

         Contract.Assert(traceNodes.Contains(entryBlock));

         trace.Add(entryBlock);

@@ -1831,7 +1831,7 @@ namespace VC {
           // find the corresponding Block (assertNodes.Count is likely to be 1, or small in any case, so just do a linear search here)

           foreach (Block b in traceNodes) {

             if (b.Cmds.Contains(a)) {

-              BlockSeq trace = new BlockSeq();

+              List<Block> trace = new List<Block>();

               trace.Add(b);

               Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, model, MvInfo, context);

               callback.OnCounterexample(newCounterexample, null);

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

       // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges

       // below assumes that the start node has no predecessor)

-      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new BlockSeq(impl.Blocks[0]))));

+      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new List<Block> { impl.Blocks[0] })));

       ResetPredecessors(impl.Blocks);

       

       #region Convert program CFG into a DAG

@@ -1991,7 +1991,7 @@ namespace VC {
           if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Count > 1 )

           {

             // then remove the backedge by removing the target block from the list of gotos

-            BlockSeq remainingTargets = new BlockSeq();

+            List<Block> remainingTargets = new List<Block>();

             List<String> remainingLabels = new List<String>();

             Contract.Assume( gtc.labelNames != null);

             for (int i = 0, n = gtc.labelTargets.Count; i < n; i++)

@@ -2019,7 +2019,7 @@ namespace VC {
                 RecordCutEdge(edgesCut, backEdgeNode, gtc.labelTargets[0]);

           }

           #region Remove the backedge node from the list of predecessor nodes in the header

-          BlockSeq newPreds = new BlockSeq();

+          List<Block> newPreds = new List<Block>();

           foreach ( Block p in header.Predecessors )

           {

             if ( p != backEdgeNode )

@@ -2328,7 +2328,7 @@ namespace VC {
         var cex = cexInfo.counterexample;

         // Go through all blocks in the trace, map them back to blocks in the original program (if there is one)

         var ret = cex.Clone();

-        ret.Trace = new BlockSeq();

+        ret.Trace = new List<Block>();

         ret.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

 

         for (int numBlock = 0; numBlock < cex.Trace.Count; numBlock ++ )

@@ -2448,7 +2448,7 @@ namespace VC {
     }

 

     static Counterexample TraceCounterexample(

-                          Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, Model errModel, ModelViewInfo mvInfo,

+                          Block/*!*/ b, Hashtable/*!*/ traceNodes, List<Block>/*!*/ trace, Model errModel, ModelViewInfo mvInfo,

                           Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap,

                           ProverContext/*!*/ context,

                           Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples)

@@ -2493,7 +2493,7 @@ namespace VC {
       return null;

     }

 

-    public static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context) 

+    public static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, List<Block> trace, Model errModel, ModelViewInfo mvInfo, ProverContext context) 

     {

       Contract.Requires(cmd != null);

       Contract.Requires(transferCmd != null);

@@ -3024,13 +3024,13 @@ namespace VC {
     /// Remove the empty blocks reachable from the block.

     /// It changes the visiting state of the blocks, so that if you want to visit again the blocks, you have to reset them...

     /// </summary>

-    static BlockSeq RemoveEmptyBlocks(Block b) {

+    static List<Block> RemoveEmptyBlocks(Block b) {

       Contract.Requires(b != null);

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

+      Contract.Ensures(Contract.Result<List<Block>>() != null);

 

       Contract.Assert(b.TraversingStatus == Block.VisitState.ToVisit);

       Block renameInfo;

-      BlockSeq retVal = removeEmptyBlocksWorker(b, true, out renameInfo);

+      List<Block> retVal = removeEmptyBlocksWorker(b, true, out renameInfo);

       if (renameInfo != null && !b.tok.IsValid) {

         bool onlyAssumes = true;

         foreach (Cmd c in b.Cmds) {

@@ -3054,14 +3054,14 @@ namespace VC {
     /// If renameInfoForStartBlock is non-null, it denotes an empty block with location information, and that

     /// information would be appropriate to display

     /// </summary>

-    private static BlockSeq removeEmptyBlocksWorker(Block b, bool startNode, out Block renameInfoForStartBlock)

+    private static List<Block> removeEmptyBlocksWorker(Block b, bool startNode, out Block renameInfoForStartBlock)

   {

       Contract.Requires(b != null);

       Contract.Ensures(Contract.ValueAtReturn(out renameInfoForStartBlock) == null || Contract.ValueAtReturn(out renameInfoForStartBlock).tok.IsValid);

       // ensures: b in result ==> renameInfoForStartBlock == null;

     

       renameInfoForStartBlock = null;

-      BlockSeq bs = new BlockSeq();

+      List<Block> bs = new List<Block>();

       GotoCmd gtc = b.TransferCmd as GotoCmd;

 

       // b has no successors

@@ -3103,7 +3103,7 @@ namespace VC {
         int m = 0;  // in the following loop, set renameInfoForStartBlock to the value that all recursive calls agree on, if possible; otherwise, null

         foreach (Block dest in gtc.labelTargets){Contract.Assert(dest != null);

           Block renameInfo;

-          BlockSeq ys = removeEmptyBlocksWorker(dest, false, out renameInfo);

+          List<Block> ys = removeEmptyBlocksWorker(dest, false, out renameInfo);

           Contract.Assert(ys != null);

           if (m == 0) {

             renameInfoForStartBlock = renameInfo;

@@ -3118,7 +3118,7 @@ namespace VC {
         }

         b.TraversingStatus = Block.VisitState.AlreadyVisited;

 

-        BlockSeq setOfSuccessors = new BlockSeq();

+        List<Block> setOfSuccessors = new List<Block>();

         foreach (Block d in mergedSuccessors)

           setOfSuccessors.Add(d);

         if (b.Cmds.Count == 0 && !startNode) {

@@ -3137,11 +3137,11 @@ namespace VC {
         if (!startNode) {

           renameInfoForStartBlock = null;

         }

-        return new BlockSeq(b);

+        return new List<Block> { b };

       }

       else // b has some successors, but we are already visiting it, or we have already visited it...

       {

-        return new BlockSeq(b);

+        return new List<Block> { b };

       }

     }