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/dafny0 | |
| parent | bbf809e2a1a474e6e79b1c02faa42ec22af8ac8c (diff) | |
Don't inline opaque functions.
Added a verifying example with opaque functions and explicit proofs.
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Answer | 5 | ||||
| -rw-r--r-- | Test/dafny0/OpaqueFunctions.dfy | 21 |
2 files changed, 25 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);
+ }
+}
|