Don't inline opaque functions.

Added a verifying example with opaque functions and explicit proofs.

1 files changed, 21 insertions, 0 deletions

diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy
index c15515d2..9879c66b 100644
--- a/Test/dafny0/OpaqueFunctions.dfy
+++ b/Test/dafny0/OpaqueFunctions.dfy
@@ -121,3 +121,24 @@ module B' refines B {
   }

 }

 

+// ---------------------------------

+

+module OpaqueFunctionsAreNotInlined {

+  predicate {:opaque} F(n: int)

+  {

+    0 <= n < 100

+  }

+

+  method M()

+  {

+    var x := 18;

+    assert F(x);  // error: cannot be determined, since F is opaque

+  }

+

+  method M'()

+  {

+    var x := 18;

+    reveal_F();

+    assert F(x);

+  }

+}