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

---
 Source/Dafny/Compiler.cs           | 14 +++++-----
 Test/dafny0/Compilation.dfy        | 55 +++++++++++++++++++++++++++++++++++++-
 Test/dafny0/Compilation.dfy.expect |  6 ++++-
 3 files changed, 66 insertions(+), 9 deletions(-)

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index f992d6c0..2786133e 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -2637,27 +2637,27 @@ namespace Microsoft.Dafny {
             opString = "&&";  break;
 
           case BinaryExpr.ResolvedOpcode.EqCommon: {
-            if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
-              callString = "Equals";
-            } else if (e.E0.Type.IsRefType) {
+            if (e.E0.Type.IsRefType) {
               // Dafny's type rules are slightly different C#, so we may need a cast here.
               // For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
               // type parameter.
               opString = "== (object)";
+            } else if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
+              callString = "Equals";
             } else {
               opString = "==";
             }
             break;
           }
           case BinaryExpr.ResolvedOpcode.NeqCommon: {
-            if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
-              preOpString = "!";
-              callString = "Equals";
-            } else if (e.E0.Type.IsRefType) {
+            if (e.E0.Type.IsRefType) {
               // Dafny's type rules are slightly different C#, so we may need a cast here.
               // For example, Dafny allows x==y if x:array<T> and y:array<int> and T is some
               // type parameter.
               opString = "!= (object)";
+            } else if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
+              preOpString = "!";
+              callString = "Equals";
             } else {
               opString = "!=";
             }
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