diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-09-11 13:20:52 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-09-11 13:20:52 -0700 |
| commit | 4e1b5db18c8c57ec44421031a13e6e79bb7e5d64 (patch) | |
| tree | 51c978f47a5223dd11ec916dfe72f301b65e580c /Dafny/Compiler.cs | |
| parent | 3e68c6c93cc1bfbb6491e42945ce3c0b630a1f2f (diff) | |
Dafny: generate a compiler error upon encountering an assume statement
Dafny: don't compile programs unless all methods have been verified (or a forced compile is requested)
Diffstat (limited to 'Dafny/Compiler.cs')
| -rw-r--r-- | Dafny/Compiler.cs | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs index 69008d26..c8051e2b 100644 --- a/Dafny/Compiler.cs +++ b/Dafny/Compiler.cs @@ -658,10 +658,56 @@ namespace Microsoft.Dafny { // ----- Stmt ---------------------------------------------------------------------------------
+ void CheckHasNoAssumes(Statement stmt) {
+ Contract.Requires(stmt != null);
+ if (stmt is AssumeStmt) {
+ Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);
+ } else if (stmt is BlockStmt) {
+ foreach (Statement s in ((BlockStmt)stmt).Body) {
+ CheckHasNoAssumes(s);
+ }
+ } else if (stmt is IfStmt) {
+ IfStmt s = (IfStmt)stmt;
+ CheckHasNoAssumes(s.Thn);
+ if (s.Els != null) {
+ CheckHasNoAssumes(s.Els);
+ }
+ } else if (stmt is AlternativeStmt) {
+ foreach (var alternative in ((AlternativeStmt)stmt).Alternatives) {
+ foreach (Statement s in alternative.Body) {
+ CheckHasNoAssumes(s);
+ }
+ }
+ } else if (stmt is WhileStmt) {
+ WhileStmt s = (WhileStmt)stmt;
+ CheckHasNoAssumes(s.Body);
+ } else if (stmt is AlternativeLoopStmt) {
+ foreach (var alternative in ((AlternativeLoopStmt)stmt).Alternatives) {
+ foreach (Statement s in alternative.Body) {
+ CheckHasNoAssumes(s);
+ }
+ }
+ } else if (stmt is ForeachStmt) {
+ ForeachStmt s = (ForeachStmt)stmt;
+ foreach (PredicateStmt t in s.BodyPrefix) {
+ CheckHasNoAssumes(t);
+ }
+ CheckHasNoAssumes(s.GivenBody);
+ } else if (stmt is MatchStmt) {
+ MatchStmt s = (MatchStmt)stmt;
+ foreach (MatchCaseStmt mc in s.Cases) {
+ foreach (Statement bs in mc.Body) {
+ CheckHasNoAssumes(bs);
+ }
+ }
+ }
+ }
+
void TrStmt(Statement stmt, int indent)
{
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
+ CheckHasNoAssumes(stmt);
return;
}
|