Skip to content

Commit 5959b39

Browse files
committed
use a test inspired from @gebner
1 parent fe47c53 commit 5959b39

1 file changed

Lines changed: 7 additions & 0 deletions

File tree

test/pure_fn.c

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -49,3 +49,10 @@ void test() {
4949
bool pure_not_result = pure_not(true);
5050
_assert(pure_not_result == false);
5151
}
52+
53+
_pure int pure_ghost_stmt()
54+
_ensures(1 == 0)
55+
{
56+
_ghost_stmt(assume False);
57+
return 1;
58+
}

0 commit comments

Comments
 (0)