diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-13 21:56:40 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-13 21:56:40 -0800 |
| commit | 47637c8e97c4cb5f238de2f8d7f3870a869c372f (patch) | |
| tree | 42c373823f9504237e90a0100fe5002d26a7d179 /Test/dafny0/AutoReq.dfy | |
| parent | c1341a323aa60f563a59355a0ede693c80dd2fc0 (diff) | |
Improve autoReq's interactions with opaque
Diffstat (limited to 'Test/dafny0/AutoReq.dfy')
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 0936176f..08acfc50 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -297,3 +297,17 @@ module StaticTest { EvenDoubler(y)
}
}
+
+module OpaqueTest {
+ static function bar(x:int) : int
+ requires x>7;
+ {
+ x-2
+ }
+
+ static function {:autoReq} {:opaque} foo(x:int) : int
+ {
+ bar(x)
+ }
+
+}
|