Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435// rust_verify/tests/example.rs#[allow(unused_imports)]use verus_builtin::*;#[allow(unused_imports)]use verus_builtin_macros::*;use vstd::thread::*;
verus! {
fn test_calling_thread_id_twice_same_value() { let (tid1, Tracked(is1)) = thread_id(); let (tid2, Tracked(is2)) = thread_id(); proof { is1.agrees(is2); } assert(tid1 == tid2);}
fn test_calling_thread_id_twice_diff_threads() { let (tid1, Tracked(is1)) = thread_id(); spawn( move || { let (tid2, Tracked(is2)) = thread_id(); // This isn't allowed: Send error /*proof { is1.agrees(is2); }*/ }, );}
} // verus!fn main() {}