creusot_contracts/std/
rc.rs

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

creusot_contracts/std/
rc.rs
