diff options
33 files changed, 180 insertions, 229 deletions
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index c024a62a..0e095c44 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -658,7 +658,7 @@ namespace Microsoft.Boogie.AbstractInterpretation public override Expr VisitNAryExpr(NAryExpr node) {
if (node.Fun is UnaryOperator) {
var op = (UnaryOperator)node.Fun;
- Contract.Assert(node.Args.Length == 1);
+ Contract.Assert(node.Args.Count == 1);
if (op.Op == UnaryOperator.Opcode.Neg) {
BigInteger? lo, hi;
VisitExpr(node.Args[0]);
@@ -681,7 +681,7 @@ namespace Microsoft.Boogie.AbstractInterpretation }
} else if (node.Fun is BinaryOperator) {
var op = (BinaryOperator)node.Fun;
- Contract.Assert(node.Args.Length == 2);
+ Contract.Assert(node.Args.Count == 2);
BigInteger? lo0, hi0, lo1, hi1;
VisitExpr(node.Args[0]);
lo0 = Lo; hi0 = Hi;
@@ -837,7 +837,7 @@ namespace Microsoft.Boogie.AbstractInterpretation }
} else if (node.Fun is IfThenElse) {
var op = (IfThenElse)node.Fun;
- Contract.Assert(node.Args.Length == 3);
+ Contract.Assert(node.Args.Count == 3);
BigInteger? guardLo, guardHi, lo0, hi0, lo1, hi1;
VisitExpr(node.Args[0]);
guardLo = Lo; guardHi = Hi;
@@ -1037,7 +1037,7 @@ namespace Microsoft.Boogie.AbstractInterpretation public override Expr VisitNAryExpr(NAryExpr node) {
if (node.Fun is BinaryOperator) {
var op = (BinaryOperator)node.Fun;
- Contract.Assert(node.Args.Length == 2);
+ Contract.Assert(node.Args.Count == 2);
var arg0 = node.Args[0];
var arg1 = node.Args[1];
BigInteger? k;
diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs index a1e88656..633ad86e 100644 --- a/Source/AbsInt/Traverse.cs +++ b/Source/AbsInt/Traverse.cs @@ -88,7 +88,7 @@ namespace Microsoft.Boogie { //PM: The folowing assumption is needed because we cannot prove that a simple field update
//PM: leaves the value of a property unchanged.
- Contract.Assume(g.labelNames == null || g.labelNames.Length == g.labelTargets.Length);
+ Contract.Assume(g.labelNames == null || g.labelNames.Count == g.labelTargets.Count);
cce.EndExpose();
} else {
Contract.Assert(b.TransferCmd == null || b.TransferCmd is ReturnCmd); // It must be a returnCmd;
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 9d857e22..b29e050c 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -564,7 +564,7 @@ namespace Microsoft.Boogie { if (detLoopExtract) {
GotoCmd auxGotoCmd = block.TransferCmd as GotoCmd;
Contract.Assert(auxGotoCmd != null && auxGotoCmd.labelNames != null &&
- auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Length >= 1);
+ auxGotoCmd.labelTargets != null && auxGotoCmd.labelTargets.Count >= 1);
foreach(var bl in auxGotoCmd.labelTargets) {
bool found = false;
foreach(var n in g.NaturalLoops(header, source)) { //very expensive, can we do a contains?
@@ -621,10 +621,10 @@ namespace Microsoft.Boogie { dummyBlocks.Add(block1.Label);
GotoCmd gotoCmd = source.TransferCmd as GotoCmd;
- Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Length >= 1);
+ Contract.Assert(gotoCmd != null && gotoCmd.labelNames != null && gotoCmd.labelTargets != null && gotoCmd.labelTargets.Count >= 1);
StringSeq/*!*/ newLabels = new StringSeq();
BlockSeq/*!*/ newTargets = new BlockSeq();
- for (int i = 0; i < gotoCmd.labelTargets.Length; i++) {
+ for (int i = 0; i < gotoCmd.labelTargets.Count; i++) {
if (gotoCmd.labelTargets[i] == header)
continue;
newTargets.Add(gotoCmd.labelTargets[i]);
@@ -667,14 +667,14 @@ namespace Microsoft.Boogie { Contract.Assume(gotoCmd.labelNames != null && gotoCmd.labelTargets != null);
StringSeq newLabels = new StringSeq();
BlockSeq newTargets = new BlockSeq();
- for (int i = 0; i < gotoCmd.labelTargets.Length; i++) {
+ for (int i = 0; i < gotoCmd.labelTargets.Count; i++) {
Block target = gotoCmd.labelTargets[i];
if (blockMap.ContainsKey(target)) {
newLabels.Add(gotoCmd.labelNames[i]);
newTargets.Add(blockMap[target]);
}
}
- if (newTargets.Length == 0) {
+ if (newTargets.Count == 0) {
if (!detLoopExtract)
newBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.False));
newBlock.TransferCmd = new ReturnCmd(Token.NoToken);
@@ -2423,7 +2423,7 @@ namespace Microsoft.Boogie { e.Emit(stream, level);
}
- if (this.Modifies.Length > 0) {
+ if (this.Modifies.Count > 0) {
stream.Write(level, "modifies ");
this.Modifies.Emit(stream, false);
stream.WriteLine(";");
@@ -3209,21 +3209,6 @@ namespace Microsoft.Boogie { // Generic Sequences
//---------------------------------------------------------------------
- public sealed class TypedIdentSeq : PureCollections.Sequence {
- public TypedIdentSeq(params Type[]/*!*/ args)
- : base(args) {
- Contract.Requires(args != null);
- }
- public new TypedIdent this[int index] {
- get {
- return (TypedIdent)base[index];
- }
- set {
- base[index] = value;
- }
- }
- }
-
public sealed class VariableSeq : List<Variable> {
public VariableSeq(params Variable[]/*!*/ args)
: base(args) {
@@ -3375,7 +3360,7 @@ namespace Microsoft.Boogie { }
- public sealed class CmdSeq : PureCollections.Sequence {
+ public sealed class CmdSeq : List<Cmd> {
public CmdSeq(params Cmd[]/*!*/ args)
: base(args) {
Contract.Requires(args != null);
@@ -3712,7 +3697,7 @@ namespace Microsoft.Boogie { GotoCmd/*!*/ g = (GotoCmd)tc;
Contract.Assert(g != null);
Contract.Assume(g.labelTargets != null);
- if (g.labelTargets.Length == 1) {
+ if (g.labelTargets.Count == 1) {
return new Sequential(new AtomicRE(b), Transform(cce.NonNull(g.labelTargets[0])));
} else {
RESeq rs = new RESeq();
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 15a9fff7..bfa43a1c 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -128,7 +128,7 @@ namespace Microsoft.Boogie { Contract.Assume(PrefixCommands == null); // prefix has not been used
BigBlock bb0 = BigBlocks[0];
- if (prefixCmds.Length == 0) {
+ if (prefixCmds.Count == 0) {
// This is always a success, since there is nothing to insert. Now, decide
// which name to use for the first block.
if (bb0.Anonymous) {
@@ -369,7 +369,7 @@ namespace Microsoft.Boogie { }
} else if (bcmd.Label == bb.LabelName) {
// a break statement with a label can break out of both if statements and while statements
- if (bb.simpleCmds.Length == 0) {
+ if (bb.simpleCmds.Count == 0) {
// this is a good target: the label refers to the if/while statement
bcmd.BreakEnclosure = bb;
} else {
@@ -2700,7 +2700,7 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
- Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Length == labelTargets.Length);
+ Contract.Invariant(labelNames == null || labelTargets == null || labelNames.Count == labelTargets.Count);
}
[NotDelayed]
@@ -2715,8 +2715,8 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(labelSeq != null);
Contract.Requires(blockSeq != null);
- Debug.Assert(labelSeq.Length == blockSeq.Length);
- for (int i = 0; i < labelSeq.Length; i++) {
+ Debug.Assert(labelSeq.Count == blockSeq.Count);
+ for (int i = 0; i < labelSeq.Count; i++) {
Debug.Assert(Equals(labelSeq[i], cce.NonNull(blockSeq[i]).Label));
}
@@ -2728,7 +2728,7 @@ namespace Microsoft.Boogie { Contract.Requires(tok != null);
Contract.Requires(blockSeq != null);
StringSeq labelSeq = new StringSeq();
- for (int i = 0; i < blockSeq.Length; i++)
+ for (int i = 0; i < blockSeq.Count; i++)
labelSeq.Add(cce.NonNull(blockSeq[i]).Label);
this.labelNames = labelSeq;
this.labelTargets = blockSeq;
@@ -2783,7 +2783,7 @@ namespace Microsoft.Boogie { labelTargets.Add(b);
}
}
- Debug.Assert(rc.ErrorCount > 0 || labelTargets.Length == labelNames.Length);
+ Debug.Assert(rc.ErrorCount > 0 || labelTargets.Count == labelNames.Count);
}
public override Absy StdDispatch(StandardVisitor visitor) {
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 24622d8b..8d81c025 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1013,7 +1013,7 @@ namespace Microsoft.Boogie { Contract.Requires(tc != null);
Contract.Ensures(Contract.ValueAtReturn(out args) != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Ensures(args.Length == Contract.OldValue(args.Length));
+ Contract.Ensures(args.Count == Contract.OldValue(args.Count));
throw new NotImplementedException();
}
@@ -1108,7 +1108,7 @@ namespace Microsoft.Boogie { //Contract.Requires(stream != null);
//Contract.Requires(args != null);
stream.SetToken(ref this.tok);
- Contract.Assert(args.Length == 1);
+ Contract.Assert(args.Count == 1);
// determine if parens are needed
int opBindingStrength = 0x70;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
@@ -1144,7 +1144,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
Contract.Ensures(Contract.ValueAtReturn(out args) != null);
- Contract.Assume(args.Length == 1);
+ Contract.Assume(args.Count == 1);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type);
switch (this.op) {
@@ -1322,7 +1322,7 @@ namespace Microsoft.Boogie { //Contract.Requires(stream != null);
//Contract.Requires(args != null);
stream.SetToken(ref this.tok);
- Contract.Assert(args.Length == 2);
+ Contract.Assert(args.Count == 2);
// determine if parens are needed
int opBindingStrength;
bool fragileLeftContext = false; // false means "allow same binding power on left without parens"
@@ -1448,7 +1448,7 @@ namespace Microsoft.Boogie { //Contract.Requires(args != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
Contract.Ensures(args != null);
- Contract.Assert(args.Length == 2);
+ Contract.Assert(args.Count == 2);
// the default; the only binary operator with a type parameter is equality, but right
// we don't store this parameter because it does not appear necessary
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
@@ -1796,7 +1796,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.ValueAtReturn(out actuals) != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
Contract.Assume(this.Func != null);
- Contract.Assume(actuals.Length == Func.InParams.Length);
+ Contract.Assume(actuals.Count == Func.InParams.Length);
Contract.Assume(Func.OutParams.Length == 1);
List<Type/*!*/>/*!*/ resultingTypeArgs;
@@ -1809,7 +1809,7 @@ namespace Microsoft.Boogie { null,
// we need some token to report a possibly wrong number of
// arguments
- actuals.Length > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken,
+ actuals.Count > 0 ? cce.NonNull(actuals[0]).tok : Token.NoToken,
"application of " + name.Name,
tc);
@@ -1864,7 +1864,7 @@ namespace Microsoft.Boogie { //Contract.Requires(args != null);
//Contract.Requires(stream != null);
stream.SetToken(ref this.tok);
- Contract.Assert(args.Length == 1);
+ Contract.Assert(args.Count == 1);
// determine if parens are needed
int opBindingStrength = 0x80;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
@@ -1902,7 +1902,7 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assume(args.Length == 1);
+ Contract.Assume(args.Count == 1);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
if (!this.Type.Unify(cce.NonNull(cce.NonNull(args[0]).Type)))
@@ -2010,7 +2010,7 @@ namespace Microsoft.Boogie { Contract.Ensures(args != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assert(args.Length == 1);
+ Contract.Assert(args.Count == 1);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
@@ -2057,7 +2057,7 @@ namespace Microsoft.Boogie { Contract.Requires(args != null);
Fun = fun;
Args = args;
- Contract.Assert(Contract.ForAll(0, args.Length, index => args[index] != null));
+ Contract.Assert(Contract.ForAll(0, args.Count, index => args[index] != null));
}
[Pure]
[Reads(ReadsAttribute.Reads.Nothing)]
@@ -2113,9 +2113,9 @@ namespace Microsoft.Boogie { Contract.Assert(e != null);
e.Typecheck(tc);
}
- if (Fun.ArgumentCount != Args.Length) {
+ if (Fun.ArgumentCount != Args.Count) {
tc.Error(this, "wrong number of arguments to function: {0} ({1} instead of {2})",
- Fun.FunctionName, Args.Length, Fun.ArgumentCount);
+ Fun.FunctionName, Args.Count, Fun.ArgumentCount);
} else if (tc.ErrorCount == prevErrorCount &&
// if the type parameters are set, this node has already been
// typechecked and does not need to be checked again
@@ -2191,7 +2191,7 @@ namespace Microsoft.Boogie { int contextBindingStrength, bool fragileContext) {
//Contract.Requires(args != null);
//Contract.Requires(stream != null);
- Contract.Assume(args.Length == Arity + 1);
+ Contract.Assume(args.Count == Arity + 1);
Emit(args, stream, contextBindingStrength, fragileContext, false);
}
@@ -2211,7 +2211,7 @@ namespace Microsoft.Boogie { stream.Write("[");
string sep = "";
- int lastIndex = withRhs ? args.Length - 1 : args.Length;
+ int lastIndex = withRhs ? args.Count - 1 : args.Count;
for (int i = 1; i < lastIndex; ++i) {
stream.Write(sep);
sep = ", ";
@@ -2266,12 +2266,12 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
mapType = mapType.Expanded;
- if (mapType.IsMap && mapType.MapArity != indexes.Length) {
+ if (mapType.IsMap && mapType.MapArity != indexes.Count) {
tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1} instead of {2}",
- opName, indexes.Length, mapType.MapArity);
+ opName, indexes.Count, mapType.MapArity);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
return null;
- } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Length))) {
+ } else if (!mapType.Unify(new MapTypeProxy(map.tok, "select", indexes.Count))) {
tc.Error(map.tok, "{0} applied to a non-map: {1}", opName, map);
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
return null;
@@ -2293,10 +2293,10 @@ namespace Microsoft.Boogie { //Contract.Requires(tc != null);
//Contract.Requires(args != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assume(args.Length == Arity + 1);
+ Contract.Assume(args.Count == Arity + 1);
ExprSeq actualArgs = new ExprSeq();
- for (int i = 1; i < args.Length; ++i)
+ for (int i = 1; i < args.Count; ++i)
actualArgs.Add(args[i]);
return Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),
@@ -2317,7 +2317,7 @@ namespace Microsoft.Boogie { }
MapType mapType = a0Type.AsMap;
TypeSeq actualArgTypes = new TypeSeq();
- for (int i = 1; i < args.Length; ++i) {
+ for (int i = 1; i < args.Count; ++i) {
actualArgTypes.Add(cce.NonNull(args[i]).ShallowType);
}
return Type.InferValueType(mapType.TypeParameters, mapType.Arguments, mapType.Result, actualArgTypes);
@@ -2372,7 +2372,7 @@ namespace Microsoft.Boogie { int contextBindingStrength, bool fragileContext) {
//Contract.Requires(args != null);
//Contract.Requires(stream != null);
- Contract.Assert(args.Length == Arity + 2);
+ Contract.Assert(args.Count == Arity + 2);
MapSelect.Emit(args, stream, contextBindingStrength, fragileContext, true);
}
@@ -2401,7 +2401,7 @@ namespace Microsoft.Boogie { // part of the type checking works exactly as for MapSelect
ExprSeq selectArgs = new ExprSeq();
- for (int i = 1; i < args.Length - 1; ++i)
+ for (int i = 1; i < args.Count - 1; ++i)
selectArgs.Add(args[i]);
Type resultType =
MapSelect.Typecheck(cce.NonNull(cce.NonNull(args[0]).Type), cce.NonNull(args[0]),
@@ -2430,7 +2430,7 @@ namespace Microsoft.Boogie { //Contract.Requires(tc != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
Contract.Ensures(Contract.ValueAtReturn(out args) != null);
- Contract.Assert(args.Length == Arity + 2);
+ Contract.Assert(args.Count == Arity + 2);
return Typecheck(args, out tpInstantiation, tc, this.tok, "map store");
}
@@ -2489,7 +2489,7 @@ namespace Microsoft.Boogie { //Contract.Requires(stream != null);
//Contract.Requires(args != null);
stream.SetToken(ref this.tok);
- Contract.Assert(args.Length == 3);
+ Contract.Assert(args.Count == 3);
stream.Write("(if ");
cce.NonNull(args[0]).Emit(stream, 0x00, false);
stream.Write(" then ");
@@ -2516,7 +2516,7 @@ namespace Microsoft.Boogie { //Contract.Requires(args != null);
Contract.Ensures(args != null);
Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
- Contract.Assert(args.Length == 3);
+ Contract.Assert(args.Count == 3);
// the default; the only binary operator with a type parameter is equality, but right
// we don't store this parameter because it does not appear necessary
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index 6e719e60..a6382eb4 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -329,8 +329,8 @@ namespace Microsoft.Boogie { [ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Tr != null);
- Contract.Invariant(1 <= Tr.Length);
- Contract.Invariant(Pos || Tr.Length == 1);
+ Contract.Invariant(1 <= Tr.Count);
+ Contract.Invariant(Pos || Tr.Count == 1);
}
public Trigger Next;
@@ -339,16 +339,16 @@ namespace Microsoft.Boogie { : this(tok, pos, tr, null) {
Contract.Requires(tr != null);
Contract.Requires(tok != null);
- Contract.Requires(1 <= tr.Length);
- Contract.Requires(pos || tr.Length == 1);
+ Contract.Requires(1 <= tr.Count);
+ Contract.Requires(pos || tr.Count == 1);
}
public Trigger(IToken/*!*/ tok, bool pos, ExprSeq/*!*/ tr, Trigger next)
: base(tok) {
Contract.Requires(tok != null);
Contract.Requires(tr != null);
- Contract.Requires(1 <= tr.Length);
- Contract.Requires(pos || tr.Length == 1);
+ Contract.Requires(1 <= tr.Count);
+ Contract.Requires(pos || tr.Count == 1);
this.Pos = pos;
this.Tr = tr;
this.Next = next;
@@ -357,7 +357,7 @@ namespace Microsoft.Boogie { public void Emit(TokenTextWriter stream) {
Contract.Requires(stream != null);
stream.SetToken(this);
- Contract.Assert(this.Tr.Length >= 1);
+ Contract.Assert(this.Tr.Count >= 1);
string/*!*/ sep = Pos ? "{ " : "{:nopats ";
foreach (Expr/*!*/ e in this.Tr) {
Contract.Assert(e != null);
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index dd558f94..944bbe08 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -447,9 +447,9 @@ namespace Microsoft.Boogie { Contract.Requires(actualArgs != null);
Contract.Requires(opName != null);
Contract.Requires(tc != null);
- Contract.Requires(formalArgs.Count == actualArgs.Length);
+ Contract.Requires(formalArgs.Count == actualArgs.Count);
Contract.Requires((formalOuts == null) == (actualOuts == null));
- Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Length);
+ Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Count);
Contract.Requires(tc == null || opName != null);//Redundant
Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result<IDictionary<TypeVariable, Type>>()));
@@ -524,15 +524,15 @@ namespace Microsoft.Boogie { Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams)));
actualTypeParams = new List<Type/*!*/>();
- if (formalIns.Count != actualIns.Length) {
+ if (formalIns.Count != actualIns.Count) {
tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}",
- opName, actualIns.Length);
+ opName, actualIns.Count);
// if there are no type parameters, we can still return the result
// type and hope that the type checking proceeds
return typeParams.Count == 0 ? formalOuts : null;
- } else if (actualOuts != null && formalOuts.Count != actualOuts.Length) {
+ } else if (actualOuts != null && formalOuts.Count != actualOuts.Count) {
tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}",
- opName, actualOuts.Length);
+ opName, actualOuts.Count);
// if there are no type parameters, we can still return the result
// type and hope that the type checking proceeds
actualTypeParams = new List<Type>();
diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs index cac5068a..fd258399 100644 --- a/Source/Core/BitvectorAnalysis.cs +++ b/Source/Core/BitvectorAnalysis.cs @@ -351,7 +351,7 @@ namespace Microsoft.Boogie { public override Expr VisitNAryExpr(NAryExpr node) {
BinaryOperator op = node.Fun as BinaryOperator;
if (op != null) {
- Debug.Assert(node.Args.Length == 2);
+ Debug.Assert(node.Args.Count == 2);
MakeDisjointSet(node.Args[0]).Union(MakeDisjointSet(node.Args[1]));
}
@@ -365,7 +365,7 @@ namespace Microsoft.Boogie { x = MakeDisjointSet(node.Args[0]);
else
x = MakeDisjointSet(node);
- for (int i = 0; i < node.Args.Length; i++) {
+ for (int i = 0; i < node.Args.Count; i++) {
DisjointSet actual = MakeDisjointSet(node.Args[i]);
actual.Union(x);
}
@@ -392,8 +392,8 @@ namespace Microsoft.Boogie { int i = 0;
MapDisjointSet mapDisjointSet = (MapDisjointSet)MakeDisjointSet(node.Args[i]);
i++;
- DisjointSet[] args = new DisjointSet[node.Args.Length - 1];
- for (; i < node.Args.Length; i++) {
+ DisjointSet[] args = new DisjointSet[node.Args.Count - 1];
+ for (; i < node.Args.Count; i++) {
args[i - 1] = MakeDisjointSet(node.Args[i]);
}
mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node)));
@@ -404,8 +404,8 @@ namespace Microsoft.Boogie { int i = 0;
MapDisjointSet mapDisjointSet = (MapDisjointSet)MakeDisjointSet(node.Args[i]);
i++;
- DisjointSet[] args = new DisjointSet[node.Args.Length - 2];
- for (; i < node.Args.Length - 1; i++) {
+ DisjointSet[] args = new DisjointSet[node.Args.Count - 2];
+ for (; i < node.Args.Count - 1; i++) {
args[i - 1] = MakeDisjointSet(node.Args[i]);
}
mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node.Args[i])));
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 9cd7d524..0d737dfe 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -237,7 +237,7 @@ BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds> = (.
Contract.Requires(x != null);
Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- TypedIdentSeq/*!*/ tyds = new TypedIdentSeq();
+ List<TypedIdent>/*!*/ tyds = new List<TypedIdent>();
ds = new VariableSeq();
var dsx = ds;
.)
@@ -246,10 +246,10 @@ BoundVars<IToken/*!*/ x, out VariableSeq/*!*/ ds> /*------------------------------------------------------------------------*/
/* IdsType is used with const declarations */
-IdsType<out TypedIdentSeq/*!*/ tyds>
+IdsType<out List<TypedIdent>/*!*/ tyds>
= (. Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids; Bpl.Type/*!*/ ty; .)
Idents<out ids> ":" Type<out ty>
- (. tyds = new TypedIdentSeq();
+ (. tyds = new List<TypedIdent>();
foreach(Token/*!*/ id in ids){
Contract.Assert(id != null);
tyds.Add(new TypedIdent(id, id.val, ty, null));
@@ -379,7 +379,7 @@ Types<TypeSeq/*!*/ ts> /*------------------------------------------------------------------------*/
Consts<out VariableSeq/*!*/ ds>
-= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; TypedIdentSeq/*!*/ xs;
+= (. Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;
ds = new VariableSeq();
bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 8cd3a2ea..e1da4dd6 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -310,7 +310,7 @@ namespace Microsoft.Boogie { GotoCmd gotoCmd = (GotoCmd)b.TransferCmd;
if (gotoCmd.labelTargets == null)
continue;
- if (gotoCmd.labelTargets.Length == 1) {
+ if (gotoCmd.labelTargets.Count == 1) {
Block/*!*/ succ = cce.NonNull(gotoCmd.labelTargets[0]);
if (!multiPredBlocks.Contains(succ)) {
foreach (Cmd/*!*/ cmd in succ.Cmds) {
@@ -389,7 +389,7 @@ namespace Microsoft.Boogie { }
CmdSeq cmds = block.Cmds;
- int len = cmds.Length;
+ int len = cmds.Count;
for (int i = len - 1; i >= 0; i--) {
if (cmds[i] is CallCmd) {
Procedure/*!*/ proc = cce.NonNull(cce.NonNull((CallCmd/*!*/)cmds[i]).Proc);
@@ -470,7 +470,7 @@ namespace Microsoft.Boogie { } else if (cmd is StateCmd) {
StateCmd/*!*/ stCmd = (StateCmd)cce.NonNull(cmd);
CmdSeq/*!*/ cmds = cce.NonNull(stCmd.Cmds);
- int len = cmds.Length;
+ int len = cmds.Count;
for (int i = len - 1; i >= 0; i--) {
Propagate(cmds[i], liveSet);
}
@@ -1242,7 +1242,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; // Propagate backwards in the block
HashSet<Variable/*!*/>/*!*/ prop = new HashSet<Variable/*!*/>();
prop.UnionWith(lv);
- for (int i = block.Cmds.Length - 1; i >= 0; i--) {
+ for (int i = block.Cmds.Count - 1; i >= 0; i--) {
Cmd/*!*/ cmd = block.Cmds[i];
Contract.Assert(cmd != null);
if (cmd is CallCmd) {
@@ -1303,7 +1303,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; GenKillWeight/*!*/ w = wi.getWeightAfter();
Contract.Assert(w != null);
- for (int i = wi.block.Cmds.Length - 1; i >= 0; i--) {
+ for (int i = wi.block.Cmds.Count - 1; i >= 0; i--) {
Cmd/*!*/ c = wi.block.Cmds[i];
Contract.Assert(c != null);
if (c is CallCmd && procICFG.ContainsKey(cce.NonNull(cce.NonNull((CallCmd)c).Proc).Name)) {
@@ -1463,7 +1463,7 @@ b.liveVarsBefore = procICFG[mainImpl.Name].liveVarsAfter[b]; Contract.Assert(stCmd != null);
CmdSeq/*!*/ cmds = stCmd.Cmds;
Contract.Assert(cmds != null);
- int len = cmds.Length;
+ int len = cmds.Count;
ret = GenKillWeight.one();
for (int i = len - 1; i >= 0; i--) {
GenKillWeight/*!*/ w = getWeight(cmds[i], impl, prog);
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 47cf25d3..d2acca18 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -226,7 +226,7 @@ namespace Microsoft.Boogie { string label = block.Label;
int lblCount = 0;
- for (int i = 0; i < cmds.Length; ++i) {
+ for (int i = 0; i < cmds.Count; ++i) {
Cmd cmd = cmds[i];
CallCmd callCmd = cmd as CallCmd;
@@ -415,7 +415,7 @@ namespace Microsoft.Boogie { private CmdSeq RemoveAsserts(CmdSeq cmds) {
CmdSeq newCmdSeq = new CmdSeq();
- for (int i = 0; i < cmds.Length; i++) {
+ for (int i = 0; i < cmds.Count; i++) {
Cmd cmd = cmds[i];
if (cmd is AssertCmd) continue;
newCmdSeq.Add(cmd);
@@ -470,7 +470,7 @@ namespace Microsoft.Boogie { {
havocVars.Add(codeCopier.Subst(v));
}
- if (havocVars.Length > 0)
+ if (havocVars.Count > 0)
{
inCmds.Add(new HavocCmd(Token.NoToken, havocVars));
}
diff --git a/Source/Core/InterProceduralReachabilityGraph.cs b/Source/Core/InterProceduralReachabilityGraph.cs index 0c026757..e103c628 100644 --- a/Source/Core/InterProceduralReachabilityGraph.cs +++ b/Source/Core/InterProceduralReachabilityGraph.cs @@ -71,13 +71,13 @@ namespace Microsoft.Boogie #region Add call and return edges
foreach (var n in nodes)
{
- if (n.Cmds.Length == 1 && n.Cmds[0] is CallCmd)
+ if (n.Cmds.Count == 1 && n.Cmds[0] is CallCmd)
{
string proc = ((CallCmd)n.Cmds[0]).callee;
GotoCmd gotoCmd = n.TransferCmd as GotoCmd;
Debug.Assert(gotoCmd != null);
- for (int i = 0; i < gotoCmd.labelTargets.Length; i++)
+ for (int i = 0; i < gotoCmd.labelTargets.Count; i++)
{
(newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelTargets.Add(gotoCmd.labelTargets[i]);
(newProcedureExitNodes[proc].TransferCmd as GotoCmd).labelNames.Add(gotoCmd.labelNames[i]);
@@ -171,7 +171,7 @@ namespace Microsoft.Boogie }
Debug.Assert(prev != null);
if (b.TransferCmd is ReturnCmd || (b.TransferCmd is GotoCmd &&
- ((GotoCmd)b.TransferCmd).labelTargets.Length == 0))
+ ((GotoCmd)b.TransferCmd).labelTargets.Count == 0))
{
prev.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq { exitLabel }, new BlockSeq { newExit });
}
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 1d541183..bed2626f 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -408,7 +408,7 @@ namespace Microsoft.Boogie foreach (Block b in impl.Blocks)
{
CmdSeq newCmds = new CmdSeq();
- for (int i = 0; i < b.Cmds.Length; i++)
+ for (int i = 0; i < b.Cmds.Count; i++)
{
Cmd cmd = b.Cmds[i];
newCmds.Add(cmd);
diff --git a/Source/Core/LoopUnroll.cs b/Source/Core/LoopUnroll.cs index 403f6ff4..249e4249 100644 --- a/Source/Core/LoopUnroll.cs +++ b/Source/Core/LoopUnroll.cs @@ -268,7 +268,7 @@ namespace Microsoft.Boogie { newSuccs.Add(s);
}
- if (newSuccs.Length == 0) {
+ if (newSuccs.Count == 0) {
tcmd = new ReturnCmd(orig.TransferCmd.tok);
} else {
tcmd = new GotoCmd(orig.TransferCmd.tok, newSuccs);
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 51381625..beed64c8 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -237,14 +237,14 @@ namespace Microsoft.Boogie {
AddCallToYieldProc(newCmds, ogOldGlobalMap, domainNameToLocalVar);
- if (globalMods.Length > 0)
+ if (globalMods.Count > 0)
{
newCmds.Add(new HavocCmd(Token.NoToken, globalMods));
}
Dictionary<string, Expr> domainNameToExpr = ComputeAvailableExprs(linearTypechecker.availableLocalLinearVars[yieldCmd], domainNameToInputVar);
AddUpdatesToOldGlobalVars(newCmds, ogOldGlobalMap, domainNameToLocalVar, domainNameToExpr);
- for (int j = 0; j < cmds.Length; j++)
+ for (int j = 0; j < cmds.Count; j++)
{
PredicateCmd predCmd = (PredicateCmd)cmds[j];
newCmds.Add(new AssumeCmd(Token.NoToken, predCmd.Expr));
@@ -458,7 +458,7 @@ namespace Microsoft.Boogie {
YieldCmd yieldCmd = null;
CmdSeq newCmds = new CmdSeq();
- for (int i = 0; i < b.Cmds.Length; i++)
+ for (int i = 0; i < b.Cmds.Count; i++)
{
Cmd cmd = b.Cmds[i];
if (cmd is YieldCmd)
@@ -472,7 +472,7 @@ namespace Microsoft.Boogie if (pcmd == null)
{
DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
- if (cmds.Length > 0)
+ if (cmds.Count > 0)
{
yields.Add(cmds);
cmds = new CmdSeq();
@@ -535,7 +535,7 @@ namespace Microsoft.Boogie if (yieldCmd != null)
{
DesugarYield(yieldCmd, cmds, newCmds, ogOldGlobalMap, domainNameToInputVar, domainNameToLocalVar);
- if (cmds.Length > 0)
+ if (cmds.Count > 0)
{
yields.Add(cmds);
cmds = new CmdSeq();
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 7b172d30..c1a5efef 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -278,7 +278,7 @@ private class BvBounds : Expr { }
void Consts(out VariableSeq/*!*/ ds) {
- Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; TypedIdentSeq/*!*/ xs;
+ Contract.Ensures(Contract.ValueAtReturn(out ds) != null); IToken/*!*/ y; List<TypedIdent>/*!*/ xs;
ds = new VariableSeq();
bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
@@ -562,19 +562,19 @@ private class BvBounds : Expr { void BoundVars(IToken/*!*/ x, out VariableSeq/*!*/ ds) {
Contract.Requires(x != null);
Contract.Ensures(Contract.ValueAtReturn(out ds) != null);
- TypedIdentSeq/*!*/ tyds = new TypedIdentSeq();
+ List<TypedIdent>/*!*/ tyds = new List<TypedIdent>();
ds = new VariableSeq();
var dsx = ds;
AttrsIdsTypeWheres(true, false, "bound variables", delegate(TypedIdent tyd, QKeyValue kv) { dsx.Add(new BoundVariable(tyd.tok, tyd, kv)); } );
}
- void IdsType(out TypedIdentSeq/*!*/ tyds) {
+ void IdsType(out List<TypedIdent>/*!*/ tyds) {
Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids; Bpl.Type/*!*/ ty;
Idents(out ids);
Expect(11);
Type(out ty);
- tyds = new TypedIdentSeq();
+ tyds = new List<TypedIdent>();
foreach(Token/*!*/ id in ids){
Contract.Assert(id != null);
tyds.Add(new TypedIdent(id, id.val, ty, null));
@@ -833,7 +833,7 @@ private class BvBounds : Expr { typeParams.Add(new TypeVariable(t, t.val));}
decl = new TypeSynonymDecl(id, id.val, typeParams, body, kv);
} else {
- decl = new TypeCtorDecl(id, id.val, paramTokens.Length, kv);
+ decl = new TypeCtorDecl(id, id.val, paramTokens.Count, kv);
}
}
@@ -1664,13 +1664,13 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
Expect(18);
if (store)
- e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
+ e = new NAryExpr(x, new MapStore(x, allArgs.Count - 2), allArgs);
else if (bvExtract)
e = new BvExtractExpr(x, e,
((BvBounds)index0).Upper.ToIntSafe,
((BvBounds)index0).Lower.ToIntSafe);
else
- e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
+ e = new NAryExpr(x, new MapSelect(x, allArgs.Count - 1), allArgs);
}
}
diff --git a/Source/Core/PureCollections.cs b/Source/Core/PureCollections.cs index 58b6e9c0..8eafd73f 100644 --- a/Source/Core/PureCollections.cs +++ b/Source/Core/PureCollections.cs @@ -520,7 +520,7 @@ namespace PureCollections { public bool MoveNext() {
index++;
//while (index < seq.elems.Length); // Sequences allow nils ... && seq.elems[index] == null);
- return index < seq.Length;
+ return index < seq.Count;
}
public object Current {
get {
@@ -594,7 +594,7 @@ namespace PureCollections { }
//In place Update (and Remove) and Length - - - - - - - - - - - - - - -
- public int Length {
+ public int Count {
get {
return this.card;
}
@@ -634,40 +634,6 @@ namespace PureCollections { }
}
- public void Remove() {
- if (card == 0)
- return;
- card--;
- }
-
- // remove the first occurrence of o from this sequence
- public void Remove(Object x) {
- if (x == null)
- throw new MissingCase();
- Contract.Assert(this.elems != null);
- for (int i = 0; i < card; i++) {
- if (x.Equals(elems[i])) {
- ++i;
- while (i < card) {
- elems[i - 1] = elems[i];
- ++i;
- }
- card--;
- elems[card] = null;
- return;
- }
- }
- }
-
- public void Truncate(int newLen) {
- Contract.Requires(0 <= newLen && newLen <= Length);
- Contract.Assert(elems != null);
- for (int i = newLen; i < card; i++) {
- elems[i] = null;
- }
- card = newLen;
- }
-
//ToString - - - - - - - - - - - - - - - - - - - - - - - - - - - -
[Pure]
public override string ToString() {
diff --git a/Source/Core/ResolutionContext.cs b/Source/Core/ResolutionContext.cs index 2f840a9b..532093b1 100644 --- a/Source/Core/ResolutionContext.cs +++ b/Source/Core/ResolutionContext.cs @@ -565,7 +565,7 @@ namespace Microsoft.Boogie { public bool InFrame(Variable v) {
Contract.Requires(v != null);
Contract.Requires(Frame != null);
- return Contract.Exists(0, Frame.Length, ie => Frame[ie].Decl == v);
+ return Contract.Exists(0, Frame.Count, ie => Frame[ie].Decl == v);
}
}
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 927b73fe..77d49f3e 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -32,7 +32,7 @@ namespace Microsoft.Boogie { public virtual ExprSeq VisitExprSeq(ExprSeq list) {
Contract.Requires(list != null);
Contract.Ensures(Contract.Result<ExprSeq>() != null);
- for (int i = 0, n = list.Length; i < n; i++)
+ for (int i = 0, n = list.Count; i < n; i++)
list[i] = (Expr)this.Visit(cce.NonNull(list[i]));
return list;
}
@@ -139,7 +139,7 @@ namespace Microsoft.Boogie { public virtual BlockSeq VisitBlockSeq(BlockSeq blockSeq) {
Contract.Requires(blockSeq != null);
Contract.Ensures(Contract.Result<BlockSeq>() != null);
- for (int i = 0, n = blockSeq.Length; i < n; i++)
+ for (int i = 0, n = blockSeq.Count; i < n; i++)
blockSeq[i] = this.VisitBlock(cce.NonNull(blockSeq[i]));
return blockSeq;
}
@@ -171,7 +171,7 @@ namespace Microsoft.Boogie { public virtual CmdSeq VisitCmdSeq(CmdSeq cmdSeq) {
Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<CmdSeq>() != null);
- for (int i = 0, n = cmdSeq.Length; i < n; i++)
+ 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;
}
@@ -238,7 +238,7 @@ namespace Microsoft.Boogie { public override ExprSeq VisitExprSeq(ExprSeq exprSeq) {
//Contract.Requires(exprSeq != null);
Contract.Ensures(Contract.Result<ExprSeq>() != null);
- for (int i = 0, n = exprSeq.Length; i < n; i++)
+ for (int i = 0, n = exprSeq.Count; i < n; i++)
exprSeq[i] = this.VisitExpr(cce.NonNull(exprSeq[i]));
return exprSeq;
}
@@ -321,7 +321,7 @@ namespace Microsoft.Boogie { public virtual IdentifierExprSeq VisitIdentifierExprSeq(IdentifierExprSeq identifierExprSeq) {
Contract.Requires(identifierExprSeq != null);
Contract.Ensures(Contract.Result<IdentifierExprSeq>() != null);
- for (int i = 0, n = identifierExprSeq.Length; i < n; i++)
+ for (int i = 0, n = identifierExprSeq.Count; i < n; i++)
identifierExprSeq[i] = (IdentifierExpr)this.VisitIdentifierExpr(cce.NonNull(identifierExprSeq[i]));
return identifierExprSeq;
}
@@ -430,7 +430,7 @@ namespace Microsoft.Boogie { public virtual RESeq VisitRESeq(RESeq reSeq) {
Contract.Requires(reSeq != null);
Contract.Ensures(Contract.Result<RESeq>() != null);
- for (int i = 0, n = reSeq.Length; i < n; i++)
+ for (int i = 0, n = reSeq.Count; i < n; i++)
reSeq[i] = (RE)this.VisitRE(cce.NonNull(reSeq[i]));
return reSeq;
}
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index 2aaae096..09b6664e 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -371,21 +371,21 @@ namespace Microsoft.Boogie { IAppliable fun = ne.Fun;
ExprSeq eSeq = ne.Args;
if (fun != null) {
- if ((fun.FunctionName == "$Length" || fun.FunctionName == "$StringLength") && eSeq.Length == 1) {
+ if ((fun.FunctionName == "$Length" || fun.FunctionName == "$StringLength") && eSeq.Count == 1) {
Expr e0 = eSeq[0];
if (e0 != null) {
string s0 = PrettyPrintBplExpr(e0);
return s0 + ".Length";
}
//unexpected, just fall outside to the default
- } else if (fun.FunctionName == "$typeof" && eSeq.Length == 1) {
+ } else if (fun.FunctionName == "$typeof" && eSeq.Count == 1) {
Expr e0 = eSeq[0];
if (e0 != null) {
string s0 = PrettyPrintBplExpr(e0);
return "(the dynamic type of: " + s0 + ")";
}
//unexpected, just fall outside to the default
- } else if (fun.FunctionName == "IntArrayGet" && eSeq.Length == 2) {
+ } else if (fun.FunctionName == "IntArrayGet" && eSeq.Count == 2) {
Expr e0 = eSeq[0];
Expr e1 = eSeq[1];
if (e0 != null && e1 != null) {
@@ -394,7 +394,7 @@ namespace Microsoft.Boogie { return s0 + "[" + s1 + "]";
}
//unexpected, just fall outside to the default
- } else if (fun.FunctionName == "$Is" && eSeq.Length == 2) {
+ } else if (fun.FunctionName == "$Is" && eSeq.Count == 2) {
Expr e0 = eSeq[0];
Expr e1 = eSeq[1];
if (e0 != null && e1 != null) {
@@ -403,7 +403,7 @@ namespace Microsoft.Boogie { return "(" + s0 + " == null || (" + s0 + " is " + s1 + "))";
}
//unexpected, just fall outside to the default
- } else if (fun.FunctionName == "$IsNotNull" && eSeq.Length == 2) {
+ } else if (fun.FunctionName == "$IsNotNull" && eSeq.Count == 2) {
Expr e0 = eSeq[0];
Expr e1 = eSeq[1];
if (e0 != null && e1 != null) {
@@ -412,12 +412,12 @@ namespace Microsoft.Boogie { return "(" + s0 + " is " + s1 + ")";
}
//unexpected, just fall outside to the default
- } else if (fun is MapSelect && eSeq.Length <= 3) {
+ } else if (fun is MapSelect && eSeq.Count <= 3) {
// only maps with up to two arguments are supported right now (here)
if (cce.NonNull(eSeq[0]).ToString() == "$Heap") {
//print Index0.Index1, unless Index1 is "$elements", then just print Index0
string s0 = PrettyPrintBplExpr(cce.NonNull(eSeq[1]));
- if (eSeq.Length > 2) {
+ if (eSeq.Count > 2) {
string s1 = PrettyPrintBplExpr(cce.NonNull(eSeq[2]));
if (s1 == "$elements") {
return s0;
@@ -431,7 +431,7 @@ namespace Microsoft.Boogie { }
}
//unexpected, just fall outside to the default
- } else if (fun is Microsoft.Boogie.BinaryOperator && eSeq.Length == 2) {
+ } else if (fun is Microsoft.Boogie.BinaryOperator && eSeq.Count == 2) {
Microsoft.Boogie.BinaryOperator f = (Microsoft.Boogie.BinaryOperator)fun;
Expr e0 = eSeq[0];
Expr e1 = eSeq[1];
@@ -503,7 +503,7 @@ namespace Microsoft.Boogie { //unexpected, just fall outside to the default
} else {
string s = fun.FunctionName + "(";
- for (int i = 0; i < eSeq.Length; i++) {
+ for (int i = 0; i < eSeq.Count; i++) {
Expr ex = eSeq[i];
Contract.Assume(ex != null);
if (i > 0) {
diff --git a/Source/Core/VariableDependenceAnalyser.cs b/Source/Core/VariableDependenceAnalyser.cs index fd69d911..476f1cac 100644 --- a/Source/Core/VariableDependenceAnalyser.cs +++ b/Source/Core/VariableDependenceAnalyser.cs @@ -360,7 +360,7 @@ namespace Microsoft.Boogie { HashSet<VariableDescriptor> result = new HashSet<VariableDescriptor>();
var gotoCmd = b.TransferCmd as GotoCmd;
- if (gotoCmd != null && gotoCmd.labelTargets.Length >= 2) {
+ if (gotoCmd != null && gotoCmd.labelTargets.Count >= 2) {
foreach (Block succ in gotoCmd.labelTargets) {
foreach (Cmd c in succ.Cmds) {
AssumeCmd a = c as AssumeCmd;
diff --git a/Source/Doomed/DoomCheck.cs b/Source/Doomed/DoomCheck.cs index 6b9f91cf..83de03ff 100644 --- a/Source/Doomed/DoomCheck.cs +++ b/Source/Doomed/DoomCheck.cs @@ -375,7 +375,7 @@ void ObjectInvariant() }
} else {
Contract.Assert( gotocmd.labelTargets != null);
- List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
+ List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Count);
foreach (Block successor in gotocmd.labelTargets) {
Contract.Assert(successor != null);
int ac;
diff --git a/Source/Doomed/DoomedStrategy.cs b/Source/Doomed/DoomedStrategy.cs index eb5716bb..9e280873 100644 --- a/Source/Doomed/DoomedStrategy.cs +++ b/Source/Doomed/DoomedStrategy.cs @@ -111,14 +111,14 @@ namespace VC private List<int> __leavespp = new List<int>();
protected void m_GatherInfo(Block b, int branchingdepth, int leavespp, int plen)
{
- if (b.Predecessors.Length > 1) branchingdepth--;
+ if (b.Predecessors.Count > 1) branchingdepth--;
GotoCmd gc = b.TransferCmd as GotoCmd;
if (__DEBUG_minelements.Contains(b)) leavespp++;
plen++;
- if (gc != null && gc.labelTargets.Length>0)
+ if (gc != null && gc.labelTargets.Count>0)
{
- if (gc.labelTargets.Length > 1) branchingdepth++;
+ if (gc.labelTargets.Count > 1) branchingdepth++;
m_MaxBranchingDepth = (branchingdepth > m_MaxBranchingDepth) ? branchingdepth : m_MaxBranchingDepth;
foreach (Block s in gc.labelTargets)
{
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 2ff5975e..ceef059e 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -3237,7 +3237,7 @@ namespace Microsoft.Boogie.Houdini { var nexpr = expr as NAryExpr;
if (nexpr != null && (nexpr.Fun is BinaryOperator)
&& (nexpr.Fun as BinaryOperator).Op == BinaryOperator.Opcode.Imp
- && (nexpr.Args.Length == 2))
+ && (nexpr.Args.Count == 2))
{
postExpr = nexpr.Args[1];
preExpr = nexpr.Args[0];
@@ -3335,7 +3335,7 @@ namespace Microsoft.Boogie.Houdini { {
return ToElem((nary.Fun as BinaryOperator).Evaluate(ToValue(Eval(nary.Args[0], state)), ToValue(Eval(nary.Args[1], state))));
}
- if (nary.Fun is MapSelect && nary.Args.Length == 2)
+ if (nary.Fun is MapSelect && nary.Args.Count == 2)
{
var index = Eval(nary.Args[1], state);
var map = Eval(nary.Args[0], state) as Model.Array;
@@ -3649,7 +3649,7 @@ namespace Microsoft.Boogie.Houdini { {
return gen.Function(Translate(nary.Fun as BinaryOperator), ToVcExpr(nary.Args[0], incarnations, gen), ToVcExpr(nary.Args[1], incarnations, gen));
}
- if (nary.Fun is MapSelect && nary.Args.Length == 2)
+ if (nary.Fun is MapSelect && nary.Args.Count == 2)
{
return gen.Select(ToVcExpr(nary.Args[0], incarnations, gen), ToVcExpr(nary.Args[1], incarnations, gen));
}
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 5078d5a5..f896c27f 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -251,7 +251,7 @@ namespace Microsoft.Boogie.Houdini { Contract.Requires(cmdSeq != null);
Contract.Ensures(Contract.Result<CmdSeq>() != null);
CmdSeq newCmdSeq = new CmdSeq();
- for (int i = 0, n = cmdSeq.Length; i < n; i++) {
+ for (int i = 0, n = cmdSeq.Count; i < n; i++) {
Cmd cmd = cmdSeq[i];
CallCmd callCmd = cmd as CallCmd;
if (callCmd != null) {
diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index 83be688e..eac60511 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -76,7 +76,7 @@ public class BlockPredicator { // This may be a loop invariant. Make sure it continues to appear as
// the first statement in the block.
var assign = cmdSeq.Last();
- cmdSeq.Truncate(cmdSeq.Length-1);
+ cmdSeq.RemoveAt(cmdSeq.Count-1);
Expr newExpr = new EnabledReplacementVisitor(pExpr).VisitExpr(aCmd.Expr);
aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(pExpr, newExpr);
cmdSeq.Add(aCmd);
diff --git a/Source/Predication/SmartBlockPredicator.cs b/Source/Predication/SmartBlockPredicator.cs index 55e73161..9dc10d02 100644 --- a/Source/Predication/SmartBlockPredicator.cs +++ b/Source/Predication/SmartBlockPredicator.cs @@ -146,13 +146,13 @@ public class SmartBlockPredicator { hasPredicatedRegion = hasPredicatedRegion ||
gCmd.labelTargets.Cast<Block>().Any(b => predMap.ContainsKey(b));
- if (gCmd.labelTargets.Length == 1) {
+ if (gCmd.labelTargets.Count == 1) {
if (defMap.ContainsKey(gCmd.labelTargets[0]))
PredicateCmd(p, cmdSeq,
Cmd.SimpleAssign(Token.NoToken,
Expr.Ident(predMap[gCmd.labelTargets[0]]), Expr.True));
} else {
- Debug.Assert(gCmd.labelTargets.Length > 1);
+ Debug.Assert(gCmd.labelTargets.Count > 1);
Debug.Assert(gCmd.labelTargets.Cast<Block>().All(t => uni.IsUniform(impl.Name, t) ||
partInfo.ContainsKey(t)));
foreach (Block target in gCmd.labelTargets) {
@@ -353,9 +353,9 @@ public class SmartBlockPredicator { }
Block realDest = block;
- if (block.Cmds.Length == 0) {
+ if (block.Cmds.Count == 0) {
var gc = block.TransferCmd as GotoCmd;
- if (gc != null && gc.labelTargets.Length == 1)
+ if (gc != null && gc.labelTargets.Count == 1)
realDest = gc.labelTargets[0];
}
partInfo[block] = new PartInfo(pred, realDest);
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 6273f056..a110c817 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -377,7 +377,7 @@ namespace Microsoft.Boogie.VCExprAST { private VCExpr TranslateNAryExpr(NAryExpr node) {
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- int n = node.Args.Length;
+ int n = node.Args.Count;
List<VCExpr/*!*/>/*!*/ vcs = new List<VCExpr/*!*/>(n);
for (int i = 0; i < n; i++) {
vcs.Add(Translate(cce.NonNull(node.Args)[i]));
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index dbe20415..fe8d67f5 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -123,9 +123,9 @@ namespace Microsoft.Boogie { // Looks up the Cmd at a given index into the trace
public Cmd getTraceCmd(TraceLocation loc)
{
- Debug.Assert(loc.numBlock < Trace.Length);
+ Debug.Assert(loc.numBlock < Trace.Count);
Block b = Trace[loc.numBlock];
- Debug.Assert(loc.numInstr < b.Cmds.Length);
+ Debug.Assert(loc.numInstr < b.Cmds.Count);
return b.Cmds[loc.numInstr];
}
@@ -168,7 +168,7 @@ namespace Microsoft.Boogie { tw.WriteLine("{4}{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label, ind);
- for (int numInstr = 0; numInstr < b.Cmds.Length; numInstr++)
+ for (int numInstr = 0; numInstr < b.Cmds.Count; numInstr++)
{
var loc = new TraceLocation(numBlock, numInstr);
if (calleeCounterexamples.ContainsKey(loc))
@@ -314,16 +314,16 @@ namespace Microsoft.Boogie { private int Compare(BlockSeq bs1, BlockSeq bs2)
{
- if (bs1.Length < bs2.Length)
+ if (bs1.Count < bs2.Count)
{
return -1;
}
- else if (bs2.Length < bs1.Length)
+ else if (bs2.Count < bs1.Count)
{
return 1;
}
- for (int i = 0; i < bs1.Length; i++)
+ for (int i = 0; i < bs1.Count; i++)
{
var b1 = bs1[i];
var b2 = bs2[i];
@@ -1193,7 +1193,7 @@ namespace VC { Contract.Requires(block2Incarnation != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
- if (b.Predecessors.Length == 0) {
+ if (b.Predecessors.Count == 0) {
return new Dictionary<Variable, Expr>();
}
@@ -1376,7 +1376,7 @@ namespace VC { }
else {
// incarnationMap needs to be added only if there is some successor of b
- b.succCount = gotoCmd.labelNames.Length;
+ b.succCount = gotoCmd.labelNames.Count;
block2Incarnation.Add(b, incarnationMap);
}
#endregion Each block's map needs to be available to successor blocks
@@ -1608,7 +1608,7 @@ namespace VC { /// succ. Caller must do the add to impl.Blocks.
/// </summary>
protected Block CreateBlockBetween(int predIndex, Block succ) {
- Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Length);
+ Contract.Requires(0 <= predIndex && predIndex < succ.Predecessors.Count);
Contract.Requires(succ != null);
@@ -1641,7 +1641,7 @@ namespace VC { GotoCmd gtc = (GotoCmd)cce.NonNull(pred.TransferCmd);
Contract.Assume(gtc.labelTargets != null);
Contract.Assume(gtc.labelNames != null);
- for (int i = 0, n = gtc.labelTargets.Length; i < n; i++) {
+ for (int i = 0, n = gtc.labelTargets.Count; i < n; i++) {
if (gtc.labelTargets[i] == succ) {
gtc.labelTargets[i] = newBlock;
gtc.labelNames[i] = newBlockLabel;
@@ -1661,12 +1661,12 @@ namespace VC { #region Introduce empty blocks between join points and their multi-successor predecessors
List<Block> tweens = new List<Block>();
foreach (Block b in blocks) {
- int nPreds = b.Predecessors.Length;
+ int nPreds = b.Predecessors.Count;
if (nPreds > 1) {
// b is a join point (i.e., it has more than one predecessor)
for (int i = 0; i < nPreds; i++) {
GotoCmd gotocmd = (GotoCmd)(cce.NonNull(b.Predecessors[i]).TransferCmd);
- if (gotocmd.labelNames != null && gotocmd.labelNames.Length > 1) {
+ if (gotocmd.labelNames != null && gotocmd.labelNames.Count > 1) {
tweens.Add(CreateBlockBetween(i, b));
}
}
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index 78ed8cb5..ac7ee9be 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -253,7 +253,7 @@ namespace Microsoft.Boogie info.type = AnnotationInfo.AnnotationType.LoopInvariant;
annotationInfo.Add(name, info);
// get file and line info from havoc, if there is...
- if (header.Cmds.Length > 0)
+ if (header.Cmds.Count > 0)
{
PredicateCmd bif = header.Cmds[0] as PredicateCmd;
if (bif != null)
@@ -1177,7 +1177,7 @@ namespace Microsoft.Boogie }
CmdSeq cmds = block.Cmds;
- int len = cmds.Length;
+ int len = cmds.Count;
for (int i = len - 1; i >= 0; i--)
{
if (cmds[i] is CallCmd)
@@ -1657,7 +1657,7 @@ namespace Microsoft.Boogie CmdSeq cmds = b.Cmds;
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Length; i++)
+ for (int i = 0; i < cmds.Count; i++)
{
Cmd cmd = cce.NonNull(cmds[i]);
@@ -1723,7 +1723,7 @@ namespace Microsoft.Boogie {
RPFP.Node callee = root.Outgoing.Children[pos];
orderedStateIds.Add(new StateId(callee.Outgoing, CALL,info));
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
new CalleeCounterexampleInfo(
cce.NonNull(GenerateTrace(rpfp, callee, orderedStateIds,
implName2StratifiedInliningInfo[calleeName].impl, false)),
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index da413984..c5d88c5c 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -360,7 +360,7 @@ namespace VC { var callSiteId = 0;
foreach (Block block in implementation.Blocks) {
CmdSeq newCmds = new CmdSeq();
- for (int i = 0; i < block.Cmds.Length; i++) {
+ for (int i = 0; i < block.Cmds.Count; i++) {
Cmd cmd = block.Cmds[i];
newCmds.Add(cmd);
AssumeCmd assumeCmd = cmd as AssumeCmd;
@@ -380,7 +380,7 @@ namespace VC { public Dictionary<Block, List<CallSite>> CollectCallSites(Implementation implementation) {
var callSites = new Dictionary<Block, List<CallSite>>();
foreach (Block block in implementation.Blocks) {
- for (int i = 0; i < block.Cmds.Length; i++) {
+ for (int i = 0; i < block.Cmds.Count; i++) {
Cmd cmd = block.Cmds[i];
AssumeCmd assumeCmd = cmd as AssumeCmd;
if (assumeCmd == null) continue;
@@ -407,7 +407,7 @@ namespace VC { public Dictionary<Block, List<CallSite>> CollectRecordProcedureCallSites(Implementation implementation) {
var callSites = new Dictionary<Block, List<CallSite>>();
foreach (Block block in implementation.Blocks) {
- for (int i = 0; i < block.Cmds.Length; i++) {
+ for (int i = 0; i < block.Cmds.Count; i++) {
AssumeCmd assumeCmd = block.Cmds[i] as AssumeCmd;
if (assumeCmd == null) continue;
NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;
@@ -2584,7 +2584,7 @@ namespace VC { while (true) {
CmdSeq cmds = b.Cmds;
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Length; i++) {
+ for (int i = 0; i < cmds.Count; i++) {
Cmd cmd = cce.NonNull(cmds[i]);
// Skip if 'cmd' not contained in the trace or not an assert
@@ -2662,7 +2662,7 @@ namespace VC { Contract.Assert(false);
}
}
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
new CalleeCounterexampleInfo(null, args);
continue;
}
@@ -2680,7 +2680,7 @@ namespace VC { else {
orderedStateIds.Add(new Tuple<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
var calleeInfo = implName2StratifiedInliningInfo[calleeName];
- calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ calleeCounterexamples[new TraceLocation(trace.Count - 1, i)] =
new CalleeCounterexampleInfo(GenerateTrace(labels, errModel, calleeId, calleeInfo.impl, calleeInfo.mvInfo), new List<object>());
orderedStateIds.Add(new Tuple<int, int>(candidateId, StratifiedInliningErrorReporter.RETURN));
}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 055a79ad..873a5589 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -415,9 +415,9 @@ namespace VC { GotoCmd go = cur.TransferCmd as GotoCmd;
ReturnCmd ret = cur.TransferCmd as ReturnCmd;
- Contract.Assume(!(go != null && go.labelTargets == null && go.labelNames != null && go.labelNames.Length > 0));
+ Contract.Assume(!(go != null && go.labelTargets == null && go.labelNames != null && go.labelNames.Count > 0));
- if (ret != null || (go != null && cce.NonNull(go.labelTargets).Length == 0)) {
+ if (ret != null || (go != null && cce.NonNull(go.labelTargets).Count == 0)) {
// we end in return, so there will be no more places to check
CheckUnreachable(cur, seq);
} else if (go != null) {
@@ -426,7 +426,7 @@ namespace VC { // we're in the right place to check
foreach (Block target in cce.NonNull(go.labelTargets)) {
Contract.Assert(target != null);
- if (target.Predecessors.Length == 1) {
+ if (target.Predecessors.Count == 1) {
needToCheck = false;
}
}
@@ -668,7 +668,7 @@ namespace VC { Block next = s.virtual_successors[0];
BlockStats se = GetBlockStats(next);
CountAssertions(next);
- if (next.Predecessors.Length > 1 || se.virtual_successors.Count != 1)
+ if (next.Predecessors.Count > 1 || se.virtual_successors.Count != 1)
return;
s.virtual_successors[0] = se.virtual_successors[0];
s.assertion_cost += se.assertion_cost;
@@ -745,7 +745,7 @@ namespace VC { if (gt == null)
continue;
BlockSeq targ = cce.NonNull(gt.labelTargets);
- if (targ.Length < 2)
+ if (targ.Count < 2)
continue;
// caution, we only consider two first exits
@@ -758,7 +758,7 @@ namespace VC { right0 = DoComputeScore(false);
assumized_branches.Clear();
- for (int idx = 1; idx < targ.Length; idx++) {
+ for (int idx = 1; idx < targ.Count; idx++) {
assumized_branches.Add(cce.NonNull(targ[idx]));
}
left1 = DoComputeScore(true);
@@ -1314,7 +1314,7 @@ namespace VC { cache.Add(t);
}
- for (int i = 0; i < orig.Cmds.Length; ++i) {
+ for (int i = 0; i < orig.Cmds.Count; ++i) {
Cmd cmd = orig.Cmds[i];
if (cmd is AssertCmd) {
int found = 0;
@@ -1913,7 +1913,7 @@ namespace VC { #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();
- for (int i = 0, n = header.Cmds.Length; i < n; i++)
+ for (int i = 0, n = header.Cmds.Count; i < n; i++)
{
PredicateCmd a = header.Cmds[i] as PredicateCmd;
if (a != null)
@@ -1952,14 +1952,14 @@ namespace VC { #endregion
#region Copy the prefix of predicate commands into each predecessor. Do this *before* cutting the backedge!!
- for ( int predIndex = 0, n = header.Predecessors.Length; predIndex < n; predIndex++ )
+ for ( int predIndex = 0, n = header.Predecessors.Count; predIndex < n; predIndex++ )
{
Block pred = cce.NonNull(header.Predecessors[predIndex]);
// Create a block between header and pred for the predicate commands if pred has more than one successor
GotoCmd gotocmd = cce.NonNull((GotoCmd)pred.TransferCmd);
Contract.Assert( gotocmd.labelNames != null); // if "pred" is really a predecessor, it may be a GotoCmd with at least one label
- if (gotocmd.labelNames.Length > 1)
+ if (gotocmd.labelNames.Count > 1)
{
Block newBlock = CreateBlockBetween(predIndex, header);
impl.Blocks.Add(newBlock);
@@ -1988,13 +1988,13 @@ namespace VC { {Contract.Assert(backEdgeNode != null);
Debug.Assert(backEdgeNode.TransferCmd is GotoCmd,"An node was identified as the source for a backedge, but it does not have a goto command.");
GotoCmd gtc = backEdgeNode.TransferCmd as GotoCmd;
- if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length > 1 )
+ 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();
StringSeq remainingLabels = new StringSeq();
Contract.Assume( gtc.labelNames != null);
- for (int i = 0, n = gtc.labelTargets.Length; i < n; i++)
+ for (int i = 0, n = gtc.labelTargets.Count; i < n; i++)
{
if (gtc.labelTargets[i] != header)
{
@@ -2015,7 +2015,7 @@ namespace VC { AssumeCmd ac = new AssumeCmd(Token.NoToken,Expr.False);
backEdgeNode.Cmds.Add(ac);
backEdgeNode.TransferCmd = new ReturnCmd(Token.NoToken);
- if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length == 1)
+ if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Count == 1)
RecordCutEdge(edgesCut, backEdgeNode, gtc.labelTargets[0]);
}
#region Remove the backedge node from the list of predecessor nodes in the header
@@ -2331,13 +2331,13 @@ namespace VC { ret.Trace = new BlockSeq();
ret.calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();
- for (int numBlock = 0; numBlock < cex.Trace.Length; numBlock ++ )
+ for (int numBlock = 0; numBlock < cex.Trace.Count; numBlock ++ )
{
Block block = cex.Trace[numBlock];
var origBlock = elGetBlock(currProc, block, extractLoopMappingInfo);
if (origBlock != null) ret.Trace.Add(origBlock);
var callCnt = 1;
- for (int numInstr = 0; numInstr < block.Cmds.Length; numInstr ++) {
+ for (int numInstr = 0; numInstr < block.Cmds.Count; numInstr ++) {
Cmd cmd = block.Cmds[numInstr];
var loc = new TraceLocation(numBlock, numInstr);
if (!cex.calleeCounterexamples.ContainsKey(loc))
@@ -2356,7 +2356,7 @@ namespace VC { {
// Absorb the trace into the current trace
- int currLen = ret.Trace.Length;
+ int currLen = ret.Trace.Count;
ret.Trace.AddRange(origTrace.counterexample.Trace);
foreach (var kvp in origTrace.counterexample.calleeCounterexamples)
@@ -2368,7 +2368,7 @@ namespace VC { }
else
{
- var origLoc = new TraceLocation(ret.Trace.Length - 1, getCallCmdPosition(origBlock, callCnt, inlinedProcs, callee));
+ var origLoc = new TraceLocation(ret.Trace.Count - 1, getCallCmdPosition(origBlock, callCnt, inlinedProcs, callee));
ret.calleeCounterexamples.Add(origLoc, origTrace);
callCnt++;
}
@@ -2383,7 +2383,7 @@ namespace VC { private int getCallCmdPosition(Block block, int i, HashSet<string> inlinedProcs, string callee)
{
Debug.Assert(i >= 1);
- for (int pos = 0; pos < block.Cmds.Length; pos++)
+ for (int pos = 0; pos < block.Cmds.Count; pos++)
{
Cmd cmd = block.Cmds[pos];
string procCalled = getCallee(cmd, inlinedProcs);
@@ -2463,7 +2463,7 @@ namespace VC { CmdSeq cmds = b.Cmds;
Contract.Assert(cmds != null);
TransferCmd transferCmd = cce.NonNull(b.TransferCmd);
- for (int i = 0; i < cmds.Length; i++)
+ for (int i = 0; i < cmds.Count; i++)
{
Cmd cmd = cce.NonNull( cmds[i]);
@@ -2588,7 +2588,7 @@ namespace VC { }
else {
Contract.Assert(gotocmd.labelTargets != null);
- List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
+ List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Count);
foreach (Block successor in gotocmd.labelTargets) {
Contract.Assert(successor != null);
VCExpr s = blockVariables[successor];
@@ -2652,7 +2652,7 @@ namespace VC { }
} else {
Contract.Assert( gotocmd.labelTargets != null);
- List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
+ List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Count);
foreach (Block successor in gotocmd.labelTargets) {
Contract.Assert(successor != null);
int ac;
@@ -3065,9 +3065,9 @@ namespace VC { GotoCmd gtc = b.TransferCmd as GotoCmd;
// b has no successors
- if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Length == 0)
+ if (gtc == null || gtc.labelTargets == null || gtc.labelTargets.Count == 0)
{
- if (b.Cmds.Length != 0){ // only empty blocks are removed...
+ if (b.Cmds.Count != 0){ // only empty blocks are removed...
bs.Add(b);
} else if (b.tok.IsValid) {
renameInfoForStartBlock = b;
@@ -3086,11 +3086,11 @@ namespace VC { // by pushing the location onto b's successor. This can be done if (0) b has
// exactly one successor, (1) that successor has no location of its own, and
// (2) that successor has no other predecessors.
- if (b.Cmds.Length == 0 && !startNode) {
+ if (b.Cmds.Count == 0 && !startNode) {
// b is about to become extinct; try to save its name and location, if possible
- if (b.tok.IsValid && gtc.labelTargets.Length == 1) {
+ if (b.tok.IsValid && gtc.labelTargets.Count == 1) {
Block succ = cce.NonNull(gtc.labelTargets[0]);
- if (!succ.tok.IsValid && succ.Predecessors.Length == 1) {
+ if (!succ.tok.IsValid && succ.Predecessors.Count == 1) {
succ.tok = b.tok;
succ.Label = b.Label;
}
@@ -3121,7 +3121,7 @@ namespace VC { BlockSeq setOfSuccessors = new BlockSeq();
foreach (Block d in mergedSuccessors)
setOfSuccessors.Add(d);
- if (b.Cmds.Length == 0 && !startNode) {
+ if (b.Cmds.Count == 0 && !startNode) {
// b is about to become extinct
if (b.tok.IsValid) {
renameInfoForStartBlock = b;
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index eed4e2a5..277d9a94 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -59,7 +59,7 @@ namespace VC { VCExpr res = N;
- for (int i = b.Cmds.Length; --i >= 0; )
+ for (int i = b.Cmds.Count; --i >= 0; )
{
res = Cmd(b, cce.NonNull( b.Cmds[i]), res, ctxt);
}
@@ -200,14 +200,14 @@ namespace VC { {
Choice ch = (Choice) r;
VCExpr res;
- if (ch.rs == null || ch.rs.Length==0)
+ if (ch.rs == null || ch.rs.Count==0)
{
res = N;
}
else
{
VCExpr currentWLP = RegExpr(cce.NonNull(ch.rs[0]), N, ctxt);
- for (int i = 1, n = ch.rs.Length; i < n; i++)
+ for (int i = 1, n = ch.rs.Count; i < n; i++)
{
currentWLP = ctxt.Ctxt.ExprGen.And(currentWLP, RegExpr(cce.NonNull(ch.rs[i]), N, ctxt));
}
|