diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 9 | ||||
| -rw-r--r-- | Source/DafnyDriver/DafnyDriver.cs | 2 |
2 files changed, 8 insertions, 3 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 080930ea..1e27c4db 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1128,9 +1128,14 @@ namespace Microsoft.Dafny { s.TargetStmt = target;
}
}
-
+ if (specContextOnly) {
+ Error(stmt, "break statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
+
} else if (stmt is ReturnStmt) {
- // nothing to resolve
+ if (specContextOnly) {
+ Error(stmt, "return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)");
+ }
} else if (stmt is AssignStmt) {
AssignStmt s = (AssignStmt)stmt;
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index b3efd7aa..aa0be9dd 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -268,7 +268,7 @@ namespace Microsoft.Boogie }
if (tok is Dafny.NestedToken) {
var nt = (Dafny.NestedToken)tok;
- ReportBplError(nt.Inner, "Related location", false);
+ ReportBplError(nt.Inner, "Related location: Related location", false);
}
}
|