From 679af7cd0963341cbb057cf9049c81b515a8fa26 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 17 Dec 2013 13:56:41 -0800
Subject: Don't inline opaque functions. Added a verifying example with opaque
 functions and explicit proofs.

---
 Test/dafny0/Answer              |  5 ++++-
 Test/dafny0/OpaqueFunctions.dfy | 21 +++++++++++++++++++++
 2 files changed, 25 insertions(+), 1 deletion(-)

(limited to 'Test/dafny0')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 676c0313..3b475659 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1785,8 +1785,11 @@ OpaqueFunctions.dfy(119,14): Error: assertion violation
 Execution trace:
     (0,0): anon0
     (0,0): anon6_Else
+OpaqueFunctions.dfy(135,12): Error: assertion violation
+Execution trace:
+    (0,0): anon0
 
-Dafny program verifier finished with 32 verified, 18 errors
+Dafny program verifier finished with 37 verified, 19 errors
 
 -------------------- Maps.dfy --------------------
 Maps.dfy(76,8): Error: element may not be in domain
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);
+  }
+}
-- 
cgit v1.2.3