2025-01-09 00:38:25 +00:00
|
|
|
//@ revisions: unchk_pass unchk_fail_pre unchk_fail_post chk_pass chk_fail_pre chk_fail_post
|
|
|
|
//
|
|
|
|
//@ [unchk_pass] run-pass
|
|
|
|
//@ [unchk_fail_pre] run-pass
|
|
|
|
//@ [unchk_fail_post] run-pass
|
|
|
|
//@ [chk_pass] run-pass
|
|
|
|
//
|
|
|
|
//@ [chk_fail_pre] run-fail
|
|
|
|
//@ [chk_fail_post] run-fail
|
|
|
|
//
|
|
|
|
//@ [unchk_pass] compile-flags: -Zcontract-checks=no
|
|
|
|
//@ [unchk_fail_pre] compile-flags: -Zcontract-checks=no
|
|
|
|
//@ [unchk_fail_post] compile-flags: -Zcontract-checks=no
|
|
|
|
//
|
|
|
|
//@ [chk_pass] compile-flags: -Zcontract-checks=yes
|
|
|
|
//@ [chk_fail_pre] compile-flags: -Zcontract-checks=yes
|
|
|
|
//@ [chk_fail_post] compile-flags: -Zcontract-checks=yes
|
|
|
|
|
2025-01-31 01:06:09 +00:00
|
|
|
#![feature(contracts_internals)]
|
2025-01-09 00:38:25 +00:00
|
|
|
|
|
|
|
fn nest(x: Baz) -> i32
|
2025-01-31 01:06:09 +00:00
|
|
|
contract_requires(|| x.baz > 0)
|
|
|
|
contract_ensures(|ret| *ret > 100)
|
2025-01-09 00:38:25 +00:00
|
|
|
{
|
|
|
|
loop {
|
|
|
|
return x.baz + 50;
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
struct Baz { baz: i32 }
|
|
|
|
|
|
|
|
const BAZ_PASS_PRE_POST: Baz = Baz { baz: 100 };
|
|
|
|
#[cfg(any(unchk_fail_post, chk_fail_post))]
|
|
|
|
const BAZ_FAIL_POST: Baz = Baz { baz: 10 };
|
|
|
|
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
|
|
|
|
const BAZ_FAIL_PRE: Baz = Baz { baz: -10 };
|
|
|
|
|
|
|
|
fn main() {
|
|
|
|
assert_eq!(nest(BAZ_PASS_PRE_POST), 150);
|
|
|
|
#[cfg(any(unchk_fail_pre, chk_fail_pre))]
|
|
|
|
nest(BAZ_FAIL_PRE);
|
|
|
|
#[cfg(any(unchk_fail_post, chk_fail_post))]
|
|
|
|
nest(BAZ_FAIL_POST);
|
|
|
|
}
|