diff options
| author |  Rustan Leino <unknown> | 2013-12-17 13:56:41 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-12-17 13:56:41 -0800 |
| commit | 679af7cd0963341cbb057cf9049c81b515a8fa26 (patch) | |
| tree | fc796b17831d924689c491583c0efd9203edad77 | |
| parent | bbf809e2a1a474e6e79b1c02faa42ec22af8ac8c (diff) | |
Don't inline opaque functions.
Added a verifying example with opaque functions and explicit proofs.
| -rw-r--r-- | Source/Dafny/Translator.cs | 2 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 21 | ||||
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 1 |
5 files changed, 32 insertions, 1 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index a2961174..5be91c5a 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -9870,6 +9870,8 @@ namespace Microsoft.Dafny { (codeContext == null || !codeContext.MustReverify)) {
// The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything
// that needed to be proved about the function was proved already in the previous module, even without the body definition).
+ } else if (IsOpaqueFunction(f)) {
+ // Don't inline opaque functions
} else {
// inline this body
var body = GetSubstitutedBody(fexp, f, false);
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);
+ }
+}
diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer index f326d2f9..5b7357e6 100644 --- a/Test/dafny3/Answer +++ b/Test/dafny3/Answer @@ -54,3 +54,7 @@ Dafny program verifier finished with 10 verified, 0 errors -------------------- InfiniteTrees.dfy --------------------
Dafny program verifier finished with 88 verified, 0 errors
+
+-------------------- OpaqueTrees.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat index 7a3d3a20..9bce80c5 100644 --- a/Test/dafny3/runtest.bat +++ b/Test/dafny3/runtest.bat @@ -9,6 +9,7 @@ for %%f in ( SimpleInduction.dfy SimpleCoinduction.dfy CalcExample.dfy
InductionVsCoinduction.dfy Zip.dfy SetIterations.dfy
Paulson.dfy Filter.dfy WideTrees.dfy InfiniteTrees.dfy
+ OpaqueTrees.dfy
) do (
echo.
echo -------------------- %%f --------------------
|