diff options
25 files changed, 190 insertions, 201 deletions
diff --git a/Source/AbsInt/NativeLattice.cs b/Source/AbsInt/NativeLattice.cs index 4fccc14b..8bb44385 100644 --- a/Source/AbsInt/NativeLattice.cs +++ b/Source/AbsInt/NativeLattice.cs @@ -242,7 +242,7 @@ namespace Microsoft.Boogie.AbstractInterpretation foreach (var b in impl.Blocks) {
var element = pre[b.aiId];
if (element != null && (b.widenBlock || CommandLineOptions.Clo.InstrumentInfer == CommandLineOptions.InstrumentationPlaces.Everywhere)) {
- CmdSeq newCommands = new CmdSeq();
+ List<Cmd> newCommands = new List<Cmd>();
Expr inv = element.ToExpr();
PredicateCmd cmd;
var kv = new QKeyValue(Token.NoToken, "inferred", new List<object>(), null);
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 8654af37..8d68102a 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -604,19 +604,19 @@ namespace Microsoft.Boogie { }
}
- CmdSeq cmdSeq;
+ List<Cmd> cmdSeq;
if (headRecursion)
- cmdSeq = new CmdSeq();
+ cmdSeq = new List<Cmd>();
else
{
CallCmd callCmd = (CallCmd)(loopHeaderToCallCmd2[header]).Clone();
addUniqueCallAttr(si_unique_loc, callCmd);
si_unique_loc++;
- cmdSeq = new CmdSeq(callCmd);
+ cmdSeq = new List<Cmd> { callCmd };
}
Block/*!*/ block1 = new Block(Token.NoToken, source.Label + "_dummy",
- new CmdSeq(new AssumeCmd(Token.NoToken, Expr.False)), new ReturnCmd(Token.NoToken));
+ new List<Cmd>{ new AssumeCmd(Token.NoToken, Expr.False) }, new ReturnCmd(Token.NoToken));
Block/*!*/ block2 = new Block(Token.NoToken, block1.Label,
cmdSeq, new ReturnCmd(Token.NoToken));
impl.Blocks.Add(block1);
@@ -639,7 +639,7 @@ namespace Microsoft.Boogie { blockMap[block1] = block2;
}
List<Block/*!*/>/*!*/ blocks = new List<Block/*!*/>();
- Block exit = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ 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 BlockSeq(blockMap[header], exit));
@@ -650,7 +650,7 @@ namespace Microsoft.Boogie { new BlockSeq(blockMap[header]));
Block entry;
- CmdSeq initCmds = new CmdSeq();
+ List<Cmd> initCmds = new List<Cmd>();
if (loopHeaderToAssignCmd.ContainsKey(header)) {
AssignCmd assignCmd = loopHeaderToAssignCmd[header];
initCmds.Add(assignCmd);
@@ -700,7 +700,7 @@ namespace Microsoft.Boogie { string lastIterBlockName = header.Label + "_last";
Block lastIterBlock = new Block(Token.NoToken, lastIterBlockName, header.Cmds, header.TransferCmd);
newBlocksCreated[header] = lastIterBlock;
- header.Cmds = new CmdSeq(loopHeaderToCallCmd1[header]);
+ header.Cmds = new List<Cmd> { loopHeaderToCallCmd1[header] };
header.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(lastIterBlockName), new BlockSeq(lastIterBlock));
impl.Blocks.Add(lastIterBlock);
blockMap[origHeader] = blockMap[header];
@@ -821,7 +821,7 @@ namespace Microsoft.Boogie { gotoCmd.labelTargets.Remove(splitCandidate);
CodeCopier codeCopier = new CodeCopier(new Hashtable(), new Hashtable());
- CmdSeq newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds);
+ List<Cmd> newCmdSeq = codeCopier.CopyCmdSeq(splitCandidate.Cmds);
TransferCmd newTransferCmd;
GotoCmd splitGotoCmd = splitCandidate.TransferCmd as GotoCmd;
if (splitGotoCmd == null) {
@@ -3234,17 +3234,6 @@ namespace Microsoft.Boogie { }
}
- public sealed class CmdSeq : List<Cmd> {
- public CmdSeq(params Cmd[]/*!*/ args)
- : base(args) {
- Contract.Requires(args != null);
- }
- public CmdSeq(CmdSeq/*!*/ cmdSeq)
- : base(cmdSeq) {
- Contract.Requires(cmdSeq != null);
- }
- }
-
public sealed class ExprSeq : List<Expr> {
public ExprSeq(params Expr[]/*!*/ args)
: base(args) {
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index ace4e7b6..a11d53a2 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -34,13 +34,13 @@ namespace Microsoft.Boogie { public readonly bool Anonymous;
[Rep]
- public CmdSeq/*!*/ simpleCmds;
+ public List<Cmd>/*!*/ simpleCmds;
public StructuredCmd ec;
public TransferCmd tc;
public BigBlock successorBigBlock; // null if successor is end of procedure body (or if field has not yet been initialized)
- public BigBlock(IToken tok, string labelName, [Captured] CmdSeq simpleCmds, StructuredCmd ec, TransferCmd tc) {
+ public BigBlock(IToken tok, string labelName, [Captured] List<Cmd> simpleCmds, StructuredCmd ec, TransferCmd tc) {
Contract.Requires(simpleCmds != null);
Contract.Requires(tok != null);
Contract.Requires(ec == null || tc == null);
@@ -75,7 +75,7 @@ namespace Microsoft.Boogie { public class StmtList {
[Rep]
public readonly List<BigBlock/*!*/>/*!*/ BigBlocks;
- public CmdSeq PrefixCommands;
+ public List<Cmd> PrefixCommands;
public readonly IToken/*!*/ EndCurly;
public StmtList ParentContext;
public BigBlock ParentBigBlock;
@@ -122,7 +122,7 @@ namespace Microsoft.Boogie { /// Note, to be conservative (that is, ignoring the possible optimization that this
/// method enables), this method can do nothing and return false.
/// </summary>
- public bool PrefixFirstBlock([Captured] CmdSeq prefixCmds, ref string suggestedLabel) {
+ public bool PrefixFirstBlock([Captured] List<Cmd> prefixCmds, ref string suggestedLabel) {
Contract.Requires(suggestedLabel != null);
Contract.Requires(prefixCmds != null);
Contract.Ensures(Contract.Result<bool>() || cce.Owner.None(prefixCmds)); // "prefixCmds" is captured only on success
@@ -162,7 +162,7 @@ namespace Microsoft.Boogie { public class StmtListBuilder {
List<BigBlock/*!*/>/*!*/ bigBlocks = new List<BigBlock/*!*/>();
string label;
- CmdSeq simpleCmds;
+ List<Cmd> simpleCmds;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(bigBlocks));
@@ -175,7 +175,7 @@ namespace Microsoft.Boogie { // nothing to do
} else {
if (simpleCmds == null) {
- simpleCmds = new CmdSeq();
+ simpleCmds = new List<Cmd>();
}
bigBlocks.Add(new BigBlock(Token.NoToken, label, simpleCmds, scmd, tcmd));
label = null;
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<StmtList>() != null);
Dump(null, null);
if (bigBlocks.Count == 0) {
- simpleCmds = new CmdSeq(); // the StmtList constructor doesn't like an empty list of BigBlock's
+ simpleCmds = new List<Cmd>(); // the StmtList constructor doesn't like an empty list of BigBlock's
Dump(null, null);
}
return new StmtList(bigBlocks, endCurlyBrace);
@@ -201,7 +201,7 @@ namespace Microsoft.Boogie { public void Add(Cmd cmd) {
Contract.Requires(cmd != null);
if (simpleCmds == null) {
- simpleCmds = new CmdSeq();
+ simpleCmds = new List<Cmd>();
}
simpleCmds.Add(cmd);
}
@@ -453,17 +453,17 @@ namespace Microsoft.Boogie { void CreateBlocks(StmtList stmtList, string runOffTheEndLabel) {
Contract.Requires(stmtList != null);
Contract.Requires(blocks != null);
- CmdSeq cmdPrefixToApply = stmtList.PrefixCommands;
+ List<Cmd> cmdPrefixToApply = stmtList.PrefixCommands;
int n = stmtList.BigBlocks.Count;
foreach (BigBlock b in stmtList.BigBlocks) {
n--;
Contract.Assert(b.LabelName != null);
- CmdSeq theSimpleCmds;
+ List<Cmd> theSimpleCmds;
if (cmdPrefixToApply == null) {
theSimpleCmds = b.simpleCmds;
} else {
- theSimpleCmds = new CmdSeq();
+ theSimpleCmds = new List<Cmd>();
theSimpleCmds.AddRange(cmdPrefixToApply);
theSimpleCmds.AddRange(b.simpleCmds);
cmdPrefixToApply = null; // now, we've used 'em up
@@ -499,8 +499,8 @@ namespace Microsoft.Boogie { string loopDoneLabel = prefix + anon + "_LoopDone";
anon++;
- CmdSeq ssBody = new CmdSeq();
- CmdSeq ssDone = new CmdSeq();
+ List<Cmd> ssBody = new List<Cmd>();
+ List<Cmd> ssDone = new List<Cmd>();
if (wcmd.Guard != null) {
var ac = new AssumeCmd(wcmd.tok, wcmd.Guard);
ac.Attributes = new QKeyValue(wcmd.tok, "partition", new List<object>(), null);
@@ -519,7 +519,7 @@ namespace Microsoft.Boogie { blocks.Add(block);
// LoopHead: assert/assume loop_invariant; goto LoopDone, LoopBody;
- CmdSeq ssHead = new CmdSeq();
+ List<Cmd> ssHead = new List<Cmd>();
foreach (PredicateCmd inv in wcmd.Invariants) {
ssHead.Add(inv);
}
@@ -549,7 +549,7 @@ namespace Microsoft.Boogie { } else {
IfCmd ifcmd = (IfCmd)b.ec;
string predLabel = b.LabelName;
- CmdSeq predCmds = theSimpleCmds;
+ List<Cmd> predCmds = theSimpleCmds;
for (; ifcmd != null; ifcmd = ifcmd.elseIf) {
string thenLabel = prefix + anon + "_Then";
@@ -558,8 +558,8 @@ namespace Microsoft.Boogie { Contract.Assert(elseLabel != null);
anon++;
- CmdSeq ssThen = new CmdSeq();
- CmdSeq ssElse = new CmdSeq();
+ List<Cmd> ssThen = new List<Cmd>();
+ List<Cmd> ssElse = new List<Cmd>();
if (ifcmd.Guard != null) {
var ac = new AssumeCmd(ifcmd.tok, ifcmd.Guard);
ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
@@ -605,7 +605,7 @@ namespace Microsoft.Boogie { } else if (ifcmd.elseIf != null) {
// this is an "else if"
predLabel = elseLabel;
- predCmds = new CmdSeq();
+ predCmds = new List<Cmd>();
if (ifcmd.Guard != null) {
var ac = new AssumeCmd(ifcmd.tok, Expr.Not(ifcmd.Guard));
ac.Attributes = new QKeyValue(ifcmd.tok, "partition", new List<object>(), null);
@@ -796,7 +796,7 @@ namespace Microsoft.Boogie { public string/*!*/ Label; // Note, Label is mostly readonly, but it can change to the name of a nearby block during block coalescing and empty-block removal
[Rep]
[ElementsPeer]
- public CmdSeq/*!*/ Cmds;
+ public List<Cmd>/*!*/ Cmds;
[Rep] //PM: needed to verify Traverse.Visit
public TransferCmd TransferCmd; // maybe null only because we allow deferred initialization (necessary for cyclic structures)
@@ -837,11 +837,11 @@ namespace Microsoft.Boogie { }
public Block()
- : this(Token.NoToken, "", new CmdSeq(), new ReturnCmd(Token.NoToken)) {
+ : this(Token.NoToken, "", new List<Cmd>(), new ReturnCmd(Token.NoToken)) {
}
- public Block(IToken tok, string/*!*/ label, CmdSeq/*!*/ cmds, TransferCmd transferCmd)
+ public Block(IToken tok, string/*!*/ label, List<Cmd>/*!*/ cmds, TransferCmd transferCmd)
: base(tok) {
Contract.Requires(label != null);
Contract.Requires(cmds != null);
@@ -1536,9 +1536,9 @@ namespace Microsoft.Boogie { }
public /*readonly, except for the StandardVisitor*/ List<Variable>/*!*/ Locals;
- public /*readonly, except for the StandardVisitor*/ CmdSeq/*!*/ Cmds;
+ public /*readonly, except for the StandardVisitor*/ List<Cmd>/*!*/ Cmds;
- public StateCmd(IToken tok, List<Variable>/*!*/ locals, CmdSeq/*!*/ cmds)
+ public StateCmd(IToken tok, List<Variable>/*!*/ locals, List<Cmd>/*!*/ cmds)
: base(tok) {
Contract.Requires(locals != null);
Contract.Requires(cmds != null);
@@ -2033,7 +2033,7 @@ namespace Microsoft.Boogie { protected override Cmd ComputeDesugaring() {
Contract.Ensures(Contract.Result<Cmd>() != null);
- CmdSeq newBlockBody = new CmdSeq();
+ List<Cmd> newBlockBody = new List<Cmd>();
Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
Dictionary<Variable, Expr> substMapOld = new Dictionary<Variable, Expr>();
Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>();
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 4b20e4a7..a8a03567 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -84,7 +84,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) Pgm = new Program();
dummyExpr = new LiteralExpr(Token.NoToken, false);
dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
- dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));
dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
dummyExprSeq = new ExprSeq ();
dummyTransferCmd = new ReturnCmd(Token.NoToken);
@@ -681,7 +681,7 @@ StmtList<out StmtList/*!*/ stmtList> = (. Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();
/* built-up state for the current BigBlock: */
IToken startToken = null; string currentLabel = null;
- CmdSeq cs = null; /* invariant: startToken != null ==> cs != null */
+ List<Cmd> cs = null; /* invariant: startToken != null ==> cs != null */
/* temporary variables: */
IToken label; Cmd c; BigBlock b;
StructuredCmd ec = null; StructuredCmd/*!*/ ecn;
@@ -693,7 +693,7 @@ StmtList<out StmtList/*!*/ stmtList> (. if (c != null) {
// LabelOrCmd read a Cmd
Contract.Assert(label == null);
- if (startToken == null) { startToken = c.tok; cs = new CmdSeq(); }
+ if (startToken == null) { startToken = c.tok; cs = new List<Cmd>(); }
Contract.Assert(cs != null);
cs.Add(c);
} else {
@@ -708,13 +708,13 @@ StmtList<out StmtList/*!*/ stmtList> }
startToken = label;
currentLabel = label.val;
- cs = new CmdSeq();
+ cs = new List<Cmd>();
}
.)
| StructuredCmd<out ecn>
(. ec = ecn;
- if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); }
+ if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); }
Contract.Assert(cs != null);
b = new BigBlock(startToken, currentLabel, cs, ec, null);
bigblocks.Add(b);
@@ -723,7 +723,7 @@ StmtList<out StmtList/*!*/ stmtList> | TransferCmd<out tcn>
(. tc = tcn;
- if (startToken == null) { startToken = tc.tok; cs = new CmdSeq(); }
+ if (startToken == null) { startToken = tc.tok; cs = new List<Cmd>(); }
Contract.Assert(cs != null);
b = new BigBlock(startToken, currentLabel, cs, null, tc);
bigblocks.Add(b);
@@ -735,7 +735,7 @@ StmtList<out StmtList/*!*/ stmtList> "}"
(. IToken/*!*/ endCurly = t;
if (startToken == null && bigblocks.Count == 0) {
- startToken = t; cs = new CmdSeq();
+ startToken = t; cs = new List<Cmd>();
}
if (startToken != null) {
Contract.Assert(cs != null);
@@ -1314,7 +1314,7 @@ CodeExpression<.out List<Variable>/*!*/ locals, out List<Block/*!*/>/*!*/ blocks SpecBlock<out Block/*!*/ b>
= (. Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;
Cmd c; IToken label;
- CmdSeq cs = new CmdSeq();
+ List<Cmd> cs = new List<Cmd>();
List<IToken>/*!*/ xs;
StringSeq ss = new StringSeq();
b = dummyBlock;
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 62dfa03f..356ff272 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -388,7 +388,7 @@ namespace Microsoft.Boogie { }
}
- CmdSeq cmds = block.Cmds;
+ List<Cmd> cmds = block.Cmds;
int len = cmds.Count;
for (int i = len - 1; i >= 0; i--) {
if (cmds[i] is CallCmd) {
@@ -469,7 +469,7 @@ namespace Microsoft.Boogie { Propagate(sugCmd.Desugaring, liveSet);
} else if (cmd is StateCmd) {
StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd);
- CmdSeq/*!*/ cmds = cce.NonNull(stCmd.Cmds);
+ List<Cmd>/*!*/ cmds = cce.NonNull(stCmd.Cmds);
int len = cmds.Count;
for (int i = len - 1; i >= 0; i--) {
Propagate(cmds[i], liveSet);
@@ -1461,7 +1461,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; } else if (cmd is StateCmd) {
StateCmd/*!*/ stCmd = (StateCmd)cmd;
Contract.Assert(stCmd != null);
- CmdSeq/*!*/ cmds = stCmd.Cmds;
+ List<Cmd>/*!*/ cmds = stCmd.Cmds;
Contract.Assert(cmds != null);
int len = cmds.Count;
ret = GenKillWeight.one();
diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index 019711e7..e59dd27e 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -118,9 +118,9 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<Choice>() != null);
return base.VisitChoice((Choice)node.Clone());
}
- public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
//Contract.Requires(cmdSeq != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
return base.VisitCmdSeq(cmdSeq);
}
public override Constant VisitConstant(Constant node) {
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 07c44bac..0d412fbc 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -220,8 +220,8 @@ namespace Microsoft.Boogie { foreach (Block block in blocks) {
TransferCmd/*!*/ transferCmd = cce.NonNull(block.TransferCmd);
- CmdSeq cmds = block.Cmds;
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> cmds = block.Cmds;
+ List<Cmd> newCmds = new List<Cmd>();
Block newBlock;
string label = block.Label;
int lblCount = 0;
@@ -296,7 +296,7 @@ namespace Microsoft.Boogie { newBlocks.AddRange(inlinedBlocks);
lblCount = nextlblCount;
- newCmds = new CmdSeq();
+ newCmds = new List<Cmd>();
} else if (inline == 0) {
inlinedSomething = true;
if (CommandLineOptions.Clo.ProcedureInlining == CommandLineOptions.Inlining.Assert) {
@@ -413,8 +413,8 @@ namespace Microsoft.Boogie { }
}
- private CmdSeq RemoveAsserts(CmdSeq cmds) {
- CmdSeq newCmdSeq = new CmdSeq();
+ private List<Cmd> RemoveAsserts(List<Cmd> cmds) {
+ List<Cmd> newCmdSeq = new List<Cmd>();
for (int i = 0; i < cmds.Count; i++) {
Cmd cmd = cmds[i];
if (cmd is AssertCmd) continue;
@@ -442,7 +442,7 @@ namespace Microsoft.Boogie { List<Block/*!*/>/*!*/ inlinedBlocks = new List<Block/*!*/>();
// create in block
- CmdSeq inCmds = new CmdSeq();
+ List<Cmd> inCmds = new List<Cmd>();
// assign in parameters
for (int i = 0; i < impl.InParams.Count; ++i) {
@@ -516,7 +516,7 @@ namespace Microsoft.Boogie { // inject the blocks of the implementation
Block intBlock;
foreach (Block block in implBlocks) {
- CmdSeq copyCmds = codeCopier.CopyCmdSeq(block.Cmds);
+ List<Cmd> copyCmds = codeCopier.CopyCmdSeq(block.Cmds);
if (0 <= inlineDepth) {
copyCmds = RemoveAsserts(copyCmds);
}
@@ -526,7 +526,7 @@ namespace Microsoft.Boogie { }
// create out block
- CmdSeq outCmds = new CmdSeq();
+ List<Cmd> outCmds = new List<Cmd>();
// inject ensures
for (int i = 0; i < proc.Ensures.Count; i++) {
@@ -603,10 +603,10 @@ namespace Microsoft.Boogie { public CodeCopier() {
}
- public CmdSeq CopyCmdSeq(CmdSeq cmds) {
+ public List<Cmd> CopyCmdSeq(List<Cmd> cmds) {
Contract.Requires(cmds != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
- CmdSeq newCmds = new CmdSeq();
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
+ List<Cmd> newCmds = new List<Cmd>();
foreach (Cmd/*!*/ cmd in cmds) {
Contract.Assert(cmd != null);
newCmds.Add(CopyCmd(cmd));
diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs index e103c628..eb34065f 100644 --- a/Source/Core/InterProceduralReachabilityGraph.cs +++ b/Source/Core/InterProceduralReachabilityGraph.cs @@ -122,7 +122,7 @@ namespace Microsoft.Boogie {
if (!newProcedureEntryNodes.ContainsKey(proc.Name))
{
- Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq()));
+ Block newBlock = new Block(Token.NoToken, proc + "__dummy_node", new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));
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 CmdSeq(), new GotoCmd(Token.NoToken, new BlockSeq()));
+ Block newExit = new Block(Token.NoToken, exitLabel, new List<Cmd>(), new GotoCmd(Token.NoToken, new BlockSeq()));
nodes.Add(newExit);
newProcedureExitNodes[impl.Name] = newExit;
foreach (Block b in impl.Blocks)
@@ -150,7 +150,7 @@ namespace Microsoft.Boogie Block newBlock;
if (prev == null)
{
- newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new CmdSeq(cmds.ToArray()), null);
+ newBlock = new Block(b.tok, "__" + impl.Name + "_" + b.Label, new List<Cmd>(cmds.ToArray()), null);
nodes.Add(newBlock);
originalToNew[b] = newBlock;
if (impl.Blocks[0] == b)
@@ -161,7 +161,7 @@ namespace Microsoft.Boogie else
{
string label = "__" + impl.Name + "_" + b.Label + "_call_" + i;
- newBlock = new Block(b.tok, label, new CmdSeq(cmds.ToArray()), null);
+ 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 });
@@ -190,7 +190,7 @@ namespace Microsoft.Boogie #endregion
}
- private List<List<Cmd>> PartitionCmds(CmdSeq cmds) {
+ private List<List<Cmd>> PartitionCmds(List<Cmd> cmds) {
List<List<Cmd>> result = new List<List<Cmd>>();
List<Cmd> current = new List<Cmd>();
result.Add(current);
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 957718fa..00caea52 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -365,7 +365,7 @@ namespace Microsoft.Boogie return base.VisitCallCmd(node);
}
- private void AddDisjointnessExpr(CmdSeq newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
+ private void AddDisjointnessExpr(List<Cmd> newCmds, Absy absy, Dictionary<string, Variable> domainNameToInputVar)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
foreach (var domainName in linearDomains.Keys)
@@ -412,7 +412,7 @@ namespace Microsoft.Boogie foreach (Block b in impl.Blocks)
{
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
for (int i = 0; i < b.Cmds.Count; i++)
{
Cmd cmd = b.Cmds[i];
@@ -478,7 +478,7 @@ namespace Microsoft.Boogie {
foreach (Block header in g.Headers)
{
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
AddDisjointnessExpr(newCmds, header, domainNameToInputVar);
newCmds.AddRange(header.Cmds);
header.Cmds = newCmds;
diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs index 249e4249..a67f23f7 100644 --- a/Source/Core/LoopUnroll.cs +++ b/Source/Core/LoopUnroll.cs @@ -70,7 +70,7 @@ namespace Microsoft.Boogie { class GraphNode {
public readonly Block/*!*/ Block;
- public readonly CmdSeq/*!*/ Body;
+ public readonly List<Cmd>/*!*/ Body;
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Block != null);
@@ -94,16 +94,16 @@ namespace Microsoft.Boogie { [Rep]
public readonly List<GraphNode/*!*/>/*!*/ Predecessors = new List<GraphNode/*!*/>();
- GraphNode(Block b, CmdSeq body) {
+ GraphNode(Block b, List<Cmd> body) {
Contract.Requires(body != null);
Contract.Requires(b != null);
this.Block = b;
this.Body = body;
}
- static CmdSeq GetOptimizedBody(CmdSeq cmds) {
+ static List<Cmd> GetOptimizedBody(List<Cmd> cmds) {
Contract.Requires(cmds != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
int n = 0;
foreach (Cmd c in cmds) {
n++;
@@ -114,7 +114,7 @@ namespace Microsoft.Boogie { for (int i = 0; i < n; i++) {
s[i] = cmds[i];
}
- return new CmdSeq(s);
+ return new List<Cmd>(s);
}
}
return cmds;
@@ -140,7 +140,7 @@ namespace Microsoft.Boogie { }
} else {
- CmdSeq body = GetOptimizedBody(b.Cmds);
+ List<Cmd> body = GetOptimizedBody(b.Cmds);
g = new GraphNode(b, body);
gd.Add(b, g);
if (from != null) {
@@ -224,13 +224,13 @@ namespace Microsoft.Boogie { Contract.Assert(nw != null);
} else {
- CmdSeq body;
+ List<Cmd> body;
TransferCmd tcmd;
Contract.Assert(orig.TransferCmd != null);
if (next == null && node.IsCutPoint) {
// as the body, use the assert/assume commands that make up the loop invariant
- body = new CmdSeq();
+ body = new List<Cmd>();
foreach (Cmd/*!*/ c in node.Body) {
Contract.Assert(c != null);
if (c is PredicateCmd || c is CommentCmd) {
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index cbaff3ef..1d0eb0fd 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -180,7 +180,7 @@ namespace Microsoft.Boogie yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1)));
}
- private void AddCallToYieldProc(CmdSeq newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
+ private void AddCallToYieldProc(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar)
{
ExprSeq exprSeq = new ExprSeq();
foreach (string domainName in linearTypechecker.linearDomains.Keys)
@@ -213,7 +213,7 @@ namespace Microsoft.Boogie return domainNameToExpr;
}
- private void AddUpdatesToOldGlobalVars(CmdSeq newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
+ private void AddUpdatesToOldGlobalVars(List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToLocalVar, Dictionary<string, Expr> domainNameToExpr)
{
List<AssignLhs> lhss = new List<AssignLhs>();
List<Expr> rhss = new List<Expr>();
@@ -233,7 +233,7 @@ namespace Microsoft.Boogie }
}
- private void DesugarYield(YieldCmd yieldCmd, CmdSeq cmds, CmdSeq newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
+ private void DesugarYield(YieldCmd yieldCmd, List<Cmd> cmds, List<Cmd> newCmds, Dictionary<Variable, Variable> ogOldGlobalMap, Dictionary<string, Variable> domainNameToInputVar, Dictionary<string, Variable> domainNameToLocalVar)
{
AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
@@ -317,7 +317,7 @@ namespace Microsoft.Boogie return proc;
}
- private void CreateYieldCheckerImpl(DeclWithFormals decl, List<CmdSeq> yields, Dictionary<Variable, Expr> map)
+ private void CreateYieldCheckerImpl(DeclWithFormals decl, List<List<Cmd>> yields, Dictionary<Variable, Expr> map)
{
if (yields.Count == 0) return;
@@ -373,15 +373,15 @@ namespace Microsoft.Boogie List<Block> yieldCheckerBlocks = new List<Block>();
StringSeq labels = new StringSeq();
BlockSeq labelTargets = new BlockSeq();
- Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ Block yieldCheckerBlock = new Block(Token.NoToken, "exit", new List<Cmd>(), new ReturnCmd(Token.NoToken));
labels.Add(yieldCheckerBlock.Label);
labelTargets.Add(yieldCheckerBlock);
yieldCheckerBlocks.Add(yieldCheckerBlock);
int yieldCount = 0;
- foreach (CmdSeq cs in yields)
+ foreach (List<Cmd> cs in yields)
{
var linearDomains = linearTypechecker.linearDomains;
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
foreach (Cmd cmd in cs)
{
PredicateCmd predCmd = (PredicateCmd)cmd;
@@ -402,7 +402,7 @@ namespace Microsoft.Boogie labelTargets.Add(yieldCheckerBlock);
yieldCheckerBlocks.Add(yieldCheckerBlock);
}
- yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), new GotoCmd(Token.NoToken, labels, labelTargets)));
+ yieldCheckerBlocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), new GotoCmd(Token.NoToken, labels, labelTargets)));
// Create the yield checker procedure
var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name);
@@ -452,12 +452,12 @@ namespace Microsoft.Boogie }
// Collect the yield predicates and desugar yields
- List<CmdSeq> yields = new List<CmdSeq>();
- CmdSeq cmds = new CmdSeq();
+ List<List<Cmd>> yields = new List<List<Cmd>>();
+ List<Cmd> cmds = new List<Cmd>();
foreach (Block b in impl.Blocks)
{
YieldCmd yieldCmd = null;
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
for (int i = 0; i < b.Cmds.Count; i++)
{
Cmd cmd = b.Cmds[i];
@@ -475,7 +475,7 @@ namespace Microsoft.Boogie if (cmds.Count > 0)
{
yields.Add(cmds);
- cmds = new CmdSeq();
+ cmds = new List<Cmd>();
}
yieldCmd = null;
}
@@ -538,7 +538,7 @@ namespace Microsoft.Boogie if (cmds.Count > 0)
{
yields.Add(cmds);
- cmds = new CmdSeq();
+ cmds = new List<Cmd>();
}
}
if (b.TransferCmd is ReturnCmd && (!info.isAtomic || info.isEntrypoint || info.isThreadStart))
@@ -565,7 +565,7 @@ namespace Microsoft.Boogie AddCallToYieldProc(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar);
AddUpdatesToOldGlobalVars(pred.Cmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
}
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
foreach (string domainName in linearTypechecker.linearDomains.Keys)
{
newCmds.Add(new AssumeCmd(Token.NoToken, Expr.Binary(BinaryOperator.Opcode.Eq, Expr.Ident(domainNameToLocalVar[domainName]), domainNameToExpr[domainName])));
@@ -611,7 +611,7 @@ namespace Microsoft.Boogie }
if (lhss.Count > 0)
{
- Block initBlock = new Block(Token.NoToken, "og_init", new CmdSeq(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 StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0])));
impl.Blocks.Insert(0, initBlock);
}
}
@@ -637,8 +637,8 @@ namespace Microsoft.Boogie }
// Collect the yield predicates and desugar yields
- List<CmdSeq> yields = new List<CmdSeq>();
- CmdSeq cmds = new CmdSeq();
+ List<List<Cmd>> yields = new List<List<Cmd>>();
+ List<Cmd> cmds = new List<Cmd>();
if (proc.Requires.Count > 0)
{
Dictionary<string, HashSet<Variable>> domainNameToScope = new Dictionary<string, HashSet<Variable>>();
@@ -676,7 +676,7 @@ namespace Microsoft.Boogie }
}
yields.Add(cmds);
- cmds = new CmdSeq();
+ cmds = new List<Cmd>();
}
if (info.inParallelCall && proc.Ensures.Count > 0)
{
@@ -715,7 +715,7 @@ namespace Microsoft.Boogie }
}
yields.Add(cmds);
- cmds = new CmdSeq();
+ cmds = new List<Cmd>();
}
CreateYieldCheckerImpl(proc, yields, new Dictionary<Variable, Expr>());
}
@@ -752,14 +752,14 @@ namespace Microsoft.Boogie CallCmd callCmd = new CallCmd(Token.NoToken, proc.Name, exprSeq, new List<IdentifierExpr>());
callCmd.Proc = proc;
string label = string.Format("L_{0}", labelCount++);
- Block block = new Block(Token.NoToken, label, new CmdSeq(callCmd), new ReturnCmd(Token.NoToken));
+ Block block = new Block(Token.NoToken, label, new List<Cmd> { callCmd }, new ReturnCmd(Token.NoToken));
labelTargets.Add(label);
blockTargets.Add(block);
blocks.Add(block);
}
transferCmd = new GotoCmd(Token.NoToken, labelTargets, blockTargets);
}
- blocks.Insert(0, new Block(Token.NoToken, "enter", new CmdSeq(), transferCmd));
+ blocks.Insert(0, new Block(Token.NoToken, "enter", new List<Cmd>(), transferCmd));
var yieldImpl = new Implementation(Token.NoToken, yieldProc.Name, new TypeVariableSeq(), inputs, new List<Variable>(), new List<Variable>(), blocks);
yieldImpl.Proc = yieldProc;
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index b0ce346a..bcdd01d8 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -104,7 +104,7 @@ public Parser(Scanner/*!*/ scanner, Errors/*!*/ errors, bool disambiguation) Pgm = new Program();
dummyExpr = new LiteralExpr(Token.NoToken, false);
dummyCmd = new AssumeCmd(Token.NoToken, dummyExpr);
- dummyBlock = new Block(Token.NoToken, "dummyBlock", new CmdSeq(), new ReturnCmd(Token.NoToken));
+ dummyBlock = new Block(Token.NoToken, "dummyBlock", new List<Cmd>(), new ReturnCmd(Token.NoToken));
dummyType = new BasicType(Token.NoToken, SimpleType.Bool);
dummyExprSeq = new ExprSeq ();
dummyTransferCmd = new ReturnCmd(Token.NoToken);
@@ -924,7 +924,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); List<BigBlock/*!*/> bigblocks = new List<BigBlock/*!*/>();
/* built-up state for the current BigBlock: */
IToken startToken = null; string currentLabel = null;
- CmdSeq cs = null; /* invariant: startToken != null ==> cs != null */
+ List<Cmd> cs = null; /* invariant: startToken != null ==> cs != null */
/* temporary variables: */
IToken label; Cmd c; BigBlock b;
StructuredCmd ec = null; StructuredCmd/*!*/ ecn;
@@ -936,7 +936,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { if (c != null) {
// LabelOrCmd read a Cmd
Contract.Assert(label == null);
- if (startToken == null) { startToken = c.tok; cs = new CmdSeq(); }
+ if (startToken == null) { startToken = c.tok; cs = new List<Cmd>(); }
Contract.Assert(cs != null);
cs.Add(c);
} else {
@@ -951,13 +951,13 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { }
startToken = label;
currentLabel = label.val;
- cs = new CmdSeq();
+ cs = new List<Cmd>();
}
} else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
StructuredCmd(out ecn);
ec = ecn;
- if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); }
+ if (startToken == null) { startToken = ec.tok; cs = new List<Cmd>(); }
Contract.Assert(cs != null);
b = new BigBlock(startToken, currentLabel, cs, ec, null);
bigblocks.Add(b);
@@ -966,7 +966,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { } else {
TransferCmd(out tcn);
tc = tcn;
- if (startToken == null) { startToken = tc.tok; cs = new CmdSeq(); }
+ if (startToken == null) { startToken = tc.tok; cs = new List<Cmd>(); }
Contract.Assert(cs != null);
b = new BigBlock(startToken, currentLabel, cs, null, tc);
bigblocks.Add(b);
@@ -977,7 +977,7 @@ out List<Variable>/*!*/ ins, out List<Variable>/*!*/ outs, out QKeyValue kv) { Expect(28);
IToken/*!*/ endCurly = t;
if (startToken == null && bigblocks.Count == 0) {
- startToken = t; cs = new CmdSeq();
+ startToken = t; cs = new List<Cmd>();
}
if (startToken != null) {
Contract.Assert(cs != null);
@@ -1924,7 +1924,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { void SpecBlock(out Block/*!*/ b) {
Contract.Ensures(Contract.ValueAtReturn(out b) != null); IToken/*!*/ x; IToken/*!*/ y;
Cmd c; IToken label;
- CmdSeq cs = new CmdSeq();
+ List<Cmd> cs = new List<Cmd>();
List<IToken>/*!*/ xs;
StringSeq ss = new StringSeq();
b = dummyBlock;
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 8f5cf64b..987eadb8 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -168,9 +168,9 @@ namespace Microsoft.Boogie { node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(node.Outs[i]));
return node;
}
- public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ public virtual List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
Contract.Requires(cmdSeq != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
for (int i = 0, n = cmdSeq.Count; i < n; i++)
cmdSeq[i] = (Cmd)this.Visit(cce.NonNull(cmdSeq[i])); // call general Visit so subtypes of Cmd get visited by their particular visitor
return cmdSeq;
diff --git a/Source/Doomed/DoomedLoopUnrolling.cs b/Source/Doomed/DoomedLoopUnrolling.cs index d7ba6025..2b83da37 100644 --- a/Source/Doomed/DoomedLoopUnrolling.cs +++ b/Source/Doomed/DoomedLoopUnrolling.cs @@ -88,7 +88,7 @@ namespace VC private void m_AddHavocCmdToFront(Block b, HavocCmd hcmd)
{
- CmdSeq cs = new CmdSeq();
+ List<Cmd> cs = new List<Cmd>();
cs.Add(hcmd); cs.AddRange(b.Cmds);
b.Cmds = cs;
}
@@ -357,7 +357,7 @@ namespace VC public GraphNode CloneGraphNode(GraphNode gn, string prefix)
{
- CmdSeq cmds = new CmdSeq(gn.Label.Cmds);
+ List<Cmd> cmds = new List<Cmd>(gn.Label.Cmds);
Block b = new Block(gn.Label.tok, prefix+gn.Label.Label, cmds, gn.Label.TransferCmd);
GraphNode clone = new GraphNode(b);
diff --git a/Source/Doomed/VCDoomed.cs b/Source/Doomed/VCDoomed.cs index 341644ca..bc86ca40 100644 --- a/Source/Doomed/VCDoomed.cs +++ b/Source/Doomed/VCDoomed.cs @@ -244,7 +244,7 @@ namespace VC { //}
m_doomedCmds.Clear();
- Dictionary<Block, CmdSeq> cmdbackup = new Dictionary<Block, CmdSeq>();
+ Dictionary<Block, List<Cmd>> cmdbackup = new Dictionary<Block, List<Cmd>>();
BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, 0, impl.Blocks.Count / 2 - 1);
BruteForceCESearch(errh.m_Reachvar, impl, callback, cmdbackup, impl.Blocks.Count / 2, impl.Blocks.Count - 1);
@@ -256,7 +256,7 @@ namespace VC { }
#region Undo all modifications
- foreach (KeyValuePair<Block, CmdSeq> kvp in cmdbackup) {
+ foreach (KeyValuePair<Block, List<Cmd>> kvp in cmdbackup) {
Contract.Assert(kvp.Key != null);
Contract.Assert(kvp.Value != null);
kvp.Key.Cmds = kvp.Value;
@@ -389,7 +389,7 @@ namespace VC { #endregion
bool BruteForceCESearch(Variable reachvar, Implementation impl, VerifierCallback callback,
- Dictionary<Block, CmdSeq> cmdbackup, int startidx, int endidx) {
+ Dictionary<Block, List<Cmd>> cmdbackup, int startidx, int endidx) {
Contract.Requires(reachvar != null);
Contract.Requires(impl != null);
Contract.Requires(callback != null);
@@ -398,7 +398,7 @@ namespace VC { for (int i = startidx; i <= endidx; i++) {
if (_copiedBlock.Contains(impl.Blocks[i]))
continue;
- CmdSeq cs = new CmdSeq();
+ List<Cmd> cs = new List<Cmd>();
cmdbackup.Add(impl.Blocks[i], impl.Blocks[i].Cmds);
foreach (Cmd c in impl.Blocks[i].Cmds) {
Contract.Assert(c != null);
@@ -455,9 +455,9 @@ namespace VC { Contract.Requires(impl != null);
Contract.Requires(callback != null);
#region Modify Cmds
- CmdSeq backup = b.Cmds;
+ List<Cmd> backup = b.Cmds;
Contract.Assert(backup != null);
- CmdSeq cs = new CmdSeq();
+ List<Cmd> cs = new List<Cmd>();
for (int i = 0; i < startidx; i++) {
cs.Add(b.Cmds[i]);
}
@@ -518,12 +518,12 @@ namespace VC { }
}
- void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, CmdSeq/*!*/>/*!*/ cmdbackup,
+ void UndoBlockModifications(Implementation impl, Dictionary<Block/*!*/, List<Cmd>/*!*/>/*!*/ cmdbackup,
int startidx, int endidx) {
Contract.Requires(cce.NonNullElements(cmdbackup));
Contract.Requires(impl != null);
for (int i = startidx; i <= endidx; i++) {
- CmdSeq cs = null;
+ List<Cmd> cs = null;
if (cmdbackup.TryGetValue(impl.Blocks[i], out cs)) {
Contract.Assert(cs != null);
impl.Blocks[i].Cmds = cs;
@@ -592,7 +592,7 @@ namespace VC { #region Insert pre- and post-conditions and where clauses as assume and assert statements
{
- CmdSeq cc = new CmdSeq();
+ List<Cmd> cc = new List<Cmd>();
// where clauses of global variables
foreach (Declaration d in program.TopLevelDeclarations) {
GlobalVariable gvar = d as GlobalVariable;
@@ -637,7 +637,7 @@ namespace VC { /// Add additional variable to allow checking as described in the paper
/// "It's doomed; we can prove it"
/// </summary>
- private CmdSeq GenerateReachabilityPredicates(Implementation impl)
+ private List<Cmd> GenerateReachabilityPredicates(Implementation impl)
{
Contract.Requires(impl != null);
@@ -665,14 +665,14 @@ namespace VC { rhsl.Add(Expr.Literal(1) );
- CmdSeq cs = new CmdSeq(new AssignCmd(Token.NoToken, lhsl, rhsl));
+ List<Cmd> cs = new List<Cmd> { new AssignCmd(Token.NoToken, lhsl, rhsl) };
cs.AddRange(b.Cmds);
b.Cmds = cs;
//checkBlocks.Add(new CheckableBlock(v_,b));
}
- CmdSeq incReachVars = new CmdSeq();
+ List<Cmd> incReachVars = new List<Cmd>();
foreach (KeyValuePair<Block, Variable> kvp in m_BlockReachabilityMap)
{
IdentifierExpr lhs = new IdentifierExpr(Token.NoToken, kvp.Value);
@@ -734,7 +734,7 @@ namespace VC { impl.Blocks = DeepCopyBlocks(impl.Blocks, m_UncheckableBlocks);
m_BlockReachabilityMap = new Dictionary<Block, Variable>();
- CmdSeq cs = GenerateReachabilityPredicates(impl);
+ List<Cmd> cs = GenerateReachabilityPredicates(impl);
//foreach (Block test in getTheFFinalBlock(impl.Blocks[0]))
//{
diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 0f725ccf..0da1c5d9 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -411,7 +411,7 @@ namespace Microsoft.Boogie.Houdini { #region Adapt candidate assertions to take account of stages
foreach (var b in prog.TopLevelDeclarations.OfType<Implementation>().Select(Item => Item.Blocks).SelectMany(Item => Item))
{
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
foreach (var cmd in b.Cmds)
{
var a = cmd as AssertCmd;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index b4408f03..afae3143 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -247,10 +247,10 @@ namespace Microsoft.Boogie.Houdini { }
public class InlineRequiresVisitor : StandardVisitor {
- public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
Contract.Requires(cmdSeq != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
- CmdSeq newCmdSeq = new CmdSeq();
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
+ List<Cmd> newCmdSeq = new List<Cmd>();
for (int i = 0, n = cmdSeq.Count; i < n; i++) {
Cmd cmd = cmdSeq[i];
CallCmd callCmd = cmd as CallCmd;
@@ -263,13 +263,13 @@ namespace Microsoft.Boogie.Houdini { }
return newCmdSeq;
}
- private CmdSeq InlineRequiresForCallCmd(CallCmd node) {
+ private List<Cmd> InlineRequiresForCallCmd(CallCmd node) {
Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
for (int i = 0; i < node.Proc.InParams.Count; i++) {
substMap.Add(node.Proc.InParams[i], node.Ins[i]);
}
Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);
- CmdSeq cmds = new CmdSeq();
+ List<Cmd> cmds = new List<Cmd>();
foreach (Requires requires in node.Proc.Requires) {
if (requires.Free) continue;
Requires requiresCopy = new Requires(false, Substituter.Apply(substitution, requires.Condition));
@@ -1142,7 +1142,7 @@ namespace Microsoft.Boogie.Houdini { // Treat all assertions
// TODO: do we need to also consider assumptions?
foreach (Block block in prog.TopLevelDeclarations.OfType<Implementation>().Select(item => item.Blocks).SelectMany(item => item)) {
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
foreach (Cmd cmd in block.Cmds) {
string c;
AssertCmd assertCmd = cmd as AssertCmd;
diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index c655175a..771d403b 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -61,7 +61,7 @@ public class BlockPredicator { }
}
- void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
+ void PredicateCmd(List<Cmd> cmdSeq, Cmd cmd) {
if (cmd is AssignCmd) {
var aCmd = (AssignCmd)cmd;
cmdSeq.Add(new AssignCmd(Token.NoToken, aCmd.Lhss,
@@ -125,7 +125,7 @@ public class BlockPredicator { }
else if (cmd is StateCmd) {
var sCmd = (StateCmd)cmd;
- var newCmdSeq = new CmdSeq();
+ var newCmdSeq = new List<Cmd>();
foreach (Cmd c in sCmd.Cmds)
PredicateCmd(newCmdSeq, c);
sCmd.Cmds = newCmdSeq;
@@ -136,7 +136,7 @@ public class BlockPredicator { }
}
- void PredicateTransferCmd(CmdSeq cmdSeq, TransferCmd cmd) {
+ void PredicateTransferCmd(List<Cmd> cmdSeq, TransferCmd cmd) {
if (cmd is GotoCmd) {
var gCmd = (GotoCmd)cmd;
var targets = new List<Expr>(
@@ -161,7 +161,7 @@ public class BlockPredicator { aCmd.Expr)));
}
b.Cmds =
- new CmdSeq(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());
+ new List<Cmd>(b.Cmds.Cast<Cmd>().Skip(assumes.Count()).ToArray());
}
}
}
@@ -201,9 +201,9 @@ public class BlockPredicator { Block entryBlock = new Block();
entryBlock.Label = "entry";
- entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
+ entryBlock.Cmds = new List<Cmd> { Cmd.SimpleAssign(Token.NoToken, cur,
CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],
- returnBlockId)));
+ returnBlockId)) };
newBlocks.Add(entryBlock);
var prevBlock = entryBlock;
@@ -213,9 +213,9 @@ public class BlockPredicator { newBlocks.Add(backedgeBlock);
backedgeBlock.Label = n.Item1.Label + ".backedge";
- backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
+ backedgeBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,
Expr.Eq(cur, blockIds[n.Item1]),
- new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
+ new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)) };
backedgeBlock.TransferCmd = new GotoCmd(Token.NoToken,
new BlockSeq(n.Item1));
@@ -223,8 +223,8 @@ public class BlockPredicator { newBlocks.Add(tailBlock);
tailBlock.Label = n.Item1.Label + ".tail";
- tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
- Expr.Neq(cur, blockIds[n.Item1])));
+ tailBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,
+ Expr.Neq(cur, blockIds[n.Item1])) };
prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
new BlockSeq(backedgeBlock, tailBlock));
@@ -232,7 +232,7 @@ public class BlockPredicator { } else {
var runBlock = n.Item1;
var oldCmdSeq = runBlock.Cmds;
- runBlock.Cmds = new CmdSeq();
+ runBlock.Cmds = new List<Cmd>();
newBlocks.Add(runBlock);
prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
new BlockSeq(runBlock));
@@ -267,13 +267,13 @@ public class BlockPredicator { }
}
- private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
+ private void AddUniformCandidateInvariant(List<Cmd> cs, Block header) {
cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,
CreateIfFPThenElse(blockIds[header], returnBlockId)),
"uniform loop"));
}
- private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {
+ private void AddNonUniformCandidateInvariant(List<Cmd> cs, Block header) {
var loopNodes = new HashSet<Block>();
foreach (var b in blockGraph.BackEdgeNodes(header))
loopNodes.UnionWith(blockGraph.NaturalLoops(header, b));
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 28005186..94b47f5e 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -72,7 +72,7 @@ public class SmartBlockPredicator { }
}
- void PredicateCmd(Expr p, CmdSeq cmdSeq, Cmd cmd) {
+ void PredicateCmd(Expr p, List<Cmd> cmdSeq, Cmd cmd) {
if (cmd is CallCmd) {
var cCmd = (CallCmd)cmd;
Debug.Assert(useProcedurePredicates(cCmd.Proc));
@@ -125,7 +125,7 @@ public class SmartBlockPredicator { // skip
} else if (cmd is StateCmd) {
var sCmd = (StateCmd)cmd;
- var newCmdSeq = new CmdSeq();
+ var newCmdSeq = new List<Cmd>();
foreach (Cmd c in sCmd.Cmds)
PredicateCmd(p, newCmdSeq, c);
sCmd.Cmds = newCmdSeq;
@@ -137,7 +137,7 @@ public class SmartBlockPredicator { // hasPredicatedRegion is true iff the block or its targets are predicated
// (i.e. we enter, stay within or exit a predicated region).
- void PredicateTransferCmd(Expr p, Block src, CmdSeq cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
+ void PredicateTransferCmd(Expr p, Block src, List<Cmd> cmdSeq, TransferCmd cmd, out bool hasPredicatedRegion) {
hasPredicatedRegion = predMap.ContainsKey(src);
if (cmd is GotoCmd) {
@@ -347,7 +347,7 @@ public class SmartBlockPredicator { if (parts.Count() > 0) {
pred = parts.Select(a => ((AssumeCmd)a).Expr).Aggregate(Expr.And);
block.Cmds =
- new CmdSeq(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
+ new List<Cmd>(block.Cmds.Cast<Cmd>().Skip(parts.Count()).ToArray());
} else {
continue;
}
@@ -386,8 +386,8 @@ public class SmartBlockPredicator { newBlocks.Add(backedgeBlock);
backedgeBlock.Label = n.Item1.Label + ".backedge";
- backedgeBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken, pExpr,
- new QKeyValue(Token.NoToken, "backedge", new List<object>(), null)));
+ 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));
@@ -395,8 +395,8 @@ public class SmartBlockPredicator { newBlocks.Add(tailBlock);
tailBlock.Label = n.Item1.Label + ".tail";
- tailBlock.Cmds = new CmdSeq(new AssumeCmd(Token.NoToken,
- Expr.Not(pExpr)));
+ tailBlock.Cmds = new List<Cmd> { new AssumeCmd(Token.NoToken,
+ Expr.Not(pExpr)) };
if (uni != null && !uni.IsUniform(impl.Name, n.Item1)) {
uni.AddNonUniform(impl.Name, backedgeBlock);
@@ -427,7 +427,7 @@ public class SmartBlockPredicator { var firstBlock = block;
var oldCmdSeq = block.Cmds;
- block.Cmds = new CmdSeq();
+ block.Cmds = new List<Cmd>();
newBlocks.Add(block);
if (prevBlock != null) {
prevBlock.TransferCmd = new GotoCmd(Token.NoToken, new BlockSeq(block));
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index a6287db5..3c8f4cd9 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -292,7 +292,7 @@ namespace Microsoft.Boogie return null;
}
- private bool Analyse(Implementation impl, CmdSeq cmdSeq, bool ControlFlowIsUniform)
+ private bool Analyse(Implementation impl, List<Cmd> cmdSeq, bool ControlFlowIsUniform)
{
foreach (Cmd c in cmdSeq)
{
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index b3574b94..11efecdc 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -650,9 +650,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false);
throw new cce.UnreachableException();
}
- public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
+ public override List<Cmd> VisitCmdSeq(List<Cmd> cmdSeq) {
//Contract.Requires(cmdSeq != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
Contract.Assert(false);
throw new cce.UnreachableException();
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6137678b..43627c5f 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -690,10 +690,10 @@ namespace VC { return;
}
- private static void AddAsPrefix(Block b, CmdSeq cs) {
+ private static void AddAsPrefix(Block b, List<Cmd> cs) {
Contract.Requires(b != null);
Contract.Requires(cs != null);
- CmdSeq newCommands = new CmdSeq();
+ List<Cmd> newCommands = new List<Cmd>();
newCommands.AddRange(cs);
newCommands.AddRange(b.Cmds);
b.Cmds = newCommands;
@@ -707,7 +707,7 @@ namespace VC { /// </summary>
/// <param name="impl"></param>
/// <param name="startCmds"></param>
- protected static void InjectPreconditions(Implementation impl, [Captured] CmdSeq startCmds) {
+ protected static void InjectPreconditions(Implementation impl, [Captured] List<Cmd> startCmds) {
Contract.Requires(impl != null);
Contract.Requires(startCmds != null);
Contract.Requires(impl.Proc != null);
@@ -802,7 +802,7 @@ namespace VC { // Here goes: First, create the new block, which will become the new insertion
// point and which will serve as a target for the CodeExpr. Steal the TransferCmd
// from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.
- Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);
+ Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new List<Cmd>(), insertionPoint.TransferCmd);
k++;
// Second, append the CodeExpr blocks to the implementation's blocks
ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);
@@ -827,10 +827,10 @@ namespace VC { /// Get the pre-condition of an implementation, including the where clauses from the in-parameters.
/// </summary>
/// <param name="impl"></param>
- protected static CmdSeq GetPre(Implementation impl) {
+ protected static List<Cmd> GetPre(Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
TokenTextWriter debugWriter = null;
@@ -840,7 +840,7 @@ namespace VC { }
Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
- CmdSeq pre = new CmdSeq();
+ List<Cmd> pre = new List<Cmd>();
// (free and checked) requires clauses
foreach (Requires req in impl.Proc.Requires) {
@@ -867,19 +867,19 @@ namespace VC { /// Get the post-condition of an implementation.
/// </summary>
/// <param name="impl"></param>
- protected static CmdSeq GetPost(Implementation impl) {
+ protected static List<Cmd> GetPost(Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
Console.WriteLine("Effective postcondition:");
}
// Construct an Expr for the post-condition
Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
- CmdSeq post = new CmdSeq();
+ List<Cmd> post = new List<Cmd>();
foreach (Ensures ens in impl.Proc.Ensures) {
Contract.Assert(ens != null);
if (!ens.Free) {
@@ -910,10 +910,10 @@ namespace VC { /// As a side effect, this method adds these where clauses to the out parameters.
/// </summary>
/// <param name="impl"></param>
- protected static CmdSeq GetParamWhereClauses(Implementation impl) {
+ protected static List<Cmd> GetParamWhereClauses(Implementation impl) {
Contract.Requires(impl != null);
Contract.Requires(impl.Proc != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
TokenTextWriter debugWriter = null;
if (CommandLineOptions.Clo.PrintWithUniqueASTIds) {
debugWriter = new TokenTextWriter("<console>", Console.Out, false);
@@ -921,7 +921,7 @@ namespace VC { }
Substitution formalProcImplSubst = Substituter.SubstitutionFromHashtable(impl.GetImplFormalMap());
- CmdSeq whereClauses = new CmdSeq();
+ List<Cmd> whereClauses = new List<Cmd>();
// where clauses of in-parameters
foreach (Formal f in impl.Proc.InParams) {
@@ -1104,7 +1104,7 @@ namespace VC { }
if (returnBlocks > 1) {
string unifiedExitLabel = "GeneratedUnifiedExit";
- Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new CmdSeq(), new ReturnCmd(Token.NoToken));
+ Block unifiedExit = new Block(new Token(-17, -4), unifiedExitLabel, new List<Cmd>(), new ReturnCmd(Token.NoToken));
Contract.Assert(unifiedExit != null);
foreach (Block b in impl.Blocks) {
if (b.TransferCmd is ReturnCmd) {
@@ -1289,7 +1289,7 @@ namespace VC { Contract.Requires(oldFrameSubst != null);
#region Walk forward over the commands in this block and convert them to passive commands
- CmdSeq passiveCmds = new CmdSeq();
+ List<Cmd> passiveCmds = new List<Cmd>();
foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction
TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds, mvInfo);
@@ -1413,7 +1413,7 @@ namespace VC { /// Turn a command into a passive command, and it remembers the previous step, to see if it is a havoc or not. In the case, it remembers the incarnation map BEFORE the havoc
/// Meanwhile, record any information needed to later reconstruct a model view.
/// </summary>
- protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, CmdSeq passiveCmds, ModelViewInfo mvInfo) {
+ protected void TurnIntoPassiveCmd(Cmd c, Dictionary<Variable, Expr> incarnationMap, Substitution oldFrameSubst, List<Cmd> passiveCmds, ModelViewInfo mvInfo) {
Contract.Requires(c != null);
Contract.Requires(incarnationMap != null);
Contract.Requires(oldFrameSubst != null);
@@ -1627,7 +1627,7 @@ namespace VC { Block newBlock = new Block(
new Token(-17, -4),
newBlockLabel,
- new CmdSeq(),
+ new List<Cmd>(),
new GotoCmd(Token.NoToken, ls, bs)
);
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 59e2ca9e..5a6ae6d3 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -242,7 +242,7 @@ namespace Microsoft.Boogie Expr invarExpr = new NAryExpr(Token.NoToken, new FunctionCall(function), exprs);
var invarAssertion = new AssertCmd(Token.NoToken, invarExpr);
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
newCmds.Add(invarAssertion);
// make a record in annotationInfo;
@@ -1176,7 +1176,7 @@ namespace Microsoft.Boogie }
}
- CmdSeq cmds = block.Cmds;
+ List<Cmd> cmds = block.Cmds;
int len = cmds.Count;
for (int i = len - 1; i >= 0; i--)
{
@@ -1655,7 +1655,7 @@ namespace Microsoft.Boogie {
- CmdSeq cmds = b.Cmds;
+ List<Cmd> cmds = b.Cmds;
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
for (int i = 0; i < cmds.Count; i++)
{
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index d1a83827..f29a1b80 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -359,7 +359,7 @@ namespace VC { public void InstrumentCallSites(Implementation implementation) {
var callSiteId = 0;
foreach (Block block in implementation.Blocks) {
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
for (int i = 0; i < block.Cmds.Count; i++) {
Cmd cmd = block.Cmds[i];
newCmds.Add(cmd);
@@ -2582,7 +2582,7 @@ namespace VC { Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
while (true) {
- CmdSeq cmds = b.Cmds;
+ List<Cmd> cmds = b.Cmds;
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
for (int i = 0; i < cmds.Count; i++) {
Cmd cmd = cce.NonNull(cmds[i]);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 491c7eae..96cf5486 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -134,7 +134,7 @@ namespace VC { if (copies.TryGetValue(b, out fake_res)) {
return cce.NonNull(fake_res);
}
- Block res = new Block(b.tok, b.Label, new CmdSeq(b.Cmds), null);
+ Block res = new Block(b.tok, b.Label, new List<Cmd>(b.Cmds), null);
copies[b] = res;
if (b.TransferCmd is GotoCmd) {
foreach (Block ch in cce.NonNull((GotoCmd)b.TransferCmd).labelTargets) {
@@ -160,7 +160,7 @@ namespace VC { return cce.NonNull(fake_res);
}
Block res;
- CmdSeq seq = new CmdSeq();
+ List<Cmd> seq = new List<Cmd>();
foreach (Cmd c in b.Cmds) {
Contract.Assert(c != null);
AssertCmd turn = c as AssertCmd;
@@ -252,7 +252,7 @@ namespace VC { return BooleanEval(e, ref val) && !val;
}
- bool CheckUnreachable(Block cur, CmdSeq seq)
+ bool CheckUnreachable(Block cur, List<Cmd> seq)
{
Contract.Requires(cur != null);
Contract.Requires(seq != null);
@@ -369,7 +369,7 @@ namespace VC { return;
visited.Add(cur);
- CmdSeq seq = new CmdSeq();
+ List<Cmd> seq = new List<Cmd>();
foreach (Cmd cmd_ in cur.Cmds) {
Cmd cmd = cmd_;
Contract.Assert(cmd != null);
@@ -902,15 +902,15 @@ namespace VC { return cost;
}
- CmdSeq SliceCmds(Block b) {
+ List<Cmd> SliceCmds(Block b) {
Contract.Requires(b != null);
- Contract.Ensures(Contract.Result<CmdSeq>() != null);
+ Contract.Ensures(Contract.Result<List<Cmd>>() != null);
- CmdSeq seq = b.Cmds;
+ List<Cmd> seq = b.Cmds;
Contract.Assert(seq != null);
if (!doing_slice && !ShouldAssumize(b))
return seq;
- CmdSeq res = new CmdSeq();
+ List<Cmd> res = new List<Cmd>();
foreach (Cmd c in seq) {
Contract.Assert(c != null);
AssertCmd a = c as AssertCmd;
@@ -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 CmdSeq(), new GotoCmd(Token.NoToken, new StringSeq(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 StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))));
ResetPredecessors(impl.Blocks);
#region Convert program CFG into a DAG
@@ -1911,8 +1911,8 @@ namespace VC { foreach (Block b in cce.NonNull( g.BackEdgeNodes(header))) {Contract.Assert(b != null); backEdgeNodes.Add(b, null); }
#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();
+ List<Cmd> prefixOfPredicateCmdsInit = new List<Cmd>();
+ List<Cmd> prefixOfPredicateCmdsMaintained = new List<Cmd>();
for (int i = 0, n = header.Cmds.Count; i < n; i++)
{
PredicateCmd a = header.Cmds[i] as PredicateCmd;
@@ -2056,7 +2056,7 @@ namespace VC { // pass the token of the enclosing loop header to the HavocCmd so we can reconstruct
// the source location for this later on
HavocCmd hc = new HavocCmd(header.tok,havocExprs);
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
newCmds.Add(hc);
foreach ( Cmd c in header.Cmds )
{
@@ -2079,7 +2079,7 @@ namespace VC { public void DesugarCalls(Implementation impl) {
foreach (Block block in impl.Blocks) {
- CmdSeq newCmds = new CmdSeq();
+ List<Cmd> newCmds = new List<Cmd>();
foreach (Cmd cmd in block.Cmds) {
SugaredCmd sugaredCmd = cmd as SugaredCmd;
if (sugaredCmd != null) {
@@ -2116,7 +2116,7 @@ namespace VC { #region Insert pre- and post-conditions and where clauses as assume and assert statements
{
- CmdSeq cc = new CmdSeq();
+ List<Cmd> cc = new List<Cmd>();
// where clauses of global variables
lock (program.TopLevelDeclarations)
{
@@ -2207,7 +2207,7 @@ namespace VC { }
if (axioms.Count > 0) {
- CmdSeq cmds = new CmdSeq();
+ List<Cmd> cmds = new List<Cmd>();
foreach (Expr ax in axioms) {
Contract.Assert(ax != null);
cmds.Add(new AssumeCmd(ax.tok, ax));
@@ -2273,7 +2273,7 @@ namespace VC { foreach (var b in impl.Blocks) {
if (blocksToCheck.Contains(b)) continue;
- var newCmds = new CmdSeq();
+ var newCmds = new List<Cmd>();
var copyMode = false;
foreach (Cmd c in b.Cmds) {
var p = c as PredicateCmd;
@@ -2460,7 +2460,7 @@ namespace VC { Contract.Requires(context != null);
Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));
// After translation, all potential errors come from asserts.
- CmdSeq cmds = b.Cmds;
+ List<Cmd> cmds = b.Cmds;
Contract.Assert(cmds != null);
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
for (int i = 0; i < cmds.Count; i++)
|