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

use crate::*;
pub use ::std::clone::*;

#[cfg(creusot)]
pub use creusot_contracts_proc::Clone;

extern_spec! {
    mod std {
        mod clone {
            trait Clone {
                // TODO:
                // Requiring result == *self seems too strong since objects can
                // contain information which is lost by the clone (e.g., capacity of
                // vectors...).
                #[ensures(result == *self)]
                fn clone(&self) -> Self;
            }
        }
    }
}