creusot_contracts/std/
clone.rs

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

creusot_contracts/std/
clone.rs
