StringSeq: farewell

7 files changed, 38 insertions, 45 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 8d68102a..1d6e6a30 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -624,7 +624,7 @@ namespace Microsoft.Boogie {
 

           GotoCmd gotoCmd = source.TransferCmd as GotoCmd;

           Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Count >= 1);

-          StringSeq/*!*/ newLabels = new StringSeq();

+          List<String>/*!*/ newLabels = new List<String>();

           BlockSeq/*!*/ newTargets = new BlockSeq();

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

             if (gotoCmd.labelTargets[i] == header)

@@ -641,12 +641,12 @@ namespace Microsoft.Boogie {
         List<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>();

         Block exit = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

         GotoCmd cmd = new GotoCmd(Token.NoToken,

-                                    new StringSeq(cce.NonNull(blockMap[header]).Label, exit.Label),

+                                    new List<String> { cce.NonNull(blockMap[header]).Label, exit.Label },

                                     new BlockSeq(blockMap[header], exit));

 

         if (detLoopExtract) //cutting the non-determinism

             cmd = new GotoCmd(Token.NoToken,

-                                    new StringSeq(cce.NonNull(blockMap[header]).Label),

+                                    new List<String> { cce.NonNull(blockMap[header]).Label },

                                     new BlockSeq(blockMap[header]));

 

         Block entry;

@@ -667,7 +667,7 @@ namespace Microsoft.Boogie {
             newBlock.TransferCmd = new ReturnCmd(Token.NoToken);

           } else {

             Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null);

-            StringSeq newLabels = new StringSeq();

+            List<String> newLabels = new List<String>();

             BlockSeq newTargets = new BlockSeq();

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

               Block target = gotoCmd.labelTargets[i];

@@ -701,7 +701,7 @@ namespace Microsoft.Boogie {
         Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd);

         newBlocksCreated[header] = lastIterBlock;

         header.Cmds = new List<Cmd> { loopHeaderToCallCmd1[header] };

-        header.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(lastIterBlockName), new BlockSeq(lastIterBlock));

+        header.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { lastIterBlockName }, new BlockSeq(lastIterBlock));

         impl.Blocks.Add(lastIterBlock);

         blockMap[origHeader] = blockMap[header];

         blockMap.Remove(header);

@@ -828,7 +828,7 @@ namespace Microsoft.Boogie {
             newTransferCmd = new ReturnCmd(splitCandidate.tok);

           }

           else {

-            StringSeq newLabelNames = new StringSeq();

+            List<String> newLabelNames = new List<String>();

             newLabelNames.AddRange(splitGotoCmd.labelNames);

             BlockSeq newLabelTargets = new BlockSeq();

             newLabelTargets.AddRange(splitGotoCmd.labelTargets);

@@ -3264,13 +3264,6 @@ namespace Microsoft.Boogie {
     }

   }

 

-  public sealed class StringSeq : List<String> {

-    public StringSeq(params string[]/*!*/ args)

-      : base(args) {

-      Contract.Requires(args != null);

-    }

-  }

