diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-14 13:35:11 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-14 13:35:11 -0700 |
| commit | 480afe3ff4042ece26c4206602190047f7f9bfb0 (patch) | |
| tree | 706f95174a09017502c12769f2e3e2aba1cd818c /Dafny | |
| parent | 1f267ac0d7daf434ed4db31d23914428149297bc (diff) | |
Dafny: fixed a couple of compiler bugs
Diffstat (limited to 'Dafny')
| -rw-r--r-- | Dafny/Compiler.cs | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 911e5aac..3938ec8d 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -1829,6 +1829,11 @@ namespace Microsoft.Dafny { Type t = cce.NonNull(e.E0.Type);
if (t.IsDatatype || t.IsTypeParameter) {
callString = "Equals";
+ } else if (t.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 {
opString = "==";
}
@@ -1839,6 +1844,11 @@ namespace Microsoft.Dafny { if (t.IsDatatype || t.IsTypeParameter) {
preOpString = "!";
callString = "Equals";
+ } else if (t.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 {
opString = "!=";
}
|