Merge

11 files changed, 81 insertions, 14 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);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 0ee81392..4bdea760 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -490,9 +490,12 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela
 Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)

 Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)

 Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context

-Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context

-10 resolution/type errors detected in Modules0.dfy

+Modules0.dfy(130,11): Error: old expressions are allowed only in specification and ghost contexts

+Modules0.dfy(131,11): Error: fresh expressions are allowed only in specification and ghost contexts

+Modules0.dfy(132,11): Error: allocated expressions are allowed only in specification and ghost contexts

+Modules0.dfy(148,10): Error: match source expression 'tree' has already been used as a match source expression in this context

+Modules0.dfy(187,12): Error: match source expression 'l' has already been used as a match source expression in this context

+13 resolution/type errors detected in Modules0.dfy

 

 -------------------- Modules1.dfy --------------------

 Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0

diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy
index adce71a8..59052ac2 100644
--- a/Test/dafny0/Modules0.dfy
+++ b/Test/dafny0/Modules0.dfy
@@ -121,6 +121,21 @@ class Ghosty {
   ghost method Theorem(a: int) { }

 }

 

+var SomeField: int;

+

+method SpecialFunctions()

+  modifies this;

+{

+  SomeField := SomeField + 4;

+  var a := old(SomeField);  // error: old can only be used in ghost contexts

+  var b := fresh(this);  // error: fresh can only be used in ghost contexts

+  var c := allocated(this);  // error: allocated can only be used in ghost contexts

+  if (fresh(this)) {  // this guard makes the if statement a ghost statement

+    ghost var x := old(SomeField);  // this is a ghost context, so it's okay

+    ghost var y := allocated(this);  // this is a ghost context, so it's okay

+  }

+}

+

 // ---------------------- illegal match expressions ---------------

 

 datatype Tree { Nil; Cons(int, Tree, Tree); }

diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy
index 93bd4b65..6b7ce9b9 100644
--- a/Test/dafny0/NatTypes.dfy
+++ b/Test/dafny0/NatTypes.dfy
@@ -60,7 +60,7 @@ datatype List<T> {
   Cons(nat, T, List<T>);

 }

 

-method MatchIt(list: List<bool>) returns (k: nat)

+method MatchIt(list: List<object>) returns (k: nat)

 {

   match (list) {

     case Nil =>

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index d96e12a5..d0eba7cb 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -59,6 +59,10 @@ Dafny program verifier finished with 2 verified, 0 errors
 

 Dafny program verifier finished with 17 verified, 0 errors

 

+-------------------- FindZero.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

 -------------------- TerminationDemos.dfy --------------------

 

 Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
new file mode 100644
index 00000000..cff8b934
--- /dev/null
+++ b/Test/dafny1/FindZero.dfy
@@ -0,0 +1,30 @@
+method FindZero(a: array<int>) returns (r: int)

+  requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];

+  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  ensures 0 <= r ==> r < a.Length && a[r] == 0;

+  ensures r < 0 ==> forall i :: 0 <= i && i < a.Length ==> a[i] != 0;

+{

+  var n := 0;

+  while (n < a.Length)

+    invariant forall i :: 0 <= i && i < n && i < a.Length ==> a[i] != 0;

+  {

+    if (a[n] == 0) { r := n; return; }

+    call Lemma(a, n, a[n]);

+    n := n + a[n];

+  }

+  r := -1;

+}

+

+ghost method Lemma(a: array<int>, k: int, m: int)

+  requires a != null && forall i :: 0 <= i && i < a.Length ==> 0 <= a[i];

+  requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

+  requires 0 <= k;

+  requires k < a.Length ==> m <= a[k];

+  ensures forall i :: k <= i && i < k+m && i < a.Length ==> a[i] != 0;

+  decreases m;

+{

+  if (0 < m && k < a.Length) {

+    assert a[k] != 0;

+    call Lemma(a, k+1, m-1);

+  }

+}

diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat
index 36b93883..57ac97e3 100644
--- a/Test/dafny1/runtest.bat
+++ b/Test/dafny1/runtest.bat
@@ -19,7 +19,7 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy
             ListCopy.dfy ListReverse.dfy ListContents.dfy

             MatrixFun.dfy pow2.dfy

             SchorrWaite.dfy

-            Cubes.dfy SumOfCubes.dfy

+            Cubes.dfy SumOfCubes.dfy FindZero.dfy

             TerminationDemos.dfy Substitution.dfy TreeDatatype.dfy KatzManna.dfy

             Induction.dfy Rippling.dfy

             Celebrity.dfy