diff options
| -rw-r--r-- | Source/Core/Absy.cs | 27 | ||||
| -rw-r--r-- | Source/Core/AbsyCmd.cs | 12 | ||||
| -rw-r--r-- | Source/Core/Duplicator.cs | 8 | ||||
| -rw-r--r-- | Source/Core/InterProceduralReachabilityGraph.cs | 12 | ||||
| -rw-r--r-- | Source/Core/LoopUnroll.cs | 2 | ||||
| -rw-r--r-- | Source/Core/OwickiGries.cs | 6 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 4 | ||||
| -rw-r--r-- | Source/Core/Xml.cs | 4 | ||||
| -rw-r--r-- | Source/Doomed/DoomedLoopUnrolling.cs | 4 | ||||
| -rw-r--r-- | Source/Doomed/HasseDiagram.cs | 8 | ||||
| -rw-r--r-- | Source/Doomed/VCDoomed.cs | 4 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 2 | ||||
| -rw-r--r-- | Source/Predication/BlockPredicator.cs | 10 | ||||
| -rw-r--r-- | Source/Predication/SmartBlockPredicator.cs | 10 | ||||
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 26 | ||||
| -rw-r--r-- | Source/VCGeneration/FixedpointVC.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 4 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 42 |
19 files changed, 91 insertions, 102 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));
diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs index 2b83da37..38fa99ac 100644 --- a/Source/Doomed/DoomedLoopUnrolling.cs +++ b/Source/Doomed/DoomedLoopUnrolling.cs @@ -338,11 +338,11 @@ namespace VC Block b = kvp.Key;
if (UncheckableNodes.Contains(GraphMap[b])) uncheckables.Add(b);
blocks.Add(b);
- b.Predecessors = new BlockSeq();
+ b.Predecessors = new List<Block>();
foreach (GraphNode p in kvp.Value.Pre) b.Predecessors.Add(p.Label);
if (kvp.Value.Suc.Count > 0)
{
- BlockSeq bs = new BlockSeq();
+ List<Block> bs = new List<Block>();
foreach (GraphNode s in kvp.Value.Suc) bs.Add(s.Label);
b.TransferCmd = new GotoCmd(b.tok, bs);
}
diff --git a/Source/Doomed/HasseDiagram.cs b/Source/Doomed/HasseDiagram.cs index b2ece2df..ad3d487e 100644 --- a/Source/Doomed/HasseDiagram.cs +++ b/Source/Doomed/HasseDiagram.cs @@ -335,7 +335,7 @@ namespace VC {
current = todo[0];
todo.Remove(current);
- BlockSeq pre = m_Predecessors(current, forward);
+ List<Block> pre = m_Predecessors(current, forward);
bool ready = true;
if (pre != null)
{
@@ -356,7 +356,7 @@ namespace VC done.Add(current);
unavoidableBlocks[current].Add(current);
- BlockSeq suc = m_Succecessors(current, forward);
+ List<Block> suc = m_Succecessors(current, forward);
if (suc == null) continue;
foreach (Block bsuc in suc)
{
@@ -402,7 +402,7 @@ namespace VC return ret;
}
- private BlockSeq m_Predecessors(Block b, bool forward)
+ private List<Block> m_Predecessors(Block b, bool forward)
{
if (forward) return b.Predecessors;
GotoCmd gc = b.TransferCmd as GotoCmd;
@@ -413,7 +413,7 @@ namespace VC return null;
}
- private BlockSeq m_Succecessors(Block b, bool forward)
+ private List<Block> m_Succecessors(Block b, bool forward)
{
return m_Predecessors(b, !forward);
}
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index ca282b0a..9f1d8290 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -791,7 +791,7 @@ namespace VC { // update the successors and predecessors
foreach (Block b in lb)
{
- BlockSeq newpreds = new BlockSeq();
+ List<Block> newpreds = new List<Block>();
foreach (Block b_ in b.Predecessors)
{
newpreds.Add(clonemap[b_]);
@@ -802,7 +802,7 @@ namespace VC { if (gc != null)
{
List<String> lseq = new List<String>();
- BlockSeq bseq = new BlockSeq();
+ List<Block> bseq = new List<Block>();
foreach (string s in gc.labelNames) lseq.Add(s);
foreach (Block b_ in gc.labelTargets) bseq.Add(clonemap[b_]);
GotoCmd tcmd = new GotoCmd(gc.tok, lseq, bseq);
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index e988c638..f81150b1 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1499,7 +1499,7 @@ namespace Microsoft.Boogie }
- private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, BlockSeq trace)
+ private static void WriteErrorInformationToXmlSink(ErrorInformation errorInfo, List<Block> trace)
{
var msg = "assertion violation";
switch (errorInfo.Kind)
diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index 771d403b..2174c150 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -51,9 +51,9 @@ public class BlockPredicator { contBlock.Label = block.Label + ".call.cont";
block.TransferCmd =
- new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
+ new GotoCmd(Token.NoToken, new List<Block> { trueBlock, falseBlock });
trueBlock.TransferCmd = falseBlock.TransferCmd =
- new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
+ new GotoCmd(Token.NoToken, new List<Block> { contBlock });
nextBlock = contBlock;
} else {
PredicateCmd(block.Cmds, cmd);
@@ -217,7 +217,7 @@ public class BlockPredicator { Expr.Eq(cur, blockIds[n.Item1]),
new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };
backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(n.Item1));
+ new List<Block> { n.Item1 });
var tailBlock = new Block();
newBlocks.Add(tailBlock);
@@ -227,7 +227,7 @@ public class BlockPredicator { Expr.Neq(cur, blockIds[n.Item1])) };
prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(backedgeBlock, tailBlock));
+ new List<Block> { backedgeBlock, tailBlock });
prevBlock = tailBlock;
} else {
var runBlock = n.Item1;
@@ -235,7 +235,7 @@ public class BlockPredicator { runBlock.Cmds = new List<Cmd>();
newBlocks.Add(runBlock);
prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(runBlock));
+ new List<Block> { runBlock });
pExpr = Expr.Eq(cur, blockIds[runBlock]);
if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 94b47f5e..8e1b960b 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -62,9 +62,9 @@ public class SmartBlockPredicator { contBlock.Label = block.Label + ".call.cont";
block.TransferCmd =
- new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
+ new GotoCmd(Token.NoToken, new List<Block> { trueBlock, falseBlock });
trueBlock.TransferCmd = falseBlock.TransferCmd =
- new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
+ new GotoCmd(Token.NoToken, new List<Block> { contBlock });
nextBlock = contBlock;
} else {
PredicateCmd(p, block.Cmds, cmd);
@@ -389,7 +389,7 @@ public class SmartBlockPredicator { backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken, pExpr,
new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };
backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(n.Item1));
+ new List<Block> { n.Item1 });
var tailBlock = new Block();
newBlocks.Add(tailBlock);
@@ -405,7 +405,7 @@ public class SmartBlockPredicator { if (prevBlock != null)
prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
- new BlockSeq(backedgeBlock, tailBlock));
+ new List<Block> { backedgeBlock, tailBlock });
prevBlock = tailBlock;
} else {
PredicateBlock(pExpr, n.Item1, newBlocks, ref prevBlock);
@@ -430,7 +430,7 @@ public class SmartBlockPredicator { block.Cmds = new List<Cmd>();
newBlocks.Add(block);
if (prevBlock != null) {
- prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));
+ prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new List<Block> { block });
}
if (parentMap.ContainsKey(block)) {
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 11efecdc..c6cf5221 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -626,9 +626,9 @@ namespace Microsoft.Boogie.VCExprAST { Push(e);
return codeExpr;
}
- public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) {
+ public override List<Block> VisitBlockSeq(List<Block> blockSeq) {
//Contract.Requires(blockSeq != null);
- Contract.Ensures(Contract.Result<BlockSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Block>>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
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 };
}
}
|