1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

use crate::*;
pub use ::std::mem::*;

extern_spec! {
    mod std {
        mod mem {
            #[pure]
            #[ensures(^dest == src)]
            #[ensures(result == *dest)]
            fn replace<T>(dest: &mut T, src: T) -> T;

            #[pure]
            #[ensures(^x == *y)]
            #[ensures(^y == *x)]
            fn swap<T>(x: &mut T, y: &mut T);

            #[ensures(result == *dest)]
            #[ensures((^dest).is_default())]
            fn take<T: Default>(dest: &mut T) -> T;
        }
    }
}