diff options
| author |  Ally Donaldson <unknown> | 2013-07-22 19:12:40 +0100 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-07-22 19:12:40 +0100 |
| commit | eea0a9e74d6782d08f8dd01c0e1dbec15f1a02cb (patch) | |
| tree | 26b5693006a283d80fb47507263e404c282ae2ef | |
| parent | 62d2fa72d5e1816d6cb1239063302808424c6d13 (diff) | |
More refactoring
24 files changed, 164 insertions, 186 deletions
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 6b0fcdb3..347e3db7 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -11,6 +11,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { using System.Diagnostics.Contracts;
using System.Collections;
using System.Collections.Generic;
+ using System.Linq;
public class CallSite {
public readonly Implementation/*!*/ Impl;
@@ -71,6 +72,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { namespace Microsoft.Boogie {
using System;
+ using System.Linq;
using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
@@ -210,7 +212,7 @@ namespace Microsoft.Boogie { TopLevelDeclarations = prunedTopLevelDeclarations;
foreach (DatatypeConstructor f in constructors.Values) {
- for (int i = 0; i < f.InParams.Length; i++) {
+ for (int i = 0; i < f.InParams.Count; i++) {
DatatypeSelector selector = new DatatypeSelector(f, i);
f.selectors.Add(selector);
TopLevelDeclarations.Add(selector);
@@ -1843,10 +1845,10 @@ namespace Microsoft.Boogie { stream.Write(")");
if (shortRet) {
- Contract.Assert(OutParams.Length == 1);
+ Contract.Assert(OutParams.Count == 1);
stream.Write(" : ");
cce.NonNull(OutParams[0]).TypedIdent.Type.Emit(stream);
- } else if (OutParams.Length > 0) {
+ } else if (OutParams.Count > 0) {
stream.Write(" returns (");
OutParams.Emit(stream, true);
stream.Write(")");
@@ -1863,9 +1865,9 @@ namespace Microsoft.Boogie { }
protected void SortTypeParams() {
- TypeSeq/*!*/ allTypes = InParams.ToTypeSeq;
+ TypeSeq/*!*/ allTypes = new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray());
Contract.Assert(allTypes != null);
- allTypes.AddRange(OutParams.ToTypeSeq);
+ allTypes.AddRange(new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()));
TypeParameters = Type.SortTypeParams(TypeParameters, allTypes, null);
}
@@ -2089,7 +2091,8 @@ namespace Microsoft.Boogie { }
rc.PopVarContext();
Type.CheckBoundVariableOccurrences(TypeParameters,
- InParams.ToTypeSeq, OutParams.ToTypeSeq,
+ new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
+ new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),
this.tok, "function arguments",
rc);
} finally {
@@ -2151,7 +2154,7 @@ namespace Microsoft.Boogie { // type parameters only occur in the output type
call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());
Expr def = Expr.Eq(call, definition);
- if (quantifiedTypeVars.Count != 0 || dummies.Length != 0) {
+ if (quantifiedTypeVars.Count != 0 || dummies.Count != 0) {
def = new ForallExpr(tok, quantifiedTypeVars, dummies,
kv,
new Trigger(tok, true, new ExprSeq(call), null),
@@ -2481,7 +2484,8 @@ namespace Microsoft.Boogie { ResolveAttributes(rc);
Type.CheckBoundVariableOccurrences(TypeParameters,
- InParams.ToTypeSeq, OutParams.ToTypeSeq,
+ new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
+ new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),
this.tok, "procedure arguments",
rc);
@@ -2750,7 +2754,7 @@ namespace Microsoft.Boogie { }
if (this.StructuredStmts != null && !CommandLineOptions.Clo.PrintInstrumented && !CommandLineOptions.Clo.PrintInlined) {
- if (this.LocVars.Length > 0) {
+ if (this.LocVars.Count > 0) {
stream.WriteLine();
}
if (CommandLineOptions.Clo.PrintUnstructured < 2) {
@@ -2829,7 +2833,8 @@ namespace Microsoft.Boogie { rc.PopVarContext();
Type.CheckBoundVariableOccurrences(TypeParameters,
- InParams.ToTypeSeq, OutParams.ToTypeSeq,
+ new TypeSeq(InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
+ new TypeSeq(OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),
this.tok, "implementation arguments",
rc);
} finally {
@@ -2870,7 +2875,7 @@ namespace Microsoft.Boogie { Contract.Requires(procFormals != null);
Contract.Requires(inout != null);
Contract.Requires(tc != null);
- if (implFormals.Length != procFormals.Length) {
+ if (implFormals.Count != procFormals.Count) {
tc.Error(this, "mismatched number of {0}-parameters in procedure implementation: {1}",
inout, this.Name);
} else {
@@ -2891,7 +2896,7 @@ namespace Microsoft.Boogie { subst2.Add(this.TypeParameters[i], newVar);
}
- for (int i = 0; i < implFormals.Length; i++) {
+ for (int i = 0; i < implFormals.Count; i++) {
// the names of the formals are allowed to change from the proc to the impl
// but types must be identical
@@ -2924,11 +2929,11 @@ namespace Microsoft.Boogie { if (this.formalMap != null)
return this.formalMap;
else {
- Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Length + OutParams.Length);
+ Dictionary<Variable, Expr>/*!*/ map = new Dictionary<Variable, Expr> (InParams.Count + OutParams.Count);
Contract.Assume(this.Proc != null);
- Contract.Assume(InParams.Length == Proc.InParams.Length);
- for (int i = 0; i < InParams.Length; i++) {
+ Contract.Assume(InParams.Count == Proc.InParams.Count);
+ for (int i = 0; i < InParams.Count; i++) {
Variable/*!*/ v = InParams[i];
Contract.Assert(v != null);
IdentifierExpr ie = new IdentifierExpr(v.tok, v);
@@ -2936,8 +2941,8 @@ namespace Microsoft.Boogie { Contract.Assert(pv != null);
map.Add(pv, ie);
}
- System.Diagnostics.Debug.Assert(OutParams.Length == Proc.OutParams.Length);
- for (int i = 0; i < OutParams.Length; i++) {
+ System.Diagnostics.Debug.Assert(OutParams.Count == Proc.OutParams.Count);
+ for (int i = 0; i < OutParams.Count; i++) {
Variable/*!*/ v = cce.NonNull(OutParams[i]);
IdentifierExpr ie = new IdentifierExpr(v.tok, v);
Variable pv = cce.NonNull(Proc.OutParams[i]);
@@ -3209,12 +3214,6 @@ namespace Microsoft.Boogie { // Generic Sequences
//---------------------------------------------------------------------
- public static class ListFactory {
- public static List<T> MakeList<T>(params T[]/*!*/ args) {
- return new List<T>(args);
- }
- }
-
public sealed class VariableSeq : List<Variable> {
public VariableSeq(params Variable[]/*!*/ args)
: base(args) {
@@ -3224,33 +3223,6 @@ namespace Microsoft.Boogie { : base(varSeq) {
Contract.Requires(varSeq != null);
}
- public void Emit(TokenTextWriter stream, bool emitAttributes) {
- Contract.Requires(stream != null);
- string sep = "";
- foreach (Variable/*!*/ v in this) {
- Contract.Assert(v != null);
- stream.Write(sep);
- sep = ", ";
- v.EmitVitals(stream, 0, emitAttributes);
- }
- }
- public TypeSeq/*!*/ ToTypeSeq {
- get {
- Contract.Ensures(Contract.Result<TypeSeq>() != null);
-
- TypeSeq/*!*/ res = new TypeSeq();
- foreach (Variable/*!*/ v in this) {
- Contract.Assert(v != null);
- res.Add(v.TypedIdent.Type);
- }
- return res;
- }
- }
- public int Length {
- get {
- return Count;
- }
- }
}
public sealed class TypeSeq : List<Type> {
@@ -3262,17 +3234,6 @@ namespace Microsoft.Boogie { : base(varSeq) {
Contract.Requires(varSeq != null);
}
- public void Emit(TokenTextWriter stream, string separator) {
- Contract.Requires(separator != null);
- Contract.Requires(stream != null);
- string sep = "";
- foreach (Type/*!*/ v in this) {
- Contract.Assert(v != null);
- stream.Write(sep);
- sep = separator;
- v.Emit(stream);
- }
- }
}
public sealed class TypeVariableSeq : List<TypeVariable> {
@@ -3296,17 +3257,6 @@ namespace Microsoft.Boogie { this.Add(next);
}
}
- public void Emit(TokenTextWriter stream, string separator) {
- Contract.Requires(separator != null);
- Contract.Requires(stream != null);
- string sep = "";
- foreach (TypeVariable/*!*/ v in this) {
- Contract.Assert(v != null);
- stream.Write(sep);
- sep = separator;
- v.Emit(stream);
- }
- }
}
public sealed class IdentifierExprSeq : List<IdentifierExpr> {
@@ -3318,33 +3268,7 @@ namespace Microsoft.Boogie { : base(ideSeq) {
Contract.Requires(ideSeq != null);
}
- public new IdentifierExpr/*!*/ this[int index] {
- get {
- Contract.Ensures(Contract.Result<IdentifierExpr>() != null);
-
- return cce.NonNull((IdentifierExpr)base[index]);
- }
- set {
- base[index] = value;
- }
- }
-
- public void Emit(TokenTextWriter stream, bool printWhereComments) {
- Contract.Requires(stream != null);
- string sep = "";
- foreach (IdentifierExpr/*!*/ e in this) {
- Contract.Assert(e != null);
- stream.Write(sep);
- sep = ", ";
- e.Emit(stream);
- if (printWhereComments && e.Decl != null && e.Decl.TypedIdent.WhereExpr != null) {
- stream.Write(" /* where ");
- e.Decl.TypedIdent.WhereExpr.Emit(stream);
- stream.Write(" */");
- }
- }
- }
}
@@ -3464,6 +3388,58 @@ namespace Microsoft.Boogie { }
}
+ public static void Emit(this IdentifierExprSeq ids, TokenTextWriter stream, bool printWhereComments) {
+ Contract.Requires(stream != null);
+ string sep = "";
+ foreach (IdentifierExpr/*!*/ e in ids) {
+ Contract.Assert(e != null);
+ stream.Write(sep);
+ sep = ", ";
+ e.Emit(stream);
+
+ if (printWhereComments && e.Decl != null && e.Decl.TypedIdent.WhereExpr != null) {
+ stream.Write(" /* where ");
+ e.Decl.TypedIdent.WhereExpr.Emit(stream);
+ stream.Write(" */");
+ }
+ }
+ }
+
+ public static void Emit(this VariableSeq vs, TokenTextWriter stream, bool emitAttributes) {
+ Contract.Requires(stream != null);
+ string sep = "";
+ foreach (Variable/*!*/ v in vs) {
+ Contract.Assert(v != null);
+ stream.Write(sep);
+ sep = ", ";
+ v.EmitVitals(stream, 0, emitAttributes);
+ }
+ }
+
+ public static void Emit(this TypeSeq tys, TokenTextWriter stream, string separator) {
+ Contract.Requires(separator != null);
+ Contract.Requires(stream != null);
+ string sep = "";
+ foreach (Type/*!*/ v in tys) {
+ Contract.Assert(v != null);
+ stream.Write(sep);
+ sep = separator;
+ v.Emit(stream);
+ }
+ }
+
+ public static void Emit(this TypeVariableSeq tvs, TokenTextWriter stream, string separator) {
+ Contract.Requires(separator != null);
+ Contract.Requires(stream != null);
+ string sep = "";
+ foreach (TypeVariable/*!*/ v in tvs) {
+ Contract.Assert(v != null);
+ stream.Write(sep);
+ sep = separator;
+ v.Emit(stream);
+ }
+ }
+
}
#endregion
diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index e4390634..1eb2ccc8 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -1902,20 +1902,20 @@ namespace Microsoft.Boogie { // (a similar check is in CheckArgumentTypes, but we are not
// able to call this method because it cannot cope with Ins/Outs
// that are null)
- if (Ins.Count != Proc.InParams.Length) {
+ if (Ins.Count != Proc.InParams.Count) {
rc.Error(this.tok,
"wrong number of arguments in call to {0}: {1}",
callee, Ins.Count);
return;
}
- if (Outs.Count != Proc.OutParams.Length) {
+ if (Outs.Count != Proc.OutParams.Count) {
rc.Error(this.tok,
"wrong number of result variables in call to {0}: {1}",
callee, Outs.Count);
return;
}
if (IsAsync) {
- if (Proc.OutParams.Length > 0) {
+ if (Proc.OutParams.Count > 0) {
rc.Error(this.tok, "a procedure called asynchronously can have no output parameters");
return;
}
@@ -2060,7 +2060,7 @@ namespace Microsoft.Boogie { VariableSeq/*!*/ cins = new VariableSeq();
VariableSeq wildcardVars = new VariableSeq();
Contract.Assume(this.Proc != null);
- for (int i = 0; i < this.Proc.InParams.Length; ++i) {
+ for (int i = 0; i < this.Proc.InParams.Count; ++i) {
Variable/*!*/ param = cce.NonNull(this.Proc.InParams[i]);
bool isWildcard = this.Ins[i] == null;
@@ -2105,7 +2105,7 @@ namespace Microsoft.Boogie { #region assert (exists wildcardVars :: Pre[ins := cins])
Substitution s = Substituter.SubstitutionFromHashtable(substMapBound);
- bool hasWildcard = (wildcardVars.Length != 0);
+ bool hasWildcard = (wildcardVars.Count != 0);
Expr preConjunction = null;
for (int i = 0; i < this.Proc.Requires.Count; i++) {
Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]);
@@ -2176,7 +2176,7 @@ namespace Microsoft.Boogie { #endregion
#region Create couts
VariableSeq/*!*/ couts = new VariableSeq();
- for (int i = 0; i < this.Proc.OutParams.Length; ++i) {
+ for (int i = 0; i < this.Proc.OutParams.Count; ++i) {
Variable/*!*/ param = cce.NonNull(this.Proc.OutParams[i]);
bool isWildcard = this.Outs[i] == null;
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index fd09cd20..e5d955d2 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -14,6 +14,7 @@ namespace Microsoft.Boogie { using System.Collections.Generic;
using Microsoft.Boogie.AbstractInterpretation;
using System.Diagnostics.Contracts;
+ using System.Linq;
using Microsoft.Basetypes;
using Set = GSet<object>; // not that the set used is not a set of Variable only, as it also contains TypeVariables
@@ -1787,7 +1788,7 @@ namespace Microsoft.Boogie { public virtual int ArgumentCount {
get {
Contract.Assume(Func != null); // ArgumentCount requires object to be properly resolved.
- return Func.InParams.Length;
+ return Func.InParams.Count;
}
}
public virtual Type Typecheck(ref ExprSeq actuals, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
@@ -1796,16 +1797,16 @@ 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.Count == Func.InParams.Length);
- Contract.Assume(Func.OutParams.Length == 1);
+ Contract.Assume(actuals.Count == Func.InParams.Count);
+ Contract.Assume(Func.OutParams.Count == 1);
List<Type/*!*/>/*!*/ resultingTypeArgs;
TypeSeq actualResultType =
Type.CheckArgumentTypes(Func.TypeParameters,
out resultingTypeArgs,
- Func.InParams.ToTypeSeq,
+ new TypeSeq(Func.InParams.Select(Item => Item.TypedIdent.Type).ToArray()),
actuals,
- Func.OutParams.ToTypeSeq,
+ new TypeSeq(Func.OutParams.Select(Item => Item.TypedIdent.Type).ToArray()),
null,
// we need some token to report a possibly wrong number of
// arguments
@@ -2581,7 +2582,7 @@ namespace Microsoft.Boogie { int level = 0;
stream.WriteLine(level, "|{");
- if (this.LocVars.Length > 0) {
+ if (this.LocVars.Count > 0) {
stream.Write(level + 1, "var ");
this.LocVars.Emit(stream, true);
stream.WriteLine(";");
diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index a6382eb4..e42df50f 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -12,6 +12,7 @@ namespace Microsoft.Boogie { using System.Collections;
using System.Diagnostics;
using System.Collections.Generic;
+ using System.Linq;
using Microsoft.Boogie.AbstractInterpretation;
using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
@@ -65,7 +66,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Count > 0);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
TypeParameters = typeParameters;
Dummies = dummies;
Attributes = kv;
@@ -159,7 +160,7 @@ namespace Microsoft.Boogie { rc.PopVarContext();
// establish a canonical order of the type parameters
- this.TypeParameters = Type.SortTypeParams(TypeParameters, Dummies.ToTypeSeq, null);
+ this.TypeParameters = Type.SortTypeParams(TypeParameters, new TypeSeq(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()), null);
} finally {
rc.TypeBinderState = previousTypeBinderState;
@@ -192,7 +193,7 @@ namespace Microsoft.Boogie { protected TypeVariableSeq GetUnmentionedTypeParameters() {
Contract.Ensures(Contract.Result<TypeVariableSeq>() != null);
- TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(Dummies.ToTypeSeq);
+ TypeVariableSeq/*!*/ dummyParameters = Type.FreeVariablesIn(new TypeSeq(Dummies.Select(Item => Item.TypedIdent.Type).ToArray()));
Contract.Assert(dummyParameters != null);
TypeVariableSeq/*!*/ unmentionedParameters = new TypeVariableSeq();
foreach (TypeVariable/*!*/ var in TypeParameters) {
@@ -427,21 +428,21 @@ namespace Microsoft.Boogie { Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParams.Count > 0);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
}
public ForallExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public ForallExpr(IToken tok, VariableSeq dummies, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public ForallExpr(IToken tok, TypeVariableSeq typeParams, VariableSeq dummies, Expr body)
: base(tok, typeParams, dummies, null, null, body) {
@@ -449,7 +450,7 @@ namespace Microsoft.Boogie { Contract.Requires(dummies != null);
Contract.Requires(typeParams != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length + typeParams.Count > 0);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -473,21 +474,21 @@ namespace Microsoft.Boogie { Contract.Requires(typeParams != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParams.Count > 0);
+ Contract.Requires(dummies.Count + typeParams.Count > 0);
}
public ExistsExpr(IToken tok, VariableSeq dummies, Trigger triggers, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, triggers, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public ExistsExpr(IToken tok, VariableSeq dummies, Expr body)
: base(tok, new TypeVariableSeq(), dummies, null, null, body) {
Contract.Requires(body != null);
Contract.Requires(dummies != null);
Contract.Requires(tok != null);
- Contract.Requires(dummies.Length > 0);
+ Contract.Requires(dummies.Count > 0);
}
public override Absy StdDispatch(StandardVisitor visitor) {
@@ -521,7 +522,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Count > 0);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
Contract.Assert((this is ForallExpr) || (this is ExistsExpr));
@@ -702,7 +703,7 @@ namespace Microsoft.Boogie { Contract.Requires(typeParameters != null);
Contract.Requires(dummies != null);
Contract.Requires(body != null);
- Contract.Requires(dummies.Length + typeParameters.Count > 0);
+ Contract.Requires(dummies.Count + typeParameters.Count > 0);
}
public override BinderKind Kind {
diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs index fd258399..8b35ffcb 100644 --- a/Source/Core/BitvectorAnalysis.cs +++ b/Source/Core/BitvectorAnalysis.cs @@ -190,12 +190,12 @@ namespace Microsoft.Boogie { }
public override Implementation VisitImplementation(Implementation node) {
- for (int i = 0; i < node.InParams.Length; i++) {
+ for (int i = 0; i < node.InParams.Count; i++) {
DisjointSet a = MakeDisjointSet(node.InParams[i]);
DisjointSet b = MakeDisjointSet(node.Proc.InParams[i]);
a.Union(b);
}
- for (int i = 0; i < node.OutParams.Length; i++) {
+ for (int i = 0; i < node.OutParams.Count; i++) {
DisjointSet a = MakeDisjointSet(node.OutParams[i]);
DisjointSet b = MakeDisjointSet(node.Proc.OutParams[i]);
a.Union(b);
diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 2996514f..5263fd1f 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -339,7 +339,7 @@ namespace Microsoft.Boogie { substMap.Add(locVar, ie);
}
- for (int i = 0; i < impl.InParams.Length; i++) {
+ for (int i = 0; i < impl.InParams.Count; i++) {
Variable inVar = cce.NonNull(impl.InParams[i]);
LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, inVar.Name), inVar.TypedIdent.Type, inVar.TypedIdent.WhereExpr));
newLocalVars.Add(localVar);
@@ -352,7 +352,7 @@ namespace Microsoft.Boogie { }
}
- for (int i = 0; i < impl.OutParams.Length; i++) {
+ for (int i = 0; i < impl.OutParams.Count; i++) {
Variable outVar = cce.NonNull(impl.OutParams[i]);
LocalVariable localVar = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, GetProcVarName(proc.Name, outVar.Name), outVar.TypedIdent.Type, outVar.TypedIdent.WhereExpr));
newLocalVars.Add(localVar);
@@ -445,7 +445,7 @@ namespace Microsoft.Boogie { CmdSeq inCmds = new CmdSeq();
// assign in parameters
- for (int i = 0; i < impl.InParams.Length; ++i) {
+ for (int i = 0; i < impl.InParams.Count; ++i) {
Cmd cmd = Cmd.SimpleAssign(impl.tok,
(IdentifierExpr)cce.NonNull(codeCopier.Subst)(cce.NonNull(impl.InParams[i])),
cce.NonNull(callCmd.Ins[i]));
@@ -476,7 +476,7 @@ namespace Microsoft.Boogie { }
// add where clauses of local vars as assume
- for (int i = 0; i < locVars.Length; ++i) {
+ for (int i = 0; i < locVars.Count; ++i) {
Expr whereExpr = (cce.NonNull(locVars[i])).TypedIdent.WhereExpr;
if (whereExpr != null) {
whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);
@@ -489,7 +489,7 @@ namespace Microsoft.Boogie { }
// add where clauses of output params as assume
- for (int i = 0; i < impl.OutParams.Length; ++i) {
+ for (int i = 0; i < impl.OutParams.Count; ++i) {
Expr whereExpr = (cce.NonNull(impl.OutParams[i])).TypedIdent.WhereExpr;
if (whereExpr != null) {
whereExpr = Substituter.Apply(codeCopier.Subst, whereExpr);
@@ -535,7 +535,7 @@ namespace Microsoft.Boogie { }
// assign out params
- for (int i = 0; i < impl.OutParams.Length; ++i) {
+ for (int i = 0; i < impl.OutParams.Count; ++i) {
Expr/*!*/ cout_exp = (IdentifierExpr)cce.NonNull(codeCopier.Subst(cce.NonNull(impl.OutParams[i])));
Cmd cmd = Cmd.SimpleAssign(impl.tok, cce.NonNull(callCmd.Outs[i]), cout_exp);
outCmds.Add(cmd);
diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index bed2626f..a20d8ce9 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -62,7 +62,7 @@ namespace Microsoft.Boogie public override Implementation VisitImplementation(Implementation node)
{
HashSet<Variable> start = new HashSet<Variable>();
- for (int i = 0; i < node.InParams.Length; i++)
+ for (int i = 0; i < node.InParams.Count; i++)
{
string domainName = FindDomainName(node.Proc.InParams[i]);
if (domainName != null)
@@ -71,7 +71,7 @@ namespace Microsoft.Boogie start.Add(node.InParams[i]);
}
}
- for (int i = 0; i < node.OutParams.Length; i++)
+ for (int i = 0; i < node.OutParams.Count; i++)
{
string domainName = FindDomainName(node.Proc.OutParams[i]);
if (domainName != null)
@@ -296,7 +296,7 @@ namespace Microsoft.Boogie public override Cmd VisitCallCmd(CallCmd node)
{
HashSet<Variable> inVars = new HashSet<Variable>();
- for (int i = 0; i < node.Proc.InParams.Length; i++)
+ for (int i = 0; i < node.Proc.InParams.Count; i++)
{
Variable formal = node.Proc.InParams[i];
string domainName = FindDomainName(formal);
@@ -331,7 +331,7 @@ namespace Microsoft.Boogie inVars.Add(actual.Decl);
parallelCallInvars.Add(actual.Decl);
}
- for (int i = 0; i < node.Proc.OutParams.Length; i++)
+ for (int i = 0; i < node.Proc.OutParams.Count; i++)
{
IdentifierExpr actual = node.Outs[i];
string actualDomainName = FindDomainName(actual.Decl);
diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index beed64c8..bee34156 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -329,7 +329,7 @@ namespace Microsoft.Boogie {
locals.Add(ie.Decl);
}
- for (int i = 0; i < decl.InParams.Length - linearTypechecker.linearDomains.Count; i++)
+ for (int i = 0; i < decl.InParams.Count - linearTypechecker.linearDomains.Count; i++)
{
Variable inParam = decl.InParams[i];
Variable copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, inParam.Name, inParam.TypedIdent.Type));
@@ -337,7 +337,7 @@ namespace Microsoft.Boogie map[decl.InParams[i]] = new IdentifierExpr(Token.NoToken, copy);
}
{
- int i = decl.InParams.Length - linearTypechecker.linearDomains.Count;
+ int i = decl.InParams.Count - linearTypechecker.linearDomains.Count;
foreach (string domainName in linearTypechecker.linearDomains.Keys)
{
Variable inParam = decl.InParams[i];
@@ -347,7 +347,7 @@ namespace Microsoft.Boogie i++;
}
}
- for (int i = 0; i < decl.OutParams.Length; i++)
+ for (int i = 0; i < decl.OutParams.Count; i++)
{
Variable outParam = decl.OutParams[i];
var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, outParam.Name, outParam.TypedIdent.Type));
@@ -439,7 +439,7 @@ namespace Microsoft.Boogie Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
Dictionary<string, Variable> domainNameToLocalVar = new Dictionary<string, Variable>();
{
- int i = impl.InParams.Length - linearTypechecker.linearDomains.Count;
+ int i = impl.InParams.Count - linearTypechecker.linearDomains.Count;
foreach (string domainName in linearTypechecker.linearDomains.Keys)
{
Variable inParam = impl.InParams[i];
@@ -590,7 +590,7 @@ namespace Microsoft.Boogie {
domainNameToExpr[domainName] = new IdentifierExpr(Token.NoToken, domainNameToInputVar[domainName]);
}
- for (int i = 0; i < impl.InParams.Length - linearTypechecker.linearDomains.Count; i++)
+ for (int i = 0; i < impl.InParams.Count - linearTypechecker.linearDomains.Count; i++)
{
Variable v = impl.InParams[i];
var domainName = linearTypechecker.FindDomainName(v);
@@ -627,7 +627,7 @@ namespace Microsoft.Boogie Dictionary<string, Variable> domainNameToInputVar = new Dictionary<string, Variable>();
{
- int i = proc.InParams.Length - linearTypechecker.linearDomains.Count;
+ int i = proc.InParams.Count - linearTypechecker.linearDomains.Count;
foreach (string domainName in linearTypechecker.linearDomains.Keys)
{
Variable inParam = proc.InParams[i];
@@ -653,7 +653,7 @@ namespace Microsoft.Boogie if (domainName == null) continue;
domainNameToScope[domainName].Add(v);
}
- for (int i = 0; i < proc.InParams.Length - linearTypechecker.linearDomains.Count; i++)
+ for (int i = 0; i < proc.InParams.Count - linearTypechecker.linearDomains.Count; i++)
{
Variable v = proc.InParams[i];
var domainName = linearTypechecker.FindDomainName(v);
@@ -692,7 +692,7 @@ namespace Microsoft.Boogie if (domainName == null) continue;
domainNameToScope[domainName].Add(v);
}
- for (int i = 0; i < proc.OutParams.Length; i++)
+ for (int i = 0; i < proc.OutParams.Count; i++)
{
Variable v = proc.OutParams[i];
var domainName = linearTypechecker.FindDomainName(v);
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index ed5b88ae..44d56045 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -390,7 +390,7 @@ private class BvBounds : Expr { }
if (!allUnnamed) {
Bpl.Type prevType = null;
- for (int i = arguments.Length; 0 <= --i; ) {
+ for (int i = arguments.Count; 0 <= --i; ) {
TypedIdent/*!*/ curr = cce.NonNull(arguments[i]).TypedIdent;
if (curr.HasName) {
// the argument was given as both an identifier and a type
@@ -1775,13 +1775,13 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
- if (typeParams.Count + ds.Length > 0)
+ if (typeParams.Count + ds.Count > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 89 || la.kind == 90) {
Exists();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
- if (typeParams.Count + ds.Length > 0)
+ if (typeParams.Count + ds.Count > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 91 || la.kind == 92) {
Lambda();
@@ -1789,7 +1789,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (trig != null)
SemErr("triggers not allowed in lambda expressions");
- if (typeParams.Count + ds.Length > 0)
+ if (typeParams.Count + ds.Count > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
} else SynErr(123);
Expect(10);
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 77d49f3e..8a38d67a 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -549,7 +549,7 @@ namespace Microsoft.Boogie { public virtual VariableSeq VisitVariableSeq(VariableSeq variableSeq) {
Contract.Requires(variableSeq != null);
Contract.Ensures(Contract.Result<VariableSeq>() != null);
- for (int i = 0, n = variableSeq.Length; i < n; i++)
+ for (int i = 0, n = variableSeq.Count; i < n; i++)
variableSeq[i] = this.VisitVariable(cce.NonNull(variableSeq[i]));
return variableSeq;
}
diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index ceef059e..321d4072 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -82,7 +82,7 @@ namespace Microsoft.Boogie.Houdini { // type check
existentialFunctions.Values.Iter(func =>
{
- if (func.OutParams.Length != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)
+ if (func.OutParams.Count != 1 || !func.OutParams[0].TypedIdent.Type.IsBool)
throw new AbsHoudiniInternalError(string.Format("Existential function {0} must return bool", func.Name));
if(func.Body != null)
throw new AbsHoudiniInternalError(string.Format("Existential function {0} should not have a body", func.Name));
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index f896c27f..b4408f03 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -265,7 +265,7 @@ namespace Microsoft.Boogie.Houdini { }
private CmdSeq InlineRequiresForCallCmd(CallCmd node) {
Dictionary<Variable, Expr> substMap = new Dictionary<Variable, Expr>();
- for (int i = 0; i < node.Proc.InParams.Length; i++) {
+ for (int i = 0; i < node.Proc.InParams.Count; i++) {
substMap.Add(node.Proc.InParams[i], node.Ins[i]);
}
Substitution substitution = Substituter.SubstitutionFromHashtable(substMap);
diff --git a/Source/Predication/UniformityAnalyser.cs b/Source/Predication/UniformityAnalyser.cs index ca5a0df6..a6287db5 100644 --- a/Source/Predication/UniformityAnalyser.cs +++ b/Source/Predication/UniformityAnalyser.cs @@ -338,7 +338,7 @@ namespace Microsoft.Boogie SetNonUniform(callCmd.callee);
}
}
- for (int i = 0; i < Callee.InParams.Length; i++)
+ for (int i = 0; i < Callee.InParams.Count; i++)
{
if (IsUniform(callCmd.callee, Callee.InParams[i].Name)
&& !IsUniform(impl.Name, callCmd.Ins[i]))
@@ -347,7 +347,7 @@ namespace Microsoft.Boogie }
}
- for (int i = 0; i < Callee.OutParams.Length; i++)
+ for (int i = 0; i < Callee.OutParams.Count; i++)
{
if (IsUniform(impl.Name, callCmd.Outs[i].Name)
&& !IsUniform(callCmd.callee, Callee.OutParams[i].Name))
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 7fffd6fc..4e94c238 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -273,7 +273,7 @@ namespace Microsoft.Boogie.SMTLib foreach (Function f in ctx.KnownDatatypeConstructors[datatype])
{
string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
- if (f.InParams.Length == 0)
+ if (f.InParams.Count == 0)
{
datatypeString += quotedConstructorName + " ";
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 2bbe4978..2bf8fa22 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -209,7 +209,7 @@ void ObjectInvariant() string printedName = Namer.GetQuotedName(f, f.Name);
Contract.Assert(printedName != null);
- Contract.Assert(f.OutParams.Length == 1);
+ Contract.Assert(f.OutParams.Count == 1);
var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");
string decl;
if(RegisteredRelations.Contains(op.Func))
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index a110c817..6509bc30 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -496,7 +496,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(vars != null);
// Check for a 'qid, name' pair in keyvalues
string qid = QKeyValue.FindStringAttribute(attributes, "qid");
- if (qid == null && vars.Length != 0) {
+ if (qid == null && vars.Count != 0) {
// generate default name (line:column position in .bpl file)
Variable v = vars[0];
Contract.Assert(v != null); // Rustan's claim!
@@ -1148,7 +1148,7 @@ namespace Microsoft.Boogie.VCExprAST { // first bind the formals to VCExpr variables, which are later
// substituted with the actual parameters
var inParams = app.Func.InParams;
- for (int i = 0; i < inParams.Length; ++i)
+ for (int i = 0; i < inParams.Count; ++i)
subst[BaseTranslator.BindVariable(inParams[i])] = args[i];
// recursively translate the body of the expansion
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 48bb3354..e6384e67 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -65,7 +65,7 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires(gen != null);
Contract.Requires(fun != null);
Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
- List<VCExprVar/*!*/>/*!*/ arguments = new List<VCExprVar/*!*/>(fun.InParams.Length);
+ List<VCExprVar/*!*/>/*!*/ arguments = new List<VCExprVar/*!*/>(fun.InParams.Count);
foreach (Formal/*!*/ f in fun.InParams) {
Contract.Assert(f != null);
VCExprVar/*!*/ var = gen.Variable(f.Name, f.TypedIdent.Type);
@@ -192,7 +192,7 @@ namespace Microsoft.Boogie.TypeErasure { public TypeCtorRepr(Function ctor, List<Function/*!*/>/*!*/ dtors) {
Contract.Requires(ctor != null);
Contract.Requires(cce.NonNullElements(dtors));
- Contract.Requires(ctor.InParams.Length == dtors.Count);
+ Contract.Requires(ctor.InParams.Count == dtors.Count);
this.Ctor = ctor;
this.Dtors = dtors;
}
@@ -283,7 +283,7 @@ namespace Microsoft.Boogie.TypeErasure { GenCtorAssignment(Gen.Function(typeRepr,
HelperFuns.ToVCExprList(quantifiedVars)));
- if (typeRepr.InParams.Length == 0)
+ if (typeRepr.InParams.Count == 0)
return eq;
return Gen.Forall(quantifiedVars, new List<VCTrigger/*!*/>(),
@@ -711,7 +711,7 @@ namespace Microsoft.Boogie.TypeErasure { public bool IsCast(Function fun) {
Contract.Requires(fun != null);
- if (fun.InParams.Length != 1)
+ if (fun.InParams.Count != 1)
return false;
Type/*!*/ inType = cce.NonNull(fun.InParams[0]).TypedIdent.Type;
if (inType.Equals(U)) {
diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index 79a3286b..8e4bc7ab 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -104,15 +104,15 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<Function>() != null);
Function res;
if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
- Contract.Assert(fun.OutParams.Length == 1);
+ Contract.Assert(fun.OutParams.Count == 1);
// if all of the parameters are int or bool, the function does
// not have to be changed
- if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
+ if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type)) {
res = fun;
} else {
- Type[]/*!*/ types = new Type[fun.TypeParameters.Count + fun.InParams.Length + 1];
+ Type[]/*!*/ types = new Type[fun.TypeParameters.Count + fun.InParams.Count + 1];
int i = 0;
// the first arguments are the explicit type parameters
@@ -285,13 +285,13 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); Contract.Requires(store != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;
+ int arity = select.InParams.Count - 1 - mapTypeParamNum - mapAbstractionVarNum;
List<VCExprVar/*!*/>/*!*/ types =
HelperFuns.VarVector("t", mapTypeParamNum + mapAbstractionVarNum,
AxBuilder.T, Gen);
List<Type/*!*/> indexTypes = new List<Type/*!*/>();
- for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++) {
+ for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Count; i++) {
indexTypes.Add(cce.NonNull(select.InParams[i]).TypedIdent.Type);
}
Contract.Assert(arity == indexTypes.Count);
@@ -330,7 +330,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); Contract.Requires(store != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- int arity = select.InParams.Length - 1 - mapTypeParamNum - mapAbstractionVarNum;
+ int arity = select.InParams.Count - 1 - mapTypeParamNum - mapAbstractionVarNum;
List<VCExprVar/*!*/>/*!*/ freeTypeVars =
HelperFuns.VarVector("u", mapAbstractionVarNum, AxBuilder.T, Gen);
@@ -346,7 +346,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); types1.AddRange(freeTypeVars);
List<Type/*!*/> indexTypes = new List<Type/*!*/>();
- for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Length; i++) {
+ for (int i = mapTypeParamNum + mapAbstractionVarNum + 1; i < select.InParams.Count; i++) {
indexTypes.Add(cce.NonNull(select.InParams[i]).TypedIdent.Type);
}
Contract.Assert(arity == indexTypes.Count);
@@ -673,7 +673,7 @@ Contract.Ensures(Contract.Result<VCExpr>() != null); Contract.Assert(t != null);
inferredTypeArgs.Add(t);}
- Contract.Assert(untypedOp.InParams.Length == inferredTypeArgs.Count + node.Arity);
+ Contract.Assert(untypedOp.InParams.Count == inferredTypeArgs.Count + node.Arity);
return new OpTypesPair (Gen.BoogieFunctionOp(untypedOp), inferredTypeArgs);
}
diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index d887a70f..ec2d47bd 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -370,11 +370,11 @@ namespace Microsoft.Boogie.TypeErasure Contract.Requires(fun != null);
UntypedFunction res;
if (!Typed2UntypedFunctions.TryGetValue(fun, out res)) {
- Contract.Assert(fun.OutParams.Length == 1);
+ Contract.Assert(fun.OutParams.Count == 1);
// if all of the parameters are int or bool, the function does
// not have to be changed
- if (Contract.ForAll(0, fun.InParams.Length, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
+ if (Contract.ForAll(0, fun.InParams.Count, f => UnchangedType(cce.NonNull(fun.InParams[f]).TypedIdent.Type)) &&
UnchangedType(cce.NonNull(fun.OutParams[0]).TypedIdent.Type) &&
fun.TypeParameters.Count == 0) {
res = new UntypedFunction(fun, new List<TypeVariable/*!*/>(), new List<TypeVariable/*!*/>());
@@ -388,13 +388,13 @@ namespace Microsoft.Boogie.TypeErasure List<TypeVariable/*!*/>/*!*/ implicitParams, explicitParams;
SeparateTypeParams(argTypes, fun.TypeParameters, out implicitParams, out explicitParams);
- Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Length + 1];
+ Type[]/*!*/ types = new Type[explicitParams.Count + fun.InParams.Count + 1];
int i = 0;
for (int j = 0; j < explicitParams.Count; ++j) {
types[i] = T;
i = i + 1;
}
- for (int j = 0; j < fun.InParams.Length; ++i, ++j)
+ for (int j = 0; j < fun.InParams.Count; ++i, ++j)
types[i] = TypeAfterErasure(cce.NonNull(fun.InParams[j]).TypedIdent.Type);
types[types.Length - 1] = TypeAfterErasure(cce.NonNull(fun.OutParams[0]).TypedIdent.Type);
@@ -414,7 +414,7 @@ namespace Microsoft.Boogie.TypeErasure private VCExpr GenFunctionAxiom(UntypedFunction fun, Function originalFun) {
Contract.Requires(originalFun != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/>(originalFun.InParams.Length);
+ List<Type/*!*/>/*!*/ originalInTypes = new List<Type/*!*/>(originalFun.InParams.Count);
foreach (Formal/*!*/ f in originalFun.InParams)
originalInTypes.Add(f.TypedIdent.Type);
@@ -433,7 +433,7 @@ namespace Microsoft.Boogie.TypeErasure Contract.Requires(cce.NonNullElements(explicitTypeParams));
Contract.Requires(cce.NonNullElements(originalInTypes));
Contract.Requires(originalResultType != null);
- Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Length);
+ Contract.Requires(originalInTypes.Count + explicitTypeParams.Count == fun.InParams.Count);
Contract.Ensures(Contract.Result<VCExpr>() != null);
if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.None) {
@@ -764,9 +764,9 @@ namespace Microsoft.Boogie.TypeErasure Contract.Requires(cce.NonNullElements(originalInTypes));
Contract.Requires(cce.NonNullElements(explicitTypeParamsSelect));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- int arity = store.InParams.Length - 2;
+ int arity = store.InParams.Count - 2;
List<VCExprVar/*!*/> inParams = new List<VCExprVar/*!*/>();
- List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Length);
+ List<VCExprVar/*!*/> quantifiedVars = new List<VCExprVar/*!*/>(store.InParams.Count);
VariableBindings bindings = new VariableBindings();
// bound variable: m
@@ -779,7 +779,7 @@ namespace Microsoft.Boogie.TypeErasure // bound variables: indexes
List<Type/*!*/> origIndexTypes = new List<Type/*!*/>(arity);
List<Type/*!*/> indexTypes = new List<Type/*!*/>(arity);
- for (int i = 1; i < store.InParams.Length - 1; i++) {
+ for (int i = 1; i < store.InParams.Count - 1; i++) {
origIndexTypes.Add(originalInTypes[i]);
indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);
}
@@ -856,10 +856,10 @@ namespace Microsoft.Boogie.TypeErasure Contract.Requires(select != null);
Contract.Requires(cce.NonNullElements(explicitSelectParams));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- int arity = store.InParams.Length - 2;
+ int arity = store.InParams.Count - 2;
List<Type/*!*/> indexTypes = new List<Type/*!*/>();
- for (int i = 1; i < store.InParams.Length - 1; i++) {
+ for (int i = 1; i < store.InParams.Count - 1; i++) {
indexTypes.Add(cce.NonNull(store.InParams[i]).TypedIdent.Type);
}
Contract.Assert(indexTypes.Count == arity);
@@ -1279,7 +1279,7 @@ namespace Microsoft.Boogie.TypeErasure List<int>/*!*/ explicitTypeParams =
AxBuilderPremisses.MapTypeAbstracterPremisses
.ExplicitSelectTypeParams(mapType);
- Contract.Assert(select.InParams.Length == explicitTypeParams.Count + node.Arity);
+ Contract.Assert(select.InParams.Count == explicitTypeParams.Count + node.Arity);
List<Type/*!*/>/*!*/ typeArgs = new List<Type/*!*/>(explicitTypeParams.Count);
foreach (int i in explicitTypeParams)
@@ -1309,7 +1309,7 @@ namespace Microsoft.Boogie.TypeErasure Function/*!*/ oriFun = ((VCExprBoogieFunctionOp)node.Op).Func;
Contract.Assert(oriFun != null);
UntypedFunction untypedFun = AxBuilderPremisses.Typed2Untyped(oriFun);
- Contract.Assert(untypedFun.Fun.InParams.Length ==
+ Contract.Assert(untypedFun.Fun.InParams.Count ==
untypedFun.ExplicitTypeParams.Count + node.Arity);
List<Type/*!*/>/*!*/ typeArgs =
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 90dcb2de..3961f096 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -1785,7 +1785,7 @@ namespace Microsoft.Boogie.VCExprAST { public override int Arity {
get {
- return Func.InParams.Length;
+ return Func.InParams.Count;
}
}
public override int TypeParamArity {
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index fe8d67f5..01366633 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -938,8 +938,8 @@ namespace VC { }
// where clauses of out-parameters
- Contract.Assert(impl.OutParams.Length == impl.Proc.OutParams.Length);
- for (int i = 0; i < impl.OutParams.Length; i++) {
+ Contract.Assert(impl.OutParams.Count == impl.Proc.OutParams.Count);
+ for (int i = 0; i < impl.OutParams.Count; i++) {
Variable f = cce.NonNull(impl.Proc.OutParams[i]);
if (f.TypedIdent.WhereExpr != null) {
Expr e = Substituter.Apply(formalProcImplSubst, f.TypedIdent.WhereExpr);
diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs index ac7ee9be..b4080e2c 100644 --- a/Source/VCGeneration/FixedpointVC.cs +++ b/Source/VCGeneration/FixedpointVC.cs @@ -643,7 +643,7 @@ namespace Microsoft.Boogie var proc = decl as Procedure;
if (proc == null) continue;
if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Length == 1);
+ Contract.Assert(proc.InParams.Count == 1);
// Make a new function
TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index c5d88c5c..5848e63b 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -326,7 +326,7 @@ namespace VC { var proc = decl as Procedure;
if (proc == null) continue;
if (!proc.Name.StartsWith(recordProcName)) continue;
- Contract.Assert(proc.InParams.Length == 1);
+ Contract.Assert(proc.InParams.Count == 1);
// Make a new function
TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 873a5589..eff8c2e2 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1240,7 +1240,7 @@ namespace VC { VCExpr startCorrect = VCGen.LetVC(codeExpr.Blocks[0], null, label2absy, blockVariables, bindings, ctx, out ac);
VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
- if (vcgen.CurrentLocalVariables.Length != 0)
+ if (vcgen.CurrentLocalVariables.Count != 0)
{
Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
List<VCExprVar> boundVars = new List<VCExprVar>();
|