-

   public sealed class BlockSeq : List<Block> {

     public BlockSeq(params Block[]/*!*/ args)

       : base(args) {

@@ -3299,7 +3292,7 @@ namespace Microsoft.Boogie {
       }

     }

 

-    public static void Emit(this StringSeq ss, TokenTextWriter stream) {

+    public static void Emit(this List<String> ss, TokenTextWriter stream) {

       Contract.Requires(stream != null);

       string sep = "";

       foreach (string/*!*/ s in ss) {

diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index a11d53a2..635b82f2 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -479,7 +479,7 @@ namespace Microsoft.Boogie {
           TransferCmd trCmd;

           if (n == 0 && runOffTheEndLabel != null) {

             // goto the given label instead of the textual successor block

-            trCmd = new GotoCmd(stmtList.EndCurly, new StringSeq(runOffTheEndLabel));

+            trCmd = new GotoCmd(stmtList.EndCurly, new List<String> { runOffTheEndLabel });

           } else {

             trCmd = GotoSuccessor(stmtList.EndCurly, b);

           }

@@ -515,7 +515,7 @@ namespace Microsoft.Boogie {
           bool bodyGuardTakenCareOf = wcmd.Body.PrefixFirstBlock(ssBody, ref loopBodyLabel);

 

           // ... goto LoopHead;

-          Block block = new Block(b.tok, b.LabelName, theSimpleCmds, new GotoCmd(wcmd.tok, new StringSeq(loopHeadLabel)));

+          Block block = new Block(b.tok, b.LabelName, theSimpleCmds, new GotoCmd(wcmd.tok, new List<String> { loopHeadLabel }));

           blocks.Add(block);

 

           // LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody;

@@ -523,12 +523,12 @@ namespace Microsoft.Boogie {
           foreach (PredicateCmd inv in wcmd.Invariants) {

             ssHead.Add(inv);

           }

-          block = new Block(wcmd.tok, loopHeadLabel, ssHead, new GotoCmd(wcmd.tok, new StringSeq(loopDoneLabel, loopBodyLabel)));

+          block = new Block(wcmd.tok, loopHeadLabel, ssHead, new GotoCmd(wcmd.tok, new List<String> { loopDoneLabel, loopBodyLabel }));

           blocks.Add(block);

 

           if (!bodyGuardTakenCareOf) {

             // LoopBody: assume guard; goto firstLoopBlock;

-            block = new Block(wcmd.tok, loopBodyLabel, ssBody, new GotoCmd(wcmd.tok, new StringSeq(wcmd.Body.BigBlocks[0].LabelName)));

+            block = new Block(wcmd.tok, loopBodyLabel, ssBody, new GotoCmd(wcmd.tok, new List<String> { wcmd.Body.BigBlocks[0].LabelName }));

             blocks.Add(block);

           }

 

@@ -539,7 +539,7 @@ namespace Microsoft.Boogie {
           TransferCmd trCmd;

           if (n == 0 && runOffTheEndLabel != null) {

             // goto the given label instead of the textual successor block

-            trCmd = new GotoCmd(wcmd.tok, new StringSeq(runOffTheEndLabel));

+            trCmd = new GotoCmd(wcmd.tok, new List<String> { runOffTheEndLabel });

           } else {

             trCmd = GotoSuccessor(wcmd.tok, b);

           }

@@ -579,12 +579,12 @@ namespace Microsoft.Boogie {
 

             // ... goto Then, Else;

             Block block = new Block(b.tok, predLabel, predCmds,

-              new GotoCmd(ifcmd.tok, new StringSeq(thenLabel, elseLabel)));

+              new GotoCmd(ifcmd.tok, new List<String> { thenLabel, elseLabel }));

             blocks.Add(block);

 

             if (!thenGuardTakenCareOf) {

               // Then: assume guard; goto firstThenBlock;

-              block = new Block(ifcmd.tok, thenLabel, ssThen, new GotoCmd(ifcmd.tok, new StringSeq(ifcmd.thn.BigBlocks[0].LabelName)));

+              block = new Block(ifcmd.tok, thenLabel, ssThen, new GotoCmd(ifcmd.tok, new List<String> { ifcmd.thn.BigBlocks[0].LabelName }));

               blocks.Add(block);

             }

 

@@ -595,7 +595,7 @@ namespace Microsoft.Boogie {
               Contract.Assert(ifcmd.elseIf == null);

               if (!elseGuardTakenCareOf) {

                 // Else: assume !guard; goto firstElseBlock;

-                block = new Block(ifcmd.tok, elseLabel, ssElse, new GotoCmd(ifcmd.tok, new StringSeq(ifcmd.elseBlock.BigBlocks[0].LabelName)));

+                block = new Block(ifcmd.tok, elseLabel, ssElse, new GotoCmd(ifcmd.tok, new List<String> { ifcmd.elseBlock.BigBlocks[0].LabelName }));

                 blocks.Add(block);

               }

 

@@ -618,7 +618,7 @@ namespace Microsoft.Boogie {
               TransferCmd trCmd;

               if (n == 0 && runOffTheEndLabel != null) {

                 // goto the given label instead of the textual successor block

-                trCmd = new GotoCmd(ifcmd.tok, new StringSeq(runOffTheEndLabel));

+                trCmd = new GotoCmd(ifcmd.tok, new List<String> { runOffTheEndLabel });

               } else {

                 trCmd = GotoSuccessor(ifcmd.tok, b);

               }

@@ -635,7 +635,7 @@ namespace Microsoft.Boogie {
       Contract.Requires(tok != null);

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

       if (b.successorBigBlock != null) {

-        return new GotoCmd(tok, new StringSeq(b.successorBigBlock.LabelName));

+        return new GotoCmd(tok, new List<String> { b.successorBigBlock.LabelName });

       } else {

         return new ReturnCmd(tok);

       }

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

   public class GotoCmd : TransferCmd {

     [Rep]

-    public StringSeq labelNames;

+    public List<String> labelNames;

     [Rep]

     public BlockSeq labelTargets;

 

@@ -2698,13 +2698,13 @@ namespace Microsoft.Boogie {
     }

 

     [NotDelayed]

-    public GotoCmd(IToken/*!*/ tok, StringSeq/*!*/ labelSeq)

+    public GotoCmd(IToken/*!*/ tok, List<String>/*!*/ labelSeq)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(labelSeq != null);

       this.labelNames = labelSeq;

     }

-    public GotoCmd(IToken/*!*/ tok, StringSeq/*!*/ labelSeq, BlockSeq/*!*/ blockSeq)

+    public GotoCmd(IToken/*!*/ tok, List<String>/*!*/ labelSeq, BlockSeq/*!*/ blockSeq)

       : base(tok) {

       Contract.Requires(tok != null);

       Contract.Requires(labelSeq != null);

@@ -2721,7 +2721,7 @@ namespace Microsoft.Boogie {
       : base(tok) { //requires (blockSeq[i] != null ==> blockSeq[i].Label != null);

       Contract.Requires(tok != null);

       Contract.Requires(blockSeq != null);

-      StringSeq labelSeq = new StringSeq();

+      List<String> labelSeq = new List<String>();

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

         labelSeq.Add(cce.NonNull(blockSeq[i]).Label);

       this.labelNames = labelSeq;

diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg
index a8a03567..dec0b3a8 100644
--- a/Source/Core/BoogiePL.atg
+++ b/Source/Core/BoogiePL.atg
@@ -750,7 +750,7 @@ StmtList<out StmtList/*!*/ stmtList>
 TransferCmd<out TransferCmd/*!*/ tc>

 = (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;

      Token y;  List<IToken>/*!*/ xs;

-     StringSeq ss = new StringSeq();

+     List<String> ss = new List<String>();

   .)

   ( "goto"             (. y = t; .)

     Idents<out xs>     (. foreach(IToken/*!*/ s in xs){

@@ -1316,7 +1316,7 @@ SpecBlock<out Block/*!*/ b>
      Cmd c;  IToken label;

      List<Cmd> cs = new List<Cmd>();

      List<IToken>/*!*/ xs;

-     StringSeq ss = new StringSeq();

+     List<String> ss = new List<String>();

      b = dummyBlock;

      Expr/*!*/ e;

   .)

diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs
index 0d412fbc..70daa7da 100644
--- a/Source/Core/Inline.cs
+++ b/Source/Core/Inline.cs
@@ -289,7 +289,7 @@ namespace Microsoft.Boogie {
               Block/*!*/ startBlock = inlinedBlocks[0];

               Contract.Assert(startBlock != null);

 

-              GotoCmd gotoCmd = new GotoCmd(Token.NoToken, new StringSeq(startBlock.Label));

+              GotoCmd gotoCmd = new GotoCmd(Token.NoToken, new List<String> { startBlock.Label });

               newBlock = new Block(block.tok, ((lblCount == 0) ? (label) : (label + "$" + lblCount)), newCmds, gotoCmd);

 

               newBlocks.Add(newBlock);

@@ -509,7 +509,7 @@ namespace Microsoft.Boogie {
         inCmds.Add(assign);

       }

 

-      GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new StringSeq(GetInlinedProcLabel(proc.Name) + "$" + startLabel));

+      GotoCmd inGotoCmd = new GotoCmd(callCmd.tok, new List<String> { GetInlinedProcLabel(proc.Name) + "$" + startLabel });

       Block inBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Entry", inCmds, inGotoCmd);

       inlinedBlocks.Add(inBlock);

 

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

 

       // create out block

-      GotoCmd outGotoCmd = new GotoCmd(Token.NoToken, new StringSeq(nextBlockLabel));

+      GotoCmd outGotoCmd = new GotoCmd(Token.NoToken, new List<String> { nextBlockLabel });

       Block outBlock = new Block(impl.tok, GetInlinedProcLabel(proc.Name) + "$Return", outCmds, outGotoCmd);

       inlinedBlocks.Add(outBlock);

 

@@ -556,15 +556,15 @@ namespace Microsoft.Boogie {
 

       GotoCmd gotoCmd = transferCmd as GotoCmd;

       if (gotoCmd != null) {

-        StringSeq gotoSeq = gotoCmd.labelNames;

-        StringSeq newGotoSeq = new StringSeq();

+        List<String> gotoSeq = gotoCmd.labelNames;

+        List<String> newGotoSeq = new List<String>();

         foreach (string/*!*/ blockLabel in cce.NonNull(gotoSeq)) {

           Contract.Assert(blockLabel != null);

           newGotoSeq.Add(procLabel + "$" + blockLabel);

         }

         newTransferCmd = new GotoCmd(transferCmd.tok, newGotoSeq);

       } else {

-        newTransferCmd = new GotoCmd(transferCmd.tok, new StringSeq(procLabel + "$Return"));

+        newTransferCmd = new GotoCmd(transferCmd.tok, new List<String> { procLabel + "$Return" });

       }

 

       return newTransferCmd;

@@ -621,7 +621,7 @@ namespace Microsoft.Boogie {
       GotoCmd gotocmd = cmd as GotoCmd;

       if (gotocmd != null) {

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

-        StringSeq labels = new StringSeq();

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

         labels.AddRange(gotocmd.labelNames);

         transferCmd = new GotoCmd(cmd.tok, labels);

       } else {

diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index eb34065f..c8941bbf 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -83,7 +83,7 @@ namespace Microsoft.Boogie
             (newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]);

           }

           gotoCmd.labelTargets = new BlockSeq { newProcedureEntryNodes[proc] };

-          gotoCmd.labelNames = new StringSeq { newProcedureEntryNodes[proc].Label };

+          gotoCmd.labelNames = new List<String> { newProcedureEntryNodes[proc].Label };

         }

       }

       #endregion

@@ -164,7 +164,7 @@ namespace Microsoft.Boogie
               newBlock = new Block(b.tok, label, new List<Cmd>(cmds.ToArray()), null);

               nodes.Add(newBlock);

               originalToNew[newBlock] = newBlock;

-              prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { label }, new BlockSeq { newBlock });

+              prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { label }, new BlockSeq { newBlock });

             }

             prev = newBlock;

             i++;

@@ -173,7 +173,7 @@ namespace Microsoft.Boogie
           if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd &&

               ((GotoCmd)b.TransferCmd).labelTargets.Count == 0))

           {

-            prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { exitLabel }, new BlockSeq { newExit });

+            prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { exitLabel }, new BlockSeq { newExit });

           }

           else

           {

diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index 1d0eb0fd..eaecf887 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie
             Substitution oldSubst = Substituter.SubstitutionFromHashtable(ogOldLocalMap);

             Substitution subst = Substituter.SubstitutionFromHashtable(map);

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

-            StringSeq labels = new StringSeq();

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

             BlockSeq labelTargets = new BlockSeq();

             Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));

             labels.Add(yieldCheckerBlock.Label);

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

                 if (lhss.Count > 0)

                 {

-                    Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0])));

+                    Block initBlock = new Block(Token.NoToken, "og_init", new List<Cmd> { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List<String> { impl.Blocks[0].Label }, new BlockSeq(impl.Blocks[0])));

                     impl.Blocks.Insert(0, initBlock);

                 }

             }

@@ -740,7 +740,7 @@ namespace Microsoft.Boogie
             if (yieldCheckerProcs.Count > 0)

             {

                 BlockSeq blockTargets = new BlockSeq();

-                StringSeq labelTargets = new StringSeq();

+                List<String> labelTargets = new List<String>();

                 int labelCount = 0;

                 foreach (Procedure proc in yieldCheckerProcs)

                 {

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index bcdd01d8..17e4b0fb 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -1074,7 +1074,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) {
 	void TransferCmd(out TransferCmd/*!*/ tc) {

 		Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd;

 		Token y;  List<IToken>/*!*/ xs;

-		StringSeq ss = new StringSeq();

+		List<String> ss = new List<String>();

 		

 		if (la.kind == 38) {

 			Get();

@@ -1926,7 +1926,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 		Cmd c;  IToken label;

 		List<Cmd> cs = new List<Cmd>();

 		List<IToken>/*!*/ xs;

-		StringSeq ss = new StringSeq();

+		List<String> ss = new List<String>();

 		b = dummyBlock;

 		Expr/*!*/ e;