diff options
Diffstat (limited to 'Source/Dafny/Resolver.cs')
| -rw-r--r-- | Source/Dafny/Resolver.cs | 18 |
1 files changed, 2 insertions, 16 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 0761d865..b131912c 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -763,10 +763,6 @@ namespace Microsoft.Dafny var e = (FreshExpr)expr;
return new FreshExpr((e.tok), CloneExpr(e.E));
- } else if (expr is AllocatedExpr) {
- var e = (AllocatedExpr)expr;
- return new AllocatedExpr((e.tok), CloneExpr(e.E));
-
} else if (expr is UnaryExpr) {
var e = (UnaryExpr)expr;
return new UnaryExpr((e.tok), e.Op, CloneExpr(e.E));
@@ -3912,17 +3908,13 @@ namespace Microsoft.Dafny // fine
} else if (UserDefinedType.DenotesClass(t) != null) {
// fine
+ } else if (t.IsDatatype) {
+ // fine, treat this as the datatype itself.
} else {
Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);
}
expr.Type = Type.Bool;
- } else if (expr is AllocatedExpr) {
- AllocatedExpr e = (AllocatedExpr)expr;
- ResolveExpression(e.E, twoState);
- // e.E can be of any type
- expr.Type = Type.Bool;
-
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
ResolveExpression(e.E, twoState);
@@ -4522,10 +4514,6 @@ namespace Microsoft.Dafny Error(expr, "fresh expressions are allowed only in specification and ghost contexts");
return;
- } else if (expr is AllocatedExpr) {
- Error(expr, "allocated expressions are allowed only in specification and ghost contexts");
- return;
-
} else if (expr is PredicateExpr) {
var e = (PredicateExpr)expr;
// ignore the guard
@@ -5587,8 +5575,6 @@ namespace Microsoft.Dafny return UsesSpecFeatures(e.E);
} else if (expr is FreshExpr) {
return true;
- } else if (expr is AllocatedExpr) {
- return true;
} else if (expr is UnaryExpr) {
UnaryExpr e = (UnaryExpr)expr;
return UsesSpecFeatures(e.E);
|