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

1 files changed, 12 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;