diff options
| author |  Bryan Parno <parno@microsoft.com> | 2013-12-13 18:09:21 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2013-12-13 18:09:21 -0800 |
| commit | 98d05fbc4c087744b44df9dd6ba5e34fbddfe4bb (patch) | |
| tree | 3a12e13786f0d2ea0bd4300fa443e238235dbceb /Test | |
| parent | 0cf321947991319a86adc6899b4015d19c21a188 (diff) | |
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.
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/Compilation.dfy | 22 |
2 files changed, 23 insertions, 1 deletions
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;
+}
|