From afaeb081ffcc1c258db6eb7c34ba0b04c493919a Mon Sep 17 00:00:00 2001
From: Ally Donaldson <unknown>
Date: Mon, 22 Jul 2013 18:05:27 +0100
Subject: More refactoring towards replacing PureCollections.Sequence with List

---
 Source/Core/StandardVisitor.cs | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'Source/Core/StandardVisitor.cs')

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;
     }
-- 
cgit v1.2.3