diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-09-11 10:52:07 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-09-11 10:52:07 -0700 |
| commit | 52d410312d01293428ec3f4d81d4882a26a392d2 (patch) | |
| tree | c2287ff3493fbfc8ac2c4aa8d2eac28f7e78285a /Source/Dafny/Compiler.cs | |
| parent | e8dc0f0f04d377d58884fad15e5525bb1a9f6eca (diff) | |
Dafny: fixed compilation error where type of target "null" was undetermined
Diffstat (limited to 'Source/Dafny/Compiler.cs')
| -rw-r--r-- | Source/Dafny/Compiler.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 6a448172..7db1e98f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -601,7 +601,7 @@ namespace Microsoft.Dafny { } else if (type is IntType) {
return "new BigInteger(0)";
} else if (type.IsRefType) {
- return "null";
+ return string.Format("({0})null", TypeName(type));
} else if (type.IsDatatype) {
UserDefinedType udt = (UserDefinedType)type;
string s = "@" + udt.Name;
@@ -1175,7 +1175,7 @@ namespace Microsoft.Dafny { if (expr is LiteralExpr) {
LiteralExpr e = (LiteralExpr)expr;
if (e.Value == null) {
- wr.Write("null");
+ wr.Write("({0})null", TypeName(e.Type));
} else if (e.Value is bool) {
wr.Write((bool)e.Value ? "true" : "false");
} else if (e.Value is BigInteger) {
|