diff options
| -rw-r--r-- | Source/Dafny/Compiler.cs | 50 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/CompilationErrors.dfy | 24 |
3 files changed, 60 insertions, 20 deletions
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 2dac29c1..aa59abad 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -686,10 +686,13 @@ namespace Microsoft.Dafny { } else if (member is Function) {
Function f = (Function)member;
- if (f.Body == null && !Attributes.Contains(f.Attributes, "axiom")) {
- Error("Function {0} has no body", f.FullName);
+ if (f.Body == null) {
+ if (!Attributes.Contains(f.Attributes, "axiom")) {
+ Error("Function {0} has no body", f.FullName);
+ }
} else if (f.IsGhost) {
- // nothing to compile
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(f.Body);
} else {
Indent(indent);
wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.CompileName);
@@ -705,9 +708,14 @@ namespace Microsoft.Dafny { } else if (member is Method) {
Method m = (Method)member;
- if (m.IsGhost && m.Body == null && !Attributes.Contains(m.Attributes, "axiom")) {
- Error("Method {0} has no body", m.FullName);
- } else if (!m.IsGhost) {
+ if (m.Body == null) {
+ if (!Attributes.Contains(m.Attributes, "axiom")) {
+ Error("Method {0} has no body", m.FullName);
+ }
+ } else if (m.IsGhost) {
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(m.Body);
+ } else {
Indent(indent);
wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.CompileName);
if (m.TypeArgs.Count != 0) {
@@ -1001,18 +1009,21 @@ 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 AssignSuchThatStmt) {
- var s = (AssignSuchThatStmt)stmt;
- if (s.AssumeToken != null) {
- Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
- }
- } else {
- foreach (var ss in stmt.SubStatements) {
- CheckHasNoAssumes(ss);
+ public class CheckHasNoAssumes_Visitor : BottomUpVisitor
+ {
+ readonly Compiler compiler;
+ public CheckHasNoAssumes_Visitor(Compiler c) {
+ Contract.Requires(c != null);
+ compiler = c;
+ }
+ protected override void VisitOneStmt(Statement stmt) {
+ if (stmt is AssumeStmt) {
+ compiler.Error("an assume statement cannot be compiled (line {0})", stmt.Tok.line);
+ } else if (stmt is AssignSuchThatStmt) {
+ var s = (AssignSuchThatStmt)stmt;
+ if (s.AssumeToken != null) {
+ compiler.Error("an assume statement cannot be compiled (line {0})", s.AssumeToken.line);
+ }
}
}
}
@@ -1021,7 +1032,8 @@ namespace Microsoft.Dafny { {
Contract.Requires(stmt != null);
if (stmt.IsGhost) {
- CheckHasNoAssumes(stmt);
+ var v = new CheckHasNoAssumes_Visitor(this);
+ v.Visit(stmt);
Indent(indent); wr.WriteLine("{ }");
return;
}
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 0ce33b47..472932c5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -2327,7 +2327,7 @@ Dafny program verifier finished with 0 verified, 0 errors Dafny program verifier finished with 44 verified, 0 errors
Compiled assembly into Compilation.exe
-Dafny program verifier finished with 9 verified, 0 errors
+Dafny program verifier finished with 15 verified, 0 errors
Compilation error: Arbitrary type ('_module.MyType') cannot be compiled
Compilation error: Iterator _module.Iter has no body
Compilation error: Method _module._default.M has no body
@@ -2335,3 +2335,7 @@ Compilation error: Method _module._default.P has no body Compilation error: an assume statement cannot be compiled (line 8)
Compilation error: Function _module._default.F has no body
Compilation error: Function _module._default.H has no body
+Compilation error: an assume statement cannot be compiled (line 17)
+Compilation error: an assume statement cannot be compiled (line 20)
+Compilation error: an assume statement cannot be compiled (line 25)
+Compilation error: an assume statement cannot be compiled (line 34)
diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy index 7d21933a..205b2296 100644 --- a/Test/dafny0/CompilationErrors.dfy +++ b/Test/dafny0/CompilationErrors.dfy @@ -12,3 +12,27 @@ ghost var g: int; function F(): int // compile error: body-less ghost function
function method H(): int // compile error: body-less function method
+
+lemma Lemma() {
+ assume false; // compile error: assume
+}
+ghost method GMethod() {
+ assume false; // compile error: assume
+}
+
+function MyFunction(): int
+{
+ assume false; // compile error: assume
+ 6
+}
+
+function MyCalcFunction(): int
+{
+ calc <= {
+ 2;
+ 6;
+ { assume true; } // compile error: assume
+ 10;
+ }
+ 12
+}
|