diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-01-10 13:02:21 -0800 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-01-10 13:02:21 -0800 |
| commit | 335ac08951e427500de34d55b14713cced6c12bd (patch) | |
| tree | d7ae7d9d1c7903181b1ecb9a6131d81926a5dea0 /Test/dafny0/AutoReq.dfy | |
| parent | dd8d1baa05c4ca1bcbe594ec96a65c41f991604b (diff) | |
A better fix to deal with StaticReceiverTypes affected by autoReq.
Diffstat (limited to 'Test/dafny0/AutoReq.dfy')
| -rw-r--r-- | Test/dafny0/AutoReq.dfy | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/Test/dafny0/AutoReq.dfy b/Test/dafny0/AutoReq.dfy index 684de262..0936176f 100644 --- a/Test/dafny0/AutoReq.dfy +++ b/Test/dafny0/AutoReq.dfy @@ -285,4 +285,15 @@ module StaticTest { {
g(y)
}
-}
\ No newline at end of file +
+ static predicate IsEven(x:int)
+
+ static function EvenDoubler(x:int) : int
+ requires IsEven(x);
+
+ // Should succeed thanks to auto-generated requirement of IsEven
+ static function {:autoReq} test(y:int) : int
+ {
+ EvenDoubler(y)
+ }
+}
|