From 98d05fbc4c087744b44df9dd6ba5e34fbddfe4bb Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@microsoft.com>
Date: Fri, 13 Dec 2013 18:09:21 -0800
Subject: Add support for the :axiom attribute for ghost methods. This
 suppresses compiler errors for ghost methods and functions without bodies.
 Also changed the parser to complain about bodyless methods and functions
 without bodies if /noCheating:1 is specified.

---
 Test/dafny0/Answer          |  2 +-
 Test/dafny0/Compilation.dfy | 22 ++++++++++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 5ac570f3..424b83bb 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2442,7 +2442,7 @@ Execution trace:
 
 Dafny program verifier finished with 28 verified, 2 errors
 
-Dafny program verifier finished with 30 verified, 0 errors
+Dafny program verifier finished with 37 verified, 0 errors
 Compiled assembly into Compilation.exe
 
 Dafny program verifier finished with 9 verified, 0 errors
diff --git a/Test/dafny0/Compilation.dfy b/Test/dafny0/Compilation.dfy
index 5120bf81..734cc3e6 100644
--- a/Test/dafny0/Compilation.dfy
+++ b/Test/dafny0/Compilation.dfy
@@ -148,3 +148,25 @@ class DigitsClass {
   }
 }
 
+// Should not get errors about methods or functions with empty bodies
+// if they're marked with an :axiom attribute
+ghost method {:axiom} m_nobody() returns (y:int)
+  ensures y > 5;
+
+lemma {:axiom} l_nobody() returns (y:int)
+  ensures y > 5;
+
+function {:axiom} f_nobody():int 
+  ensures f_nobody() > 5;
+
+// Make sure the lemma created for opaque functions doesn't produce compiler errors
+function {:opaque} hidden():int
+{
+  7
+}
+
+method hidden_test()
+{
+  reveal_hidden();
+  assert hidden() == 7;
+}
-- 
cgit v1.2.3