diff options
author | Rustan Leino <leino@microsoft.com> | 2011-05-11 17:25:34 -0700 |
---|---|---|
committer | Rustan Leino <leino@microsoft.com> | 2011-05-11 17:25:34 -0700 |
commit | 27241e69516368f116baea922938d1cb10570d85 (patch) | |
tree | c4079369967b34e88de4b3921b3710b605baa18a /Source/Dafny | |
parent | dcaef29ffbe2570632e7368d27377fb9ac282d7b (diff) |
Dafny:
* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword)
* check that arrays are not null when accessed
* added dafny1/FindZero.dfy test case
Diffstat (limited to 'Source/Dafny')
-rw-r--r-- | Source/Dafny/Resolver.cs | 13 | ||||
-rw-r--r-- | Source/Dafny/Translator.cs | 3 |
2 files changed, 15 insertions, 1 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 22a58a39..ba28d531 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
@@ -2019,6 +2023,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;
@@ -2027,6 +2033,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
@@ -2047,6 +2055,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);
|