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 /Test | |
parent | bbf809e2a1a474e6e79b1c02faa42ec22af8ac8c (diff) |
Don't inline opaque functions.
Added a verifying example with opaque functions and explicit proofs.
Diffstat (limited to 'Test')
-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 |
4 files changed, 30 insertions, 1 deletions
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 --------------------
|