Fix bug in translation of 'new' for arrays

3 files changed, 39 insertions, 5 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 402a070c..76da73cd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -9512,7 +9512,7 @@ namespace Microsoft.Dafny {
         // assume $nw != null && !$Heap[$nw, alloc] && dtype($nw) == RHS;

         Bpl.Expr nwNotNull = Bpl.Expr.Neq(nw, predef.Null);

         Bpl.Expr rightType;

-        rightType = etran.GoodRef_(tok, nw, tRhs.EType, true);

+        rightType = etran.GoodRef_(tok, nw, tRhs.Type, true);

         builder.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.And(nwNotNull, rightType)));

         if (tRhs.ArrayDimensions != null) {

           int i = 0;

diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy
index f6477708..391ca5f7 100644
--- a/Test/dafny0/Array.dfy
+++ b/Test/dafny0/Array.dfy
@@ -42,12 +42,12 @@ class A {
     assert zz2 != zz0;  // holds because zz2 is newly allocated

     var o: object := zz0;

     assert this != o;  // holds because zz0 has a different type

-    /******  This would be a good thing to be able to verify, but the current encoding is not up to the task

+

     if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) {

       o := zz1[1];

       assert zz0[1] == o ==> o == null;  // holds because zz0 and zz1 have different element types

     }

-    ******/

+

     assert zz2[20] == null;  // error: no reason that this must hold

   }

 

@@ -152,7 +152,7 @@ class A {
     ensures fresh(b) && Q1(b[..]);

 }

 

-type B;

+class B { }

 

 // -------------------------------

 

@@ -301,3 +301,29 @@ method AllocationBusiness2(a: array2<MyClass>, i: int, j: int)
   var c := new MyClass;

   assert c !in a[i,j].Repr;  // the proof requires allocation axioms for multi-dim arrays

 }

+

+// ------- a regression test, testing that dtype is set correctly after allocation ------

+

+module DtypeRegression {

+  predicate array_equal(a: array<int>, b: array<int>)

+    requires a != null && b != null;

+    reads a, b;

+  {

+    a[..] == b[..]

+  }

+

+  method duplicate_array(input: array<int>, len: int) returns (output: array<int>) 

+    requires input != null && len == input.Length;

+    ensures output != null && array_equal(input, output);

+  {

+    output := new int[len];

+    var i := 0;

+    while i < len

+      invariant 0 <= i <= len;

+      invariant forall j :: 0 <= j < i ==> output[j] == input[j];

+    {

+      output[i] := input[i];

+      i := i + 1;

+    }

+  }

+}

diff --git a/Test/dafny0/Array.dfy.expect b/Test/dafny0/Array.dfy.expect
index 081fd258..bf4da25f 100644
--- a/Test/dafny0/Array.dfy.expect
+++ b/Test/dafny0/Array.dfy.expect
@@ -13,6 +13,14 @@ Execution trace:
 Array.dfy(51,20): Error: assertion violation

 Execution trace:

     (0,0): anon0

+    (0,0): anon12_Then

+    (0,0): anon13_Then

+    (0,0): anon14_Then

+    (0,0): anon6

+    (0,0): anon15_Then

+    (0,0): anon16_Then

+    (0,0): anon9

+    (0,0): anon11

 Array.dfy(59,8): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

@@ -104,4 +112,4 @@ Execution trace:
     (0,0): anon2

     (0,0): anon6_Then

 

-Dafny program verifier finished with 46 verified, 20 errors

+Dafny program verifier finished with 49 verified, 20 errors