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 | 4d5757e19265d5e065a1b3848beab1c583a40a4c (patch) | |
| tree | 8551b88136a60db325c3b9ab7914859cdb914dfe | |
| parent | 904420332a82fb0750fff2a34f70fe4e8868543c (diff) | |
Dafny: fixed a couple of compiler bugs
| -rw-r--r-- | Binaries/DafnyRuntime.cs | 3 | ||||
| -rw-r--r-- | Source/Dafny/Compiler.cs | 10 | ||||
| -rw-r--r-- | Test/dafny2/StoreAndRetrieve.dfy | 2 |
3 files changed, 13 insertions, 2 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index f7eecfc5..61df448f 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -1,8 +1,9 @@ using System.Numerics;
-using System.Collections.Generic;
namespace Dafny
{
+ using System.Collections.Generic;
+
public class Set<T>
{
Dictionary<T, bool> dict;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 911e5aac..3938ec8d 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/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 = "!=";
}
diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy index ea26a234..15c82d65 100644 --- a/Test/dafny2/StoreAndRetrieve.dfy +++ b/Test/dafny2/StoreAndRetrieve.dfy @@ -1,4 +1,4 @@ -module A imports Library {
+ghost module A imports Library {
class {:autocontracts} StoreAndRetrieve<Thing> {
ghost var Contents: set<Thing>;
predicate Valid
|