Function extern_spec_std_time_Duration_new 

pub fn extern_spec_std_time_Duration_new(secs: u64, nanos: u32) -> Duration

extern spec for ::std::time::Duration::new

This is not a real function: its only use is for documentation.

terminates

ghost

requires

secs@ + nanos_to_secs(nanos@) <= u64::MAX@

ensures

result@ == secs_to_nanos(secs@) + nanos@