creusot_std/std/
rc.rs

1use crate::prelude::*;
2use alloc::{boxed::Box, rc::Rc};
3#[cfg(feature = "nightly")]
4use core::alloc::Allocator;
5use core::ops::Deref;
6
7#[cfg(feature = "nightly")]
8impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Rc<T, A> {
9    type DeepModelTy = T::DeepModelTy;
10    #[logic(open, inline)]
11    fn deep_model(self) -> Self::DeepModelTy {
12        pearlite! { *self.view().deep_model() }
13    }
14}
15
16#[cfg(feature = "nightly")]
17impl<T: ?Sized, A: Allocator> View for Rc<T, A> {
18    type ViewTy = Box<T>;
19    #[logic(opaque)]
20    fn view(self) -> Self::ViewTy {
21        dead
22    }
23}
24
25extern_spec! {
26    mod alloc {
27        mod rc {
28            impl<T> Rc<T> {
29                #[check(ghost)]
30                #[ensures(*result@ == value)]
31                fn new(value: T) -> Self;
32            }
33
34            impl<T, A: Allocator> AsRef for Rc<T, A> {
35                #[check(ghost)]
36                #[ensures(*result == *(*self)@)]
37                fn as_ref(&self) -> &T;
38            }
39        }
40    }
41
42    impl<T: ?Sized, A: Allocator + Clone> Clone for Rc<T, A> {
43        #[check(ghost)]
44        #[ensures(result == *self)]
45        fn clone(&self) -> Rc<T, A>;
46    }
47
48    impl<T: ?Sized, A: Allocator> Deref for Rc<T, A> {
49        #[check(ghost)]
50        #[ensures(*result == *(*self)@)]
51        fn deref(&self) -> &T;
52    }
53}
54
55/// Dummy impls that don't use the unstable trait Allocator
56#[cfg(not(feature = "nightly"))]
57impl<T: DeepModel> DeepModel for Rc<T> {
58    type DeepModelTy = T::DeepModelTy;
59}
60
61#[cfg(not(feature = "nightly"))]
62impl<T> View for Rc<T> {
63    type ViewTy = T;
64}
creusot_std/std/rc.rs

creusot_std/std/
rc.rs
