creusot_contracts/std/
sync.rs

1use crate::prelude::*;
2#[cfg(feature = "nightly")]
3use std::alloc::Allocator;
4use std::sync::Arc;
5
6#[cfg(feature = "nightly")]
7impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Arc<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 Arc<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 sync {
27            impl<T> Arc<T> {
28                #[check(ghost)]
29                #[ensures(*result@ == value)]
30                fn new(value: T) -> Self;
31            }
32
33            impl<T, A: Allocator> AsRef for Arc<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 Arc<T, A> {
42        #[check(ghost)]
43        #[ensures(result@ == (*self)@)]
44        fn clone(&self) -> Arc<T, A>;
45    }
46}
47
48/// Dummy impls that don't use the unstable trait Allocator
49#[cfg(not(feature = "nightly"))]
50impl<T: DeepModel> DeepModel for Arc<T> {
51    type DeepModelTy = T::DeepModelTy;
52}
53
54#[cfg(not(feature = "nightly"))]
55impl<T> View for Arc<T> {
56    type ViewTy = T;
57}
creusot_contracts/std/sync.rs

creusot_contracts/std/
sync.rs
