From 7cc9a11d13a1d43d6e7beb4f874bb086f73804c4 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 11 Nov 2015 17:36:24 -0800
Subject: Fixed compilation of equality between reference types

---
 Test/dafny0/Compilation.dfy        | 55 +++++++++++++++++++++++++++++++++++++-
 Test/dafny0/Compilation.dfy.expect |  6 ++++-
 2 files changed, 59 insertions(+), 2 deletions(-)

(limited to 'Test')

diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 7f9169da..965f0787 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -45,7 +45,7 @@ module CoRecursion {
   //   42
   //   9
   //   9
-  method Main() {
+  method TestMain() {
     var m := 17;
     var cell := new Cell;
     cell.data := 40;
@@ -260,3 +260,56 @@ class DigitUnderscore_Names {
     this.10 := 20;
   }
 }
+
+// ------------------------------------------------------------------
+
+method Main()
+{
+  CoRecursion.TestMain();
+  EqualityTests.TestMain();
+}
+
+// ------------------------------------------------------------------
+
+module EqualityTests {
+  class C<T> {
+  }
+
+  method TestMain()
+  {
+    // regression tests:
+    var a: C<int>, b: C<int> := null, null;
+    if a == null {
+      print "a is null\n";
+    }
+    if a != null {
+      print "a is not null\n";
+    }
+    if a == b {
+      print "a and b are equal\n";
+    }
+    if a != b {
+      print "a and b are not equal\n";
+    }
+
+    var H := new real[10];
+    ArrayTests(H);
+  }
+
+  method ArrayTests<T>(H: array<T>)
+  {
+    var G := new int[10];
+    if G == H {  // this comparison is allowed in Dafny, but requires a cast in C#
+      print "this would be highly suspicious\n";
+    }
+    if G != H {  // this comparison is allowed in Dafny, but requires a cast in C#
+      print "good world order\n";
+    }
+    if null == H {
+      print "given array is null\n";
+    }
+    if null != H {
+      print "given array is non-null\n";
+    }
+  }
+}
diff --git a/Test/dafny0/Compilation.dfy.expect b/Test/dafny0/Compilation.dfy.expect
index 2b76b107..0a934a63 100644
--- a/Test/dafny0/Compilation.dfy.expect
+++ b/Test/dafny0/Compilation.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 50 verified, 0 errors
+Dafny program verifier finished with 56 verified, 0 errors
 Program compiled successfully
 Running...
 
@@ -10,3 +10,7 @@ Running...
 42
 9
 9
+a is null
+a and b are equal
+good world order
+given array is non-null
-- 
cgit v1.2.3