creusot_std/std/
clone.rs

1use crate::prelude::*;
2
3#[cfg(creusot)]
4pub use creusot_std_proc::Clone;
5
6#[cfg(not(creusot))]
7pub use core::clone::Clone;
8
9extern_spec! {
10    mod core {
11        mod clone {
12            trait Clone {
13                fn clone(&self) -> Self;
14
15                #[ensures(resolve(*self))]
16                #[ensures(Self::clone.postcondition((source,), ^self))]
17                fn clone_from(&mut self, source: &Self) {
18                    *self = source.clone()
19                }
20            }
21        }
22    }
23
24    impl Clone for bool {
25        #[check(ghost)]
26        #[ensures(result == *self)]
27        fn clone(&self) -> bool {
28            *self
29        }
30    }
31
32    impl Clone for f32 {
33        #[check(ghost)]
34        #[ensures(result == *self)]
35        fn clone(&self) -> f32 {
36            *self
37        }
38    }
39
40    impl Clone for f64 {
41        #[check(ghost)]
42        #[ensures(result == *self)]
43        fn clone(&self) -> f64 {
44            *self
45        }
46    }
47
48    impl<'a, T: ?Sized> Clone for &'a T {
49        #[check(ghost)]
50        #[ensures(result == *self)]
51        fn clone(&self) -> &'a T {
52            *self
53        }
54    }
55}
creusot_std/std/clone.rs

creusot_std/std/
clone.rs
