vstd_extra/external/time.rs
1use vstd::prelude::*;
2
3use crate::panic::may_panic;
4
5verus! {
6
7/// Abstract result of constructing a standard-library duration.
8pub uninterp spec fn duration_new_spec(secs: u64, nanos: u32) -> core::time::Duration;
9
10#[verifier::when_used_as_spec(duration_new_spec)]
11pub assume_specification[ core::time::Duration::new ](secs: u64, nanos: u32) -> core::time::Duration
12 requires
13 secs + nanos / 1_000_000_000 > u64::MAX ==> may_panic(),
14 returns
15 duration_new_spec(secs, nanos),
16 opens_invariants none
17;
18
19} // verus!