diff options
author | Ally Donaldson <unknown> | 2013-07-22 10:35:39 +0100 |
---|---|---|
committer | Ally Donaldson <unknown> | 2013-07-22 10:35:39 +0100 |
commit | 8547ab2737f6bcb185398e4cbc3edde3847cb085 (patch) | |
tree | 9d9f2aa2866d2ef38425c53899706fe47e5ea08f /Source/Core/StandardVisitor.cs | |
parent | cd8e597689abb89e64454cc042a2f28619ea44f4 (diff) |
Requires/EnsuresSeq replaced by List<Requires/Ensures>
Diffstat (limited to 'Source/Core/StandardVisitor.cs')
-rw-r--r-- | Source/Core/StandardVisitor.cs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index ee873bd4..800a5494 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -248,10 +248,10 @@ namespace Microsoft.Boogie { @requires.Condition = this.VisitExpr(@requires.Condition);
return @requires;
}
- public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) {
+ public virtual List<Requires> VisitRequiresSeq(List<Requires> requiresSeq) {
Contract.Requires(requiresSeq != null);
- Contract.Ensures(Contract.Result<RequiresSeq>() != null);
- for (int i = 0, n = requiresSeq.Length; i < n; i++)
+ Contract.Ensures(Contract.Result<List<Requires>>() != null);
+ for (int i = 0, n = requiresSeq.Count; i < n; i++)
requiresSeq[i] = this.VisitRequires(requiresSeq[i]);
return requiresSeq;
}
@@ -261,10 +261,10 @@ namespace Microsoft.Boogie { @ensures.Condition = this.VisitExpr(@ensures.Condition);
return @ensures;
}
- public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) {
+ public virtual List<Ensures> VisitEnsuresSeq(List<Ensures> ensuresSeq) {
Contract.Requires(ensuresSeq != null);
- Contract.Ensures(Contract.Result<EnsuresSeq>() != null);
- for (int i = 0, n = ensuresSeq.Length; i < n; i++)
+ Contract.Ensures(Contract.Result<List<Ensures>>() != null);
+ for (int i = 0, n = ensuresSeq.Count; i < n; i++)
ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]);
return ensuresSeq;
}
|