diff options
| author |  leino <unknown> | 2015-11-11 17:36:24 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-11-11 17:36:24 -0800 |
| commit | 7cc9a11d13a1d43d6e7beb4f874bb086f73804c4 (patch) | |
| tree | 2a1053b087323964ccb7505d983806045da778b0 | |
| parent | 3a5f8c7e20671a8e4eb706239b8d071f98846bf1 (diff) | |
Fixed compilation of equality between reference types
| -rw-r--r-- | Source/Dafny/Compiler.cs | 14 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 55 | ||||
| -rw-r--r-- | 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 |