summaryrefslogtreecommitdiff
path: root/Source/Core
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Core')
-rw-r--r--Source/Core/Absy.cs27
-rw-r--r--Source/Core/AbsyCmd.cs12
-rw-r--r--Source/Core/Duplicator.cs8
-rw-r--r--Source/Core/InterProceduralReachabilityGraph.cs12
-rw-r--r--Source/Core/LoopUnroll.cs2
-rw-r--r--Source/Core/OwickiGries.cs6
-rw-r--r--Source/Core/StandardVisitor.cs4
-rw-r--r--Source/Core/Xml.cs4
8 files changed, 32 insertions, 43 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index 1d6e6a30..fa601737 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -625,7 +625,7 @@ namespace Microsoft.Boogie {
GotoCmd gotoCmd = source.TransferCmd as GotoCmd;
Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Count >= 1);
List<String>/*!*/ newLabels = new List<String>();
- BlockSeq/*!*/ newTargets = new BlockSeq();
+ List<Block>/*!*/ newTargets = new List<Block>();
for (int i = 0; i < gotoCmd.labelTargets.Count; i++) {
if (gotoCmd.labelTargets[i] == header)
continue;
@@ -642,12 +642,12 @@ namespace Microsoft.Boogie {
Block exit = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
GotoCmd cmd = new GotoCmd(Token.NoToken,
new List<String> { cce.NonNull(blockMap[header]).Label, exit.Label },
- new BlockSeq(blockMap[header], exit));
+ new List<Block> { blockMap[header], exit });
if (detLoopExtract) //cutting the non-determinism
cmd = new GotoCmd(Token.NoToken,
new List<String> { cce.NonNull(blockMap[header]).Label },
- new BlockSeq(blockMap[header]));
+ new List<Block> { blockMap[header] });
Block entry;
List<Cmd> initCmds = new List<Cmd>();
@@ -668,7 +668,7 @@ namespace Microsoft.Boogie {
} else {
Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null);
List<String> newLabels = new List<String>();
- BlockSeq newTargets = new BlockSeq();
+ List<Block> newTargets = new List<Block>();
for (int i = 0; i < gotoCmd.labelTargets.Count; i++) {
Block target = gotoCmd.labelTargets[i];
if (blockMap.ContainsKey(target)) {
@@ -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 List<String> { lastIterBlockName }, new BlockSeq(lastIterBlock));
+ header.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { lastIterBlockName }, new List<Block> { lastIterBlock });
impl.Blocks.Add(lastIterBlock);
blockMap[origHeader] = blockMap[header];
blockMap.Remove(header);
@@ -830,7 +830,7 @@ namespace Microsoft.Boogie {
else {
List<String> newLabelNames = new List<String>();
newLabelNames.AddRange(splitGotoCmd.labelNames);
- BlockSeq newLabelTargets = new BlockSeq();
+ List<Block> newLabelTargets = new List<Block>();
newLabelTargets.AddRange(splitGotoCmd.labelTargets);
newTransferCmd = new GotoCmd(splitCandidate.tok, newLabelNames, newLabelTargets);
}
@@ -3016,7 +3016,7 @@ namespace Microsoft.Boogie {
foreach (Block/*!*/ block in this.Blocks) {
Contract.Assert(block != null);
- block.Predecessors = new BlockSeq();
+ block.Predecessors = new List<Block>();
}
}
@@ -3070,7 +3070,7 @@ namespace Microsoft.Boogie {
/// </summary>
public void ComputePredecessorsForBlocks() {
foreach (Block b in this.Blocks) {
- b.Predecessors = new BlockSeq();
+ b.Predecessors = new List<Block>();
}
foreach (Block b in this.Blocks) {
GotoCmd gtc = b.TransferCmd as GotoCmd;
@@ -3264,17 +3264,6 @@ namespace Microsoft.Boogie {
}
}
- public sealed class BlockSeq : List<Block> {
- public BlockSeq(params Block[]/*!*/ args)
- : base(args) {
- Contract.Requires(args != null);
- }
- public BlockSeq(BlockSeq blockSeq)
- : base(blockSeq) {
- Contract.Requires(blockSeq != null);
- }
- }
-
public static class Emitter {
public static void Declarations(List<Declaration/*!*/>/*!*/ decls, TokenTextWriter stream) {
Contract.Requires(stream != null);
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs
index 635b82f2..d1f3a845 100644
--- a/Source/Core/AbsyCmd.cs
+++ b/Source/Core/AbsyCmd.cs
@@ -816,7 +816,7 @@ namespace Microsoft.Boogie {
public int iterations; // Count the number of time we visited the block during fixpoint computation. Used to decide if we widen or not
// VC generation and SCC computation
- public BlockSeq/*!*/ Predecessors;
+ public List<Block>/*!*/ Predecessors;
// This field is used during passification to null-out entries in block2Incartion hashtable early
public int succCount;
@@ -849,7 +849,7 @@ namespace Microsoft.Boogie {
this.Label = label;
this.Cmds = cmds;
this.TransferCmd = transferCmd;
- this.Predecessors = new BlockSeq();
+ this.Predecessors = new List<Block>();
this.liveVarsBefore = null;
this.TraversingStatus = VisitState.ToVisit;
this.iterations = 0;
@@ -2690,7 +2690,7 @@ namespace Microsoft.Boogie {
[Rep]
public List<String> labelNames;
[Rep]
- public BlockSeq labelTargets;
+ public List<Block> labelTargets;
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -2704,7 +2704,7 @@ namespace Microsoft.Boogie {
Contract.Requires(labelSeq != null);
this.labelNames = labelSeq;
}
- public GotoCmd(IToken/*!*/ tok, List<String>/*!*/ labelSeq, BlockSeq/*!*/ blockSeq)
+ public GotoCmd(IToken/*!*/ tok, List<String>/*!*/ labelSeq, List<Block>/*!*/ blockSeq)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(labelSeq != null);
@@ -2717,7 +2717,7 @@ namespace Microsoft.Boogie {
this.labelNames = labelSeq;
this.labelTargets = blockSeq;
}
- public GotoCmd(IToken/*!*/ tok, BlockSeq/*!*/ blockSeq)
+ public GotoCmd(IToken/*!*/ tok, List<Block>/*!*/ blockSeq)
: base(tok) { //requires (blockSeq[i] != null ==> blockSeq[i].Label != null);
Contract.Requires(tok != null);
Contract.Requires(blockSeq != null);
@@ -2767,7 +2767,7 @@ namespace Microsoft.Boogie {
return;
}
Contract.Assume(this.labelNames != null);
- labelTargets = new BlockSeq();
+ labelTargets = new List<Block>();
foreach (string/*!*/ lbl in labelNames) {
Contract.Assert(lbl != null);
Block b = rc.LookUpBlock(lbl);
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs
index e59dd27e..3355c9a0 100644
--- a/Source/Core/Duplicator.cs
+++ b/Source/Core/Duplicator.cs
@@ -73,7 +73,7 @@ namespace Microsoft.Boogie {
Contract.Assert(b != null);
GotoCmd g = b.TransferCmd as GotoCmd;
if (g != null) {
- BlockSeq targets = new BlockSeq();
+ List<Block> targets = new List<Block>();
foreach (Block t in cce.NonNull(g.labelTargets)) {
Block nt = subst[t];
targets.Add(nt);
@@ -83,10 +83,10 @@ namespace Microsoft.Boogie {
}
return clone;
}
- public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) {
+ public override List<Block> VisitBlockSeq(List<Block> blockSeq) {
//Contract.Requires(blockSeq != null);
- Contract.Ensures(Contract.Result<BlockSeq>() != null);
- return base.VisitBlockSeq(new BlockSeq(blockSeq));
+ Contract.Ensures(Contract.Result<List<Block>>() != null);
+ return base.VisitBlockSeq(new List<Block>(blockSeq));
}
public override List<Block/*!*/>/*!*/ VisitBlockList(List<Block/*!*/>/*!*/ blocks) {
//Contract.Requires(cce.NonNullElements(blocks));
diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs
index c8941bbf..63084d99 100644
--- a/Source/Core/InterProceduralReachabilityGraph.cs
+++ b/Source/Core/InterProceduralReachabilityGraph.cs
@@ -82,7 +82,7 @@ namespace Microsoft.Boogie
(newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]);
(newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]);
}
- gotoCmd.labelTargets = new BlockSeq { newProcedureEntryNodes[proc] };
+ gotoCmd.labelTargets = new List<Block> { newProcedureEntryNodes[proc] };
gotoCmd.labelNames = new List<String> { newProcedureEntryNodes[proc].Label };
}
}
@@ -97,7 +97,7 @@ namespace Microsoft.Boogie
var gotoCmd = n.TransferCmd as GotoCmd;
if (gotoCmd != null)
{
- BlockSeq newTargets = new BlockSeq();
+ List<Block> newTargets = new List<Block>();
foreach (Block t in gotoCmd.labelTargets)
{
if (originalToNew.ContainsKey(t))
@@ -122,7 +122,7 @@ namespace Microsoft.Boogie
{
if (!newProcedureEntryNodes.ContainsKey(proc.Name))
{
- Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));
+ Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List<Cmd>(), new GotoCmd(Token.NoToken, new List<Block>()));
nodes.Add(newBlock);
newProcedureEntryNodes[proc.Name] = newBlock;
newProcedureExitNodes[proc.Name] = newBlock;
@@ -137,7 +137,7 @@ namespace Microsoft.Boogie
foreach (var impl in prog.TopLevelDeclarations.OfType<Implementation>())
{
string exitLabel = "__" + impl.Name + "_newExit";
- Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));
+ Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new List<Block>()));
nodes.Add(newExit);
newProcedureExitNodes[impl.Name] = newExit;
foreach (Block b in impl.Blocks)
@@ -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 List<String> { label }, new BlockSeq { newBlock });
+ prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { label }, new List<Block> { 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 List<String> { exitLabel }, new BlockSeq { newExit });
+ prev.TransferCmd = new GotoCmd(Token.NoToken, new List<String> { exitLabel }, new List<Block> { newExit });
}
else
{
diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs
index a67f23f7..df1be84c 100644
--- a/Source/Core/LoopUnroll.cs
+++ b/Source/Core/LoopUnroll.cs
@@ -248,7 +248,7 @@ namespace Microsoft.Boogie {
} else {
body = node.Body;
- BlockSeq newSuccs = new BlockSeq();
+ List<Block> newSuccs = new List<Block>();
foreach (GraphNode succ in node.ForwardEdges) {
Block s;
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs
index eaecf887..4815c781 100644
--- a/Source/Core/OwickiGries.cs
+++ b/Source/Core/OwickiGries.cs
@@ -372,7 +372,7 @@ namespace Microsoft.Boogie
Substitution subst = Substituter.SubstitutionFromHashtable(map);
List<Block> yieldCheckerBlocks = new List<Block>();
List<String> labels = new List<String>();
- BlockSeq labelTargets = new BlockSeq();
+ List<Block> labelTargets = new List<Block>();
Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
labels.Add(yieldCheckerBlock.Label);
labelTargets.Add(yieldCheckerBlock);
@@ -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 List<String> { 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 List<Block> { impl.Blocks[0] }));
impl.Blocks.Insert(0, initBlock);
}
}
@@ -739,7 +739,7 @@ namespace Microsoft.Boogie
TransferCmd transferCmd = new ReturnCmd(Token.NoToken);
if (yieldCheckerProcs.Count > 0)
{
- BlockSeq blockTargets = new BlockSeq();
+ List<Block> blockTargets = new List<Block>();
List<String> labelTargets = new List<String>();
int labelCount = 0;
foreach (Procedure proc in yieldCheckerProcs)
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs
index 987eadb8..cf33e23e 100644
--- a/Source/Core/StandardVisitor.cs
+++ b/Source/Core/StandardVisitor.cs
@@ -136,9 +136,9 @@ namespace Microsoft.Boogie {
node.Blocks = this.VisitBlockList(node.Blocks);
return node;
}
- public virtual BlockSeq VisitBlockSeq(BlockSeq blockSeq) {
+ public virtual List<Block> VisitBlockSeq(List<Block> blockSeq) {
Contract.Requires(blockSeq != null);
- Contract.Ensures(Contract.Result<BlockSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Block>>() != null);
for (int i = 0, n = blockSeq.Count; i < n; i++)
blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));
return blockSeq;
diff --git a/Source/Core/Xml.cs b/Source/Core/Xml.cs
index b4783d28..dcc19b34 100644
--- a/Source/Core/Xml.cs
+++ b/Source/Core/Xml.cs
@@ -103,7 +103,7 @@ namespace Microsoft.Boogie {
cce.EndExpose();
}
- public void WriteError(string message, IToken errorToken, IToken relatedToken, BlockSeq trace) {
+ public void WriteError(string message, IToken errorToken, IToken relatedToken, List<Block> trace) {
Contract.Requires(errorToken != null);
Contract.Requires(message != null);
Contract.Requires(IsOpen && (trace == null || cce.Owner.Different(this, trace)));
@@ -143,7 +143,7 @@ namespace Microsoft.Boogie {
}
#if CCI
- public void WriteError(string message, Cci.Node offendingNode, BlockSeq trace) {
+ public void WriteError(string message, Cci.Node offendingNode, List<Block> trace) {
Contract.Requires(offendingNode != null);
Contract.Requires(message != null);
Contract.Requires(IsOpen && cce.Owner.Different(this, offendingNode));
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-22 20:58:23 +0000