vstd/std_specs/
clone.rs
1use super::super::prelude::*;
2use core::clone::Clone;
3
4verus! {
5
6#[verifier::external_trait_specification]
7pub trait ExClone: Sized {
8 type ExternalTraitSpecificationFor: core::clone::Clone;
9
10 fn clone(&self) -> Self;
11}
12
13pub assume_specification[ <bool as Clone>::clone ](b: &bool) -> (res: bool)
22 returns
23 b,
24;
25
26pub assume_specification[ <char as Clone>::clone ](c: &char) -> (res: char)
27 returns
28 c,
29;
30
31#[allow(suspicious_double_ref_op)]
32pub assume_specification<'b, T: ?Sized, 'a>[ <&'b T as Clone>::clone ](b: &'a &'b T) -> (res: &'b T)
33 ensures
34 res == b,
35;
36
37pub assume_specification<T: Copy>[ <Tracked<T> as Clone>::clone ](b: &Tracked<T>) -> (res: Tracked<
48 T,
49>)
50 ensures
51 res == b,
52;
53
54pub assume_specification<T>[ <Ghost<T> as Clone>::clone ](b: &Ghost<T>) -> (res: Ghost<T>)
55 ensures
56 res == b,
57;
58
59}