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 /Source | |
parent | 3a5f8c7e20671a8e4eb706239b8d071f98846bf1 (diff) |
Fixed compilation of equality between reference types
Diffstat (limited to 'Source')
-rw-r--r-- | Source/Dafny/Compiler.cs | 14 |
1 files changed, 7 insertions, 7 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 = "!=";
}
|