More refactoring towards replacing PureCollections.Sequence with List

5 files changed, 52 insertions, 52 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index dbe20415..fe8d67f5 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -123,9 +123,9 @@ namespace Microsoft.Boogie {
     // Looks up the Cmd at a given index into the trace

     public Cmd getTraceCmd(TraceLocation loc)

     {

-        Debug.Assert(loc.numBlock < Trace.Length);

+        Debug.Assert(loc.numBlock < Trace.Count);

         Block b = Trace[loc.numBlock];

-        Debug.Assert(loc.numInstr < b.Cmds.Length);

+        Debug.Assert(loc.numInstr < b.Cmds.Count);

         return b.Cmds[loc.numInstr];

     }

 

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

             tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);

 

-            for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)

+            for (int numInstr = 0; numInstr < b.Cmds.Count; numInstr++)

             {

                 var loc = new TraceLocation(numBlock, numInstr);

                 if (calleeCounterexamples.ContainsKey(loc))

@@ -314,16 +314,16 @@ namespace Microsoft.Boogie {
 

     private int Compare(BlockSeq bs1, BlockSeq bs2)

     {

-      if (bs1.Length < bs2.Length)

+      if (bs1.Count < bs2.Count)

       {

         return -1;

       }

-      else if (bs2.Length < bs1.Length)

+      else if (bs2.Count < bs1.Count)

       {

         return 1;

       }

 

-      for (int i = 0; i < bs1.Length; i++)

+      for (int i = 0; i < bs1.Count; i++)

       {

         var b1 = bs1[i];

         var b2 = bs2[i];

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

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

 

-      if (b.Predecessors.Length == 0) {

+      if (b.Predecessors.Count == 0) {

         return new Dictionary<Variable, Expr>();

       }

 

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

         else {

           // incarnationMap needs to be added only if there is some successor of b

-          b.succCount = gotoCmd.labelNames.Length;

+          b.succCount = gotoCmd.labelNames.Count;

           block2Incarnation.Add(b, incarnationMap);

         }

         #endregion Each block's map needs to be available to successor blocks

@@ -1608,7 +1608,7 @@ namespace VC {
     /// succ.  Caller must do the add to impl.Blocks.

     /// </summary>

     protected Block CreateBlockBetween(int predIndex, Block succ) {

-      Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Length);

+      Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Count);

 

 

       Contract.Requires(succ != null);

@@ -1641,7 +1641,7 @@ namespace VC {
       GotoCmd gtc = (GotoCmd)cce.NonNull(pred.TransferCmd);

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

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

-      for (int i = 0, n = gtc.labelTargets.Length; i < n; i++) {

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

         if (gtc.labelTargets[i] == succ) {

           gtc.labelTargets[i] = newBlock;

           gtc.labelNames[i] = newBlockLabel;

@@ -1661,12 +1661,12 @@ namespace VC {
       #region Introduce empty blocks between join points and their multi-successor predecessors

       List<Block> tweens = new List<Block>();

       foreach (Block b in blocks) {

-        int nPreds = b.Predecessors.Length;

+        int nPreds = b.Predecessors.Count;

         if (nPreds > 1) {

           // b is a join point (i.e., it has more than one predecessor)

           for (int i = 0; i < nPreds; i++) {

             GotoCmd gotocmd = (GotoCmd)(cce.NonNull(b.Predecessors[i]).TransferCmd);

-            if (gotocmd.labelNames != null && gotocmd.labelNames.Length > 1) {

+            if (gotocmd.labelNames != null && gotocmd.labelNames.Count > 1) {

               tweens.Add(CreateBlockBetween(i, b));

             }

           }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 78ed8cb5..ac7ee9be 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -253,7 +253,7 @@ namespace Microsoft.Boogie
             info.type = AnnotationInfo.AnnotationType.LoopInvariant;

             annotationInfo.Add(name, info);

             // get file and line info from havoc, if there is...

-            if (header.Cmds.Length > 0)

+            if (header.Cmds.Count > 0)

             {

                 PredicateCmd bif = header.Cmds[0] as PredicateCmd;

                 if (bif != null)

@@ -1177,7 +1177,7 @@ namespace Microsoft.Boogie
                         }

 

                         CmdSeq cmds = block.Cmds;

-                        int len = cmds.Length;

+                        int len = cmds.Count;

                         for (int i = len - 1; i >= 0; i--)

                         {

                             if (cmds[i] is CallCmd)

@@ -1657,7 +1657,7 @@ namespace Microsoft.Boogie
 

                 CmdSeq cmds = b.Cmds;

                 TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

-                for (int i = 0; i < cmds.Length; i++)

+                for (int i = 0; i < cmds.Count; i++)

                 {

                     Cmd cmd = cce.NonNull(cmds[i]);

 

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

                             RPFP.Node callee = root.Outgoing.Children[pos];

                             orderedStateIds.Add(new StateId(callee.Outgoing, CALL,info));

-                            calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

+                            calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =

                                 new CalleeCounterexampleInfo(

                                     cce.NonNull(GenerateTrace(rpfp, callee, orderedStateIds,

                                                 implName2StratifiedInliningInfo[calleeName].impl, false)),

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index da413984..c5d88c5c 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -360,7 +360,7 @@ namespace VC {
       var callSiteId = 0;

       foreach (Block block in implementation.Blocks) {

         CmdSeq newCmds = new CmdSeq();

-        for (int i = 0; i < block.Cmds.Length; i++) {

+        for (int i = 0; i < block.Cmds.Count; i++) {

           Cmd cmd = block.Cmds[i];

           newCmds.Add(cmd);

           AssumeCmd assumeCmd = cmd as AssumeCmd;

@@ -380,7 +380,7 @@ namespace VC {
     public Dictionary<Block, List<CallSite>> CollectCallSites(Implementation implementation) {

       var callSites = new Dictionary<Block, List<CallSite>>();

       foreach (Block block in implementation.Blocks) {

-        for (int i = 0; i < block.Cmds.Length; i++) {

+        for (int i = 0; i < block.Cmds.Count; i++) {

           Cmd cmd = block.Cmds[i];

           AssumeCmd assumeCmd = cmd as AssumeCmd;

           if (assumeCmd == null) continue;

@@ -407,7 +407,7 @@ namespace VC {
     public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {

       var callSites = new Dictionary<Block, List<CallSite>>();

       foreach (Block block in implementation.Blocks) {

-        for (int i = 0; i < block.Cmds.Length; i++) {

+        for (int i = 0; i < block.Cmds.Count; i++) {

           AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;

           if (assumeCmd == null) continue;

           NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

@@ -2584,7 +2584,7 @@ namespace VC {
         while (true) {

           CmdSeq cmds = b.Cmds;

           TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

-          for (int i = 0; i < cmds.Length; i++) {

+          for (int i = 0; i < cmds.Count; i++) {

             Cmd cmd = cce.NonNull(cmds[i]);

 

             // Skip if 'cmd' not contained in the trace or not an assert

@@ -2662,7 +2662,7 @@ namespace VC {
                       Contract.Assert(false);

                   }

               }

-              calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

+              calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =

                    new CalleeCounterexampleInfo(null, args);

               continue;

             }

@@ -2680,7 +2680,7 @@ namespace VC {
             else {

               orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));

               var calleeInfo = implName2StratifiedInliningInfo[calleeName];

-              calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

+              calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =

                   new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<object>());

               orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));

             }

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 055a79ad..873a5589 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -415,9 +415,9 @@ namespace VC {
         GotoCmd go = cur.TransferCmd as GotoCmd;

         ReturnCmd ret = cur.TransferCmd as ReturnCmd;

 

-        Contract.Assume(!(go != null && go.labelTargets == null && go.labelNames != null && go.labelNames.Length > 0));

+        Contract.Assume(!(go != null && go.labelTargets == null && go.labelNames != null && go.labelNames.Count > 0));

 

-        if (ret != null || (go != null && cce.NonNull(go.labelTargets).Length == 0)) {

+        if (ret != null || (go != null && cce.NonNull(go.labelTargets).Count == 0)) {

           // we end in return, so there will be no more places to check

           CheckUnreachable(cur, seq);

         } else if (go != null) {

@@ -426,7 +426,7 @@ namespace VC {
           // we're in the right place to check

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

             Contract.Assert(target != null);

-            if (target.Predecessors.Length == 1) {

+            if (target.Predecessors.Count == 1) {

               needToCheck = false;

             }

           }

@@ -668,7 +668,7 @@ namespace VC {
           Block next = s.virtual_successors[0];

           BlockStats se = GetBlockStats(next);

           CountAssertions(next);

-          if (next.Predecessors.Length > 1 || se.virtual_successors.Count != 1)

+          if (next.Predecessors.Count > 1 || se.virtual_successors.Count != 1)

             return;

           s.virtual_successors[0] = se.virtual_successors[0];

           s.assertion_cost += se.assertion_cost;

@@ -745,7 +745,7 @@ namespace VC {
           if (gt == null)

             continue;

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

-          if (targ.Length < 2)

+          if (targ.Count < 2)

             continue;

           // caution, we only consider two first exits

 

@@ -758,7 +758,7 @@ namespace VC {
           right0 = DoComputeScore(false);

 

           assumized_branches.Clear();

-          for (int idx = 1; idx < targ.Length; idx++) {

+          for (int idx = 1; idx < targ.Count; idx++) {

             assumized_branches.Add(cce.NonNull(targ[idx]));

           }

           left1 = DoComputeScore(true);

@@ -1314,7 +1314,7 @@ namespace VC {
           cache.Add(t);

         }

 

-        for (int i = 0; i < orig.Cmds.Length; ++i) {

+        for (int i = 0; i < orig.Cmds.Count; ++i) {

           Cmd cmd = orig.Cmds[i];

           if (cmd is AssertCmd) {

             int found = 0;

@@ -1913,7 +1913,7 @@ namespace VC {
         #region Find the (possibly empty) prefix of assert commands in the header, replace each assert with an assume of the same condition

         CmdSeq prefixOfPredicateCmdsInit = new CmdSeq();

         CmdSeq prefixOfPredicateCmdsMaintained = new CmdSeq();

-        for (int i = 0, n = header.Cmds.Length; i < n; i++)

+        for (int i = 0, n = header.Cmds.Count; i < n; i++)

         {

           PredicateCmd a = header.Cmds[i] as PredicateCmd;

           if (a != null)

@@ -1952,14 +1952,14 @@ namespace VC {
         #endregion

 

         #region Copy the prefix of predicate commands into each predecessor. Do this *before* cutting the backedge!!

-        for ( int predIndex = 0, n = header.Predecessors.Length; predIndex < n; predIndex++ )

+        for ( int predIndex = 0, n = header.Predecessors.Count; predIndex < n; predIndex++ )

         {

           Block pred = cce.NonNull(header.Predecessors[predIndex]);

           

           // Create a block between header and pred for the predicate commands if pred has more than one successor 

           GotoCmd gotocmd = cce.NonNull((GotoCmd)pred.TransferCmd);

           Contract.Assert( gotocmd.labelNames != null);  // if "pred" is really a predecessor, it may be a GotoCmd with at least one label

-          if (gotocmd.labelNames.Length > 1)

+          if (gotocmd.labelNames.Count > 1)

           {

             Block newBlock = CreateBlockBetween(predIndex, header);

             impl.Blocks.Add(newBlock);

@@ -1988,13 +1988,13 @@ namespace VC {
         {Contract.Assert(backEdgeNode != null);

           Debug.Assert(backEdgeNode.TransferCmd is GotoCmd,"An node was identified as the source for a backedge, but it does not have a goto command.");

           GotoCmd gtc = backEdgeNode.TransferCmd as GotoCmd;

-          if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length > 1 )

+          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();

             StringSeq remainingLabels = new StringSeq();

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

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

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

             {

                 if (gtc.labelTargets[i] != header)

                 {

@@ -2015,7 +2015,7 @@ namespace VC {
             AssumeCmd ac = new AssumeCmd(Token.NoToken,Expr.False);

             backEdgeNode.Cmds.Add(ac);

             backEdgeNode.TransferCmd = new ReturnCmd(Token.NoToken);

-            if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length == 1)

+            if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Count == 1)

                 RecordCutEdge(edgesCut, backEdgeNode, gtc.labelTargets[0]);

           }

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

@@ -2331,13 +2331,13 @@ namespace VC {
         ret.Trace = new BlockSeq();

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

 

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

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

         {

             Block block = cex.Trace[numBlock];

             var origBlock = elGetBlock(currProc, block, extractLoopMappingInfo);

             if (origBlock != null) ret.Trace.Add(origBlock);

             var callCnt = 1;

-            for (int numInstr = 0; numInstr < block.Cmds.Length; numInstr ++) {

+            for (int numInstr = 0; numInstr < block.Cmds.Count; numInstr ++) {

                 Cmd cmd = block.Cmds[numInstr];

                 var loc = new TraceLocation(numBlock, numInstr);

                 if (!cex.calleeCounterexamples.ContainsKey(loc))

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

                     // Absorb the trace into the current trace

 

-                    int currLen = ret.Trace.Length;

+                    int currLen = ret.Trace.Count;

                     ret.Trace.AddRange(origTrace.counterexample.Trace);

 

                     foreach (var kvp in origTrace.counterexample.calleeCounterexamples)

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

                 else

                 {

-                    var origLoc = new TraceLocation(ret.Trace.Length - 1, getCallCmdPosition(origBlock, callCnt, inlinedProcs, callee));

+                    var origLoc = new TraceLocation(ret.Trace.Count - 1, getCallCmdPosition(origBlock, callCnt, inlinedProcs, callee));

                     ret.calleeCounterexamples.Add(origLoc, origTrace);

                     callCnt++;

                 }

@@ -2383,7 +2383,7 @@ namespace VC {
     private int getCallCmdPosition(Block block, int i, HashSet<string> inlinedProcs, string callee)

     {

         Debug.Assert(i >= 1);

-        for (int pos = 0; pos < block.Cmds.Length; pos++)

+        for (int pos = 0; pos < block.Cmds.Count; pos++)

         {

             Cmd cmd = block.Cmds[pos];

             string procCalled = getCallee(cmd, inlinedProcs);

@@ -2463,7 +2463,7 @@ namespace VC {
       CmdSeq cmds = b.Cmds;

       Contract.Assert(cmds != null);

       TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

-      for (int i = 0; i < cmds.Length; i++)

+      for (int i = 0; i < cmds.Count; i++)

       {

         Cmd cmd = cce.NonNull( cmds[i]);

             

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

         else {

           Contract.Assert(gotocmd.labelTargets != null);

-          List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);

+          List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Count);

           foreach (Block successor in gotocmd.labelTargets) {

             Contract.Assert(successor != null);

             VCExpr s = blockVariables[successor];

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

         } else {

           Contract.Assert( gotocmd.labelTargets != null);

-          List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);

+          List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Count);

           foreach (Block successor in gotocmd.labelTargets) {

             Contract.Assert(successor != null);

             int ac;

@@ -3065,9 +3065,9 @@ namespace VC {
       GotoCmd gtc = b.TransferCmd as GotoCmd;

 

       // b has no successors

-      if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Length == 0) 

+      if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Count == 0) 

       {

-        if (b.Cmds.Length != 0){ // only empty blocks are removed...

+        if (b.Cmds.Count != 0){ // only empty blocks are removed...

           bs.Add(b);

         } else if (b.tok.IsValid) {

           renameInfoForStartBlock = b;

@@ -3086,11 +3086,11 @@ namespace VC {
         // by pushing the location onto b's successor.  This can be done if (0) b has

         // exactly one successor, (1) that successor has no location of its own, and

         // (2) that successor has no other predecessors.

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

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

           // b is about to become extinct; try to save its name and location, if possible

-          if (b.tok.IsValid && gtc.labelTargets.Length == 1) {

+          if (b.tok.IsValid && gtc.labelTargets.Count == 1) {

             Block succ = cce.NonNull(gtc.labelTargets[0]);

-            if (!succ.tok.IsValid && succ.Predecessors.Length == 1) {

+            if (!succ.tok.IsValid && succ.Predecessors.Count == 1) {

               succ.tok = b.tok;

               succ.Label = b.Label;

             }

@@ -3121,7 +3121,7 @@ namespace VC {
         BlockSeq setOfSuccessors = new BlockSeq();

         foreach (Block d in mergedSuccessors)

           setOfSuccessors.Add(d);

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

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

           // b is about to become extinct

           if (b.tok.IsValid) {

             renameInfoForStartBlock = b;

diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index eed4e2a5..277d9a94 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -59,7 +59,7 @@ namespace VC {
       

       VCExpr res = N;

 

-      for (int i = b.Cmds.Length; --i >= 0; )

+      for (int i = b.Cmds.Count; --i >= 0; )

       {

         res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);

       }

@@ -200,14 +200,14 @@ namespace VC {
       {

         Choice ch = (Choice) r;

         VCExpr res;

-        if (ch.rs == null || ch.rs.Length==0) 

+        if (ch.rs == null || ch.rs.Count==0) 

         {

           res = N;

         } 

         else 

         {

           VCExpr currentWLP = RegExpr(cce.NonNull(ch.rs[0]), N, ctxt);

-          for (int i = 1, n = ch.rs.Length; i < n; i++)

+          for (int i = 1, n = ch.rs.Count; i < n; i++)

           {

             currentWLP = ctxt.Ctxt.ExprGen.And(currentWLP, RegExpr(cce.NonNull(ch.rs[i]), N, ctxt));

           }