diff options
| author |  leino <unknown> | 2015-04-05 22:20:53 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-05 22:20:53 -0700 |
| commit | 1975381d81aabbc16ae552685b5976cad531122a (patch) | |
| tree | 0782ca8eccb038a103cecffce1b1bbb334188a1a | |
| parent | 0aeab928abc85e646dc58c4dc4670a03a36cbc2f (diff) | |
Fixed missing case in previous check-in
| -rw-r--r-- | Source/Dafny/Compiler.cs | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 7b63f65b..d43c57c6 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -796,8 +796,12 @@ namespace Microsoft.Dafny { }
} else if (f.IsGhost) {
// nothing to compile, but we do check for assumes
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(f.Body);
+ if (f.Body == null) {
+ Contract.Assert(c is TraitDecl && !f.IsStatic);
+ } else {
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(f.Body);
+ }
} else if (c is TraitDecl && !forCompanionClass) {
// include it, unless it's static
if (!f.IsStatic) {
@@ -832,8 +836,12 @@ namespace Microsoft.Dafny { }
} else if (m.IsGhost) {
// nothing to compile, but we do check for assumes
- var v = new CheckHasNoAssumes_Visitor(this);
- v.Visit(m.Body);
+ if (m.Body == null) {
+ Contract.Assert(c is TraitDecl && !m.IsStatic);
+ } else {
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(m.Body);
+ }
} else if (c is TraitDecl && !forCompanionClass) {
// include it, unless it's static
if (!m.IsStatic) {
|