Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384use super::super::prelude::*;use core::marker::PointeeSized;
verus! {
#[verifier::external_trait_specification]pub trait ExDefault: Sized { type ExternalTraitSpecificationFor: core::default::Default;
fn default() -> (r: Self);}
} // verus!macro_rules! assume_default_value { ($t:ty, $default_value:expr) => { verus! { pub assume_specification [ <$t as core::default::Default>::default ]() -> (r: $t) ensures r == $default_value, ; } };}
assume_default_value!(bool, false);assume_default_value!(char, '\0');assume_default_value!(f32, 0.0f32);assume_default_value!(f64, 0.0f64);assume_default_value!(i8, 0i8);assume_default_value!(i16, 0i16);assume_default_value!(i32, 0i32);assume_default_value!(i64, 0i64);assume_default_value!(i128, 0i128);assume_default_value!(isize, 0isize);assume_default_value!(u8, 0u8);assume_default_value!(u16, 0u16);assume_default_value!(u32, 0u32);assume_default_value!(u64, 0u64);assume_default_value!(u128, 0u128);assume_default_value!((), ());assume_default_value!(usize, 0usize);
// manually implementation for Option<T>, &str, PhantomData<T>, (U, T), (V, U, T)verus! {
pub assume_specification<T>[ <Option<T> as core::default::Default>::default ]() -> (r: Option<T>) ensures r == Option::<T>::None,;
pub assume_specification<'a>[ <&'a str as core::default::Default>::default ]() -> (r: &'a str) ensures r == "",;
pub assume_specification<T: PointeeSized>[ <core::marker::PhantomData< T,> as core::default::Default>::default ]() -> (r: core::marker::PhantomData<T>) ensures r == core::marker::PhantomData::<T>,;
pub assume_specification<U: core::default::Default, T: core::default::Default>[ <( U, T,) as core::default::Default>::default ]() -> (r: (U, T)) ensures call_ensures(U::default, (), r.0), call_ensures(T::default, (), r.1),;
pub assume_specification< V: core::default::Default, U: core::default::Default, T: core::default::Default,>[ <(V, U, T) as core::default::Default>::default ]() -> (r: (V, U, T)) ensures call_ensures(V::default, (), r.0), call_ensures(U::default, (), r.1), call_ensures(T::default, (), r.2),;
} // verus!