diff options
Diffstat (limited to 'Source/Core/Parser.cs')
| -rw-r--r-- | Source/Core/Parser.cs | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 95c46934..7bd21d02 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -403,7 +403,7 @@ private class BvBounds : Expr { }
Bpl.Type ty = curr.Type;
var uti = ty as UnresolvedTypeIdentifier;
- if (uti != null && uti.Arguments.Length == 0) {
+ if (uti != null && uti.Arguments.Count == 0) {
// the given "thing" was just an identifier, so let's use it as the name of the parameter
curr.Name = uti.Name;
curr.Type = prevType;
@@ -470,9 +470,9 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x;
TypeVariableSeq/*!*/ typeParams;
VariableSeq/*!*/ ins, outs;
- RequiresSeq/*!*/ pre = new RequiresSeq();
+ List<Requires>/*!*/ pre = new List<Requires>();
IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq();
- EnsuresSeq/*!*/ post = new EnsuresSeq();
+ List<Ensures>/*!*/ post = new List<Ensures>();
VariableSeq/*!*/ locals = new VariableSeq();
StmtList/*!*/ stmtList;
@@ -798,7 +798,7 @@ private class BvBounds : Expr { if (la.kind == 11) {
Get();
var uti = ty as UnresolvedTypeIdentifier;
- if (uti != null && uti.Arguments.Length == 0) {
+ if (uti != null && uti.Arguments.Count == 0) {
varName = uti.Name;
} else {
this.SemErr("expected identifier before ':'");
@@ -867,7 +867,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
}
- void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) {
+ void Spec(List<Requires>/*!*/ pre, IdentifierExprSeq/*!*/ mods, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms;
if (la.kind == 34) {
Get();
@@ -897,7 +897,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StmtList(out stmtList);
}
- void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) {
+ void SpecPrePost(bool free, List<Requires>/*!*/ pre, List<Ensures>/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
if (la.kind == 36) {
Get();
|