Let compiler complain about body-less functions and methods, even if these are ghost

1 files changed, 14 insertions, 0 deletions

diff --git a/Test/dafny0/CompilationErrors.dfy b/Test/dafny0/CompilationErrors.dfy
new file mode 100644
index 00000000..7d21933a
--- /dev/null
+++ b/Test/dafny0/CompilationErrors.dfy
@@ -0,0 +1,14 @@
+type MyType  // compile error: arbitrary type

+iterator Iter()  // compile error: body-less iterator

+ghost method M()  // compile error: body-less ghost method

+method P()  // compile error: body-less method

+method Q()

+{

+  if g == 0 {

+    assume true;  // compile error: assume

+  }

+}

+ghost var g: int;

+

+function F(): int  // compile error: body-less ghost function

+function method H(): int  // compile error: body-less function method