diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 4 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 9 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 3 |
5 files changed, 24 insertions, 9 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 8e999553..780d35ea 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -555,7 +555,7 @@ ReferenceType<out IToken/*!*/ tok, out Type/*!*/ ty> if (tok.val.Length != 5) {
dims = int.Parse(tok.val.Substring(5));
}
- ty = theBuiltIns.ArrayType(dims, gt[0], true);
+ ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
.)
| Ident<out tok> (. gt = new List<Type/*!*/>(); .)
[ GenericInstantiation<gt> ] (. ty = new UserDefinedType(tok, tok.val, gt); .)
@@ -808,7 +808,7 @@ AssignRhs<.out List<Expression> ee, out Type ty, out CallStmt initCall, Expressi [ "[" (. ee = new List<Expression>(); .)
Expressions<ee>
"]" (. // make sure an array class with this dimensionality exists
- UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
+ UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
.)
| "." Ident<out x>
"(" (. args = new List<Expression/*!*/>(); .)
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index d923e5dc..f76f24de 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -40,20 +40,21 @@ namespace Microsoft.Dafny { ClassDecl obj = new ClassDecl(Token.NoToken, "object", SystemModule, new List<TypeParameter>(), new List<MemberDecl>(), null);
SystemModule.TopLevelDecls.Add(obj);
// add one-dimensional arrays, since they may arise during type checking
- UserDefinedType tmp = ArrayType(1, Type.Int, true);
+ UserDefinedType tmp = ArrayType(Token.NoToken, 1, Type.Int, true);
}
public UserDefinedType ArrayType(int dims, Type arg) {
- return ArrayType(dims, arg, false);
+ return ArrayType(Token.NoToken, dims, arg, false);
}
- public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) {
+ public UserDefinedType ArrayType(IToken tok, int dims, Type arg, bool allowCreationOfNewClass) {
+ Contract.Requires(tok != null);
Contract.Requires(1 <= dims);
Contract.Requires(arg != null);
Contract.Ensures(Contract.Result<UserDefinedType>() != null);
List<Type/*!*/> typeArgs = new List<Type/*!*/>();
typeArgs.Add(arg);
- UserDefinedType udt = new UserDefinedType(Token.NoToken, ArrayClassName(dims), typeArgs);
+ UserDefinedType udt = new UserDefinedType(tok, ArrayClassName(dims), typeArgs);
if (allowCreationOfNewClass && !arrayTypeDecls.ContainsKey(dims)) {
ArrayClassDecl arrayClass = new ArrayClassDecl(dims, SystemModule);
for (int d = 0; d < dims; d++) {
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index db33283b..26cb7fbb 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -877,7 +877,7 @@ List<Expression/*!*/>/*!*/ decreases) { if (tok.val.Length != 5) {
dims = int.Parse(tok.val.Substring(5));
}
- ty = theBuiltIns.ArrayType(dims, gt[0], true);
+ ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);
} else if (la.kind == 1) {
Ident(out tok);
@@ -1419,7 +1419,7 @@ List<Expression/*!*/>/*!*/ decreases) { ee = new List<Expression>();
Expressions(ee);
Expect(53);
- UserDefinedType tmp = theBuiltIns.ArrayType(ee.Count, new IntType(), true);
+ UserDefinedType tmp = theBuiltIns.ArrayType(x, ee.Count, new IntType(), true);
} else {
Get();
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 00cabd1d..37b80894 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -837,7 +837,11 @@ namespace Microsoft.Dafny { #if !NO_CHEAP_OBJECT_WORKAROUND
if (a is ObjectType || b is ObjectType) { // TODO: remove this temporary hack
- // allow anything with object; this is BOGUS
+ var other = a is ObjectType ? b : a;
+ if (other is BoolType || other is IntType || other is SetType || other is SeqType || other.IsDatatype) {
+ return false;
+ }
+ // allow anything else with object; this is BOGUS
return true;
}
#endif
@@ -2022,6 +2026,8 @@ namespace Microsoft.Dafny { OldExpr e = (OldExpr)expr;
if (!twoState) {
Error(expr, "old expressions are not allowed in this context");
+ } else if (!specContext) {
+ Error(expr, "old expressions are allowed only in specification and ghost contexts");
}
ResolveExpression(e.E, twoState, specContext);
expr.Type = e.E.Type;
@@ -2030,6 +2036,8 @@ namespace Microsoft.Dafny { FreshExpr e = (FreshExpr)expr;
if (!twoState) {
Error(expr, "fresh expressions are not allowed in this context");
+ } else if (!specContext) {
+ Error(expr, "fresh expressions are allowed only in specification and ghost contexts");
}
ResolveExpression(e.E, twoState, specContext);
// the type of e.E must be either an object or a collection of objects
@@ -2050,6 +2058,9 @@ namespace Microsoft.Dafny { } else if (expr is AllocatedExpr) {
AllocatedExpr e = (AllocatedExpr)expr;
ResolveExpression(e.E, twoState, specContext);
+ if (!specContext) {
+ Error(expr, "allocated expressions are allowed only in specification and ghost contexts");
+ }
// e.E can be of any type
expr.Type = Type.Bool;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 2bb5a51e..557fcaf0 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1785,6 +1785,9 @@ namespace Microsoft.Dafny { bool isSequence = e.Seq.Type is SeqType;
CheckWellformed(e.Seq, options, locals, builder, etran);
Bpl.Expr seq = etran.TrExpr(e.Seq);
+ if (e.Seq.Type.IsArrayType) {
+ builder.Add(Assert(e.Seq.tok, Bpl.Expr.Neq(seq, predef.Null), "array may be null"));
+ }
Bpl.Expr e0 = null;
if (e.E0 != null) {
e0 = etran.TrExpr(e.E0);
|