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

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);