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                #[requires(true)]
14                fn clone(&self) -> Self;
15            }
16        }
17    }
18
19    impl Clone for bool {
20        #[check(ghost)]
21        #[ensures(result == *self)]
22        fn clone(&self) -> bool {
23            *self
24        }
25    }
26
27    impl Clone for f32 {
28        #[check(ghost)]
29        #[ensures(result == *self)]
30        fn clone(&self) -> f32 {
31            *self
32        }
33    }
34
35    impl Clone for f64 {
36        #[check(ghost)]
37        #[ensures(result == *self)]
38        fn clone(&self) -> f64 {
39            *self
40        }
41    }
42
43    impl<'a, T: ?Sized> Clone for &'a T {
44        #[check(ghost)]
45        #[ensures(result == *self)]
46        fn clone(&self) -> &'a T {
47            *self
48        }
49    }
50}
creusot_std/std/clone.rs

creusot_std/std/
clone.rs
