From f29368964a6233945a16d36109b18073e1983154 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 22:22:48 +0100 Subject: StringSeq: farewell --- Source/Core/Absy.cs | 21 +++++++------------ Source/Core/AbsyCmd.cs | 28 ++++++++++++------------- Source/Core/BoogiePL.atg | 4 ++-- Source/Core/Inline.cs | 14 ++++++------- Source/Core/InterProceduralReachabilityGraph.cs | 6 +++--- Source/Core/OwickiGries.cs | 6 +++--- Source/Core/Parser.cs | 4 ++-- 7 files changed, 38 insertions(+), 45 deletions(-) (limited to 'Source/Core') 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/*!*/ newLabels = new List(); 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/*!*/ blocks = new List(); Block exit = new Block(Token.NoToken, "exit", new List(), new ReturnCmd(Token.NoToken)); GotoCmd cmd = new GotoCmd(Token.NoToken, - new StringSeq(cce.NonNull(blockMap[header]).Label, exit.Label), + new List { 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 { 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 newLabels = new List(); 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 { loopHeaderToCallCmd1[header] }; - header.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(lastIterBlockName), new BlockSeq(lastIterBlock)); + header.TransferCmd = new GotoCmd(Token.NoToken, new List { 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 newLabelNames = new List(); newLabelNames.AddRange(splitGotoCmd.labelNames); BlockSeq newLabelTargets = new BlockSeq(); newLabelTargets.AddRange(splitGotoCmd.labelTargets); @@ -3264,13 +3264,6 @@ namespace Microsoft.Boogie { } } - public sealed class StringSeq : List { - public StringSeq(params string[]/*!*/ args) - : base(args) { - Contract.Requires(args != null); - } - } - public sealed class BlockSeq : List { 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 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 { 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 { 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 { 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 { 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 { 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 { 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 { 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 { 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 { runOffTheEndLabel }); } else { trCmd = GotoSuccessor(ifcmd.tok, b); } @@ -635,7 +635,7 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); if (b.successorBigBlock != null) { - return new GotoCmd(tok, new StringSeq(b.successorBigBlock.LabelName)); + return new GotoCmd(tok, new List { 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 labelNames; [Rep] public BlockSeq labelTargets; @@ -2698,13 +2698,13 @@ namespace Microsoft.Boogie { } [NotDelayed] - public GotoCmd(IToken/*!*/ tok, StringSeq/*!*/ labelSeq) + public GotoCmd(IToken/*!*/ tok, List/*!*/ 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/*!*/ 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 labelSeq = new List(); 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 TransferCmd = (. Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; Token y; List/*!*/ xs; - StringSeq ss = new StringSeq(); + List ss = new List(); .) ( "goto" (. y = t; .) Idents (. foreach(IToken/*!*/ s in xs){ @@ -1316,7 +1316,7 @@ SpecBlock Cmd c; IToken label; List cs = new List(); List/*!*/ xs; - StringSeq ss = new StringSeq(); + List ss = new List(); 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 { 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 { 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 { 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 gotoSeq = gotoCmd.labelNames; + List newGotoSeq = new List(); 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 { 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 labels = new List(); 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 { newProcedureEntryNodes[proc].Label }; } } #endregion @@ -164,7 +164,7 @@ namespace Microsoft.Boogie newBlock = new Block(b.tok, label, new List(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 { 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 { 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 yieldCheckerBlocks = new List(); - StringSeq labels = new StringSeq(); + List labels = new List(); BlockSeq labelTargets = new BlockSeq(); Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List(), 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 { 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 { new AssignCmd(Token.NoToken, lhss, rhss) }, new GotoCmd(Token.NoToken, new List { 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 labelTargets = new List(); 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/*!*/ ins, out List/*!*/ outs, out QKeyValue kv) { void TransferCmd(out TransferCmd/*!*/ tc) { Contract.Ensures(Contract.ValueAtReturn(out tc) != null); tc = dummyTransferCmd; Token y; List/*!*/ xs; - StringSeq ss = new StringSeq(); + List ss = new List(); if (la.kind == 38) { Get(); @@ -1926,7 +1926,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Cmd c; IToken label; List cs = new List(); List/*!*/ xs; - StringSeq ss = new StringSeq(); + List ss = new List(); b = dummyBlock; Expr/*!*/ e; -- cgit v1.2.3