Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192// rust_verify/tests/example.rs expect-success#[allow(unused_imports)]use verus_builtin::*;#[allow(unused_imports)]use verus_builtin_macros::*;
verus! {
// ANCHOR: spec_constspec const SPEC_ONE: int = 1;
spec fn spec_add_one(x: int) -> int { x + SPEC_ONE}
// ANCHOR_END: spec_const// ANCHOR: exec_const_syntaxexec const C: u64 ensures C == 7,{ 7}
// ANCHOR_END: exec_const_syntax// ANCHOR: exec_const_complicatedspec fn f() -> int { 1}
const fn e() -> (u: u64) ensures u == f(),{ 1}
exec const E: u64 ensures E == 2,{ assert(f() == 1); 1 + e()}
// ANCHOR_END: exec_const_complicated// ANCHOR: spec_exec_constconst ONE: u8 = 1;
fn add_one(x: u8) -> (ret: u8) requires x < 0xff, ensures ret == x + ONE, // use "ONE" in spec code{ x + ONE // use "ONE" in exec code
}
// ANCHOR_END: spec_exec_const// ANCHOR: when_used_as_specuse vstd::layout;
global layout usize is size == 8;
spec const SPEC_USIZE_BYTES: usize = layout::size_of_as_usize::<usize>();
#[verifier::when_used_as_spec(SPEC_USIZE_BYTES)]exec const USIZE_BYTES: usize ensures USIZE_BYTES as nat == layout::size_of::<usize>(),{ 8}
// ANCHOR_END: when_used_as_spec// ANCHOR: nonlinearpub const FOO: u8 = 4;
pub const BAR: u8 = FOO;
pub const BAR_PLUS_ONE: u8 = BAR + 1;
#[verifier::nonlinear]pub const G: u8 = BAR_PLUS_ONE * BAR;
// ANCHOR_END: nonlinearfn main() {}
} // verus!