diff options
Diffstat (limited to 'Test/inline/fundef2.bpl')
| -rw-r--r-- | Test/inline/fundef2.bpl | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Test/inline/fundef2.bpl b/Test/inline/fundef2.bpl index 2e005fcc..527d235d 100644 --- a/Test/inline/fundef2.bpl +++ b/Test/inline/fundef2.bpl @@ -1,7 +1,9 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
function {:inline true} foo(x:int) returns(bool)
{ x > 0 }
procedure P() {
assert foo(13);
assert foo(-5); // error
-}
\ No newline at end of file +}
|