diff options
| author |  qunyanm <unknown> | 2015-04-13 14:25:33 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2015-04-13 14:25:33 -0700 |
| commit | 4c70e323d1af8be2e7386ea25ecb7fe77ec09a49 (patch) | |
| tree | c27ec0f5fdd5ae48b72eee85a19171bf026d957a /Source/Dafny/Compiler.cs | |
| parent | a84dd34f6f784c344c25340838cee07f44df6d74 (diff) | |
Fix issue #67. Check SupportsEquality before determining whether to emit Equals
or == for equality testing.
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index f2a1bdcd..570ac30d 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -430,7 +430,7 @@ namespace Microsoft.Dafny { foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
string nm = FormalName(arg, i);
- if (arg.Type.IsDatatype || arg.Type.IsTypeParameter) {
+ if (arg.Type.IsDatatype || arg.Type.IsTypeParameter || arg.Type.SupportsEquality) {
wr.Write(" && this.@{0}.Equals(oth.@{0})", nm);
} else {
wr.Write(" && this.@{0} == oth.@{0}", nm);
@@ -2408,7 +2408,7 @@ namespace Microsoft.Dafny { opString = "&&"; break;
case BinaryExpr.ResolvedOpcode.EqCommon: {
- if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) {
+ if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
callString = "Equals";
} else if (e.E0.Type.IsRefType) {
// Dafny's type rules are slightly different C#, so we may need a cast here.
@@ -2421,7 +2421,7 @@ namespace Microsoft.Dafny { break;
}
case BinaryExpr.ResolvedOpcode.NeqCommon: {
- if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter) {
+ if (e.E0.Type.IsDatatype || e.E0.Type.IsTypeParameter || e.E0.Type.SupportsEquality) {
preOpString = "!";
callString = "Equals";
} else if (e.E0.Type.IsRefType) {
|