@@ -196,7 +196,7 @@ lem RawVecInner_send<A>(t1: thread_id_t)
196196 close RawVecInner_own::<A>(t1, v);
197197}
198198
199- lem_auto RawVecInner_inv<A>()
199+ lem_auto RawVecInner_inv<A: ?Sized >()
200200 req RawVecInner::<A>(?t, ?self_, ?elemLayout, ?alloc_id, ?ptr, ?capacity);
201201 ens RawVecInner::<A>(t, self_, elemLayout, alloc_id, ptr, capacity) &*&
202202 ptr != 0 &*& ptr as usize % elemLayout.align() == 0 &*&
@@ -954,7 +954,7 @@ impl<T, A: Allocator> RawVec<T, A> {
954954/// an allocator could overallocate and return a greater memory block than requested.
955955pub ( crate ) unsafe fn into_box ( self , len : usize ) -> Box < [ MaybeUninit < T > ] , A >
956956 //@ req thread_token(?t) &*& RawVec(t, self, ?alloc_id, ?ptr, len) &*& array_at_lft_(alloc_id.lft, ptr as *T, len, ?vs);
957- //@ ens thread_token(t) &*& std::boxed::Box_slice_in ::<std::mem::MaybeUninit<T>, A>(t, result, alloc_id, map(std::mem::MaybeUninit::new_maybe_uninit, vs));
957+ //@ ens thread_token(t) &*& std::boxed::Box_in ::<[ std::mem::MaybeUninit<T>] , A>(t, result, alloc_id, slice_of_elems( map(std::mem::MaybeUninit::new_maybe_uninit, vs) ));
958958 //@ on_unwind_ens thread_token(t);
959959 {
960960 // Sanity-check one half of the safety requirement (we cannot check the other half).
@@ -1005,11 +1005,12 @@ impl<T, A: Allocator> RawVec<T, A> {
10051005 //@ close_points_to(me_ref1, 1/2);
10061006 //@ end_ref_readonly(me_ref1);
10071007 //@ open_points_to(&me);
1008- //@ std::mem::array_at_lft__to_array_at_lft_MaybeUninit(slice.ptr as *T);
1008+ //@ std::mem::array_at_lft__to_array_at_lft_MaybeUninit(slice as *T);
10091009 //@ open RawVec(_, _, _, _, _);
10101010 //@ open RawVecInner(_, _, _, _, _, _);
10111011 //@ size_align::<T>();
10121012 //@ if len * std::mem::size_of::<T>() != 0 { std::alloc::Layout_repeat_some_size_aligned(Layout::new::<T>(), len); }
1013+ //@ close_points_to_slice_at_lft(slice);
10131014 Box :: from_raw_in ( slice, alloc)
10141015 }
10151016 }
@@ -1090,6 +1091,7 @@ impl<T, A: Allocator> RawVec<T, A> {
10901091 // SAFETY: Precondition passed to the caller
10911092 unsafe {
10921093 let ptr = ptr. cast ( ) ;
1094+ //@ std::ptr::NonNull_Sized_as_ptr(ptr);
10931095 //@ std::alloc::Layout_inv(Layout::new::<T>());
10941096 /*@
10951097 if 1 <= std::mem::size_of::<T>() && capacity != 0 {
@@ -1538,10 +1540,10 @@ impl<A: Allocator> RawVecInner<A> {
15381540 RawVecInner(t, v, elem_layout, alloc_id, ?ptr, ?capacity_) &*&
15391541 capacity <= capacity_ &*&
15401542 match init {
1541- raw_vec:: AllocInit::Uninitialized =>
1543+ AllocInit::Uninitialized =>
15421544 array_at_lft_(alloc_id.lft, ptr, ?n, _) &*&
15431545 elem_layout.size() % elem_layout.align() != 0 || n == capacity_ * elem_layout.size(),
1544- raw_vec:: AllocInit::Zeroed =>
1546+ AllocInit::Zeroed =>
15451547 array_at_lft(alloc_id.lft, ptr, ?n, ?bs) &*&
15461548 elem_layout.size() % elem_layout.align() != 0 || n == capacity_ * elem_layout.size() &*&
15471549 forall(bs, (eq)(0)) == true
@@ -1564,8 +1566,8 @@ impl<A: Allocator> RawVecInner<A> {
15641566 close RawVecInner0(r, elem_layout, ptr, capacity_);
15651567 close <RawVecInner<A>>.own(_t, r);
15661568 match init {
1567- raw_vec:: AllocInit::Uninitialized => { leak array_at_lft_(_, _, _, _); }
1568- raw_vec:: AllocInit::Zeroed => { leak array_at_lft(_, _, _, _); }
1569+ AllocInit::Uninitialized => { leak array_at_lft_(_, _, _, _); }
1570+ AllocInit::Zeroed => { leak array_at_lft(_, _, _, _); }
15691571 }
15701572 }
15711573 Result::Err(e) => { }
@@ -1604,8 +1606,8 @@ impl<A: Allocator> RawVecInner<A> {
16041606 //@ mul_zero(capacity, elem_layout.size());
16051607 /*@
16061608 match init {
1607- raw_vec:: AllocInit::Uninitialized => { close array_at_lft_(alloc_id.lft, ptr_, 0, []); }
1608- raw_vec:: AllocInit::Zeroed => { close array_at_lft(alloc_id.lft, ptr_, 0, []); }
1609+ AllocInit::Uninitialized => { close array_at_lft_(alloc_id.lft, ptr_, 0, []); }
1610+ AllocInit::Zeroed => { close array_at_lft(alloc_id.lft, ptr_, 0, []); }
16091611 }
16101612 @*/
16111613 return Ok ( r) ;
@@ -1684,8 +1686,8 @@ impl<A: Allocator> RawVecInner<A> {
16841686 cap : unsafe { Cap :: new_unchecked ( capacity) } ,
16851687 alloc,
16861688 } ;
1687- //@ std::alloc::alloc_block_in_aligned(ptr.ptr. as_ptr());
1688- //@ close RawVecInner(t, res, elem_layout, alloc_id, ptr.ptr. as_ptr(), _);
1689+ //@ std::alloc::alloc_block_in_aligned(ptr.as_ptr() as *u8 );
1690+ //@ close RawVecInner(t, res, elem_layout, alloc_id, ptr.as_ptr() as *u8 , _);
16891691 Ok ( res)
16901692 }
16911693
@@ -1936,7 +1938,6 @@ impl<A: Allocator> RawVecInner<A> {
19361938 <std::collections::TryReserveError>.own(t, e)
19371939 };
19381940 @*/
1939- //@ safety_proof { assume(false); } // This function should be marked `unsafe`; see https://github.com/rust-lang/rust/pull/145067
19401941 {
19411942 //@ let k = begin_lifetime();
19421943 //@ share_RawVecInner(k, self);
@@ -2019,7 +2020,6 @@ impl<A: Allocator> RawVecInner<A> {
20192020 <std::collections::TryReserveError>.own(t, e)
20202021 };
20212022 @*/
2022- //@ safety_proof { assume(false); } // This function should be marked `unsafe`; see https://github.com/rust-lang/rust/pull/145067
20232023 {
20242024 //@ let k = begin_lifetime();
20252025 //@ share_RawVecInner(k, self);
@@ -2100,9 +2100,9 @@ impl<A: Allocator> RawVecInner<A> {
21002100 #[ inline]
21012101 unsafe fn set_ptr_and_cap ( & mut self , ptr : NonNull < [ u8 ] > , cap : usize )
21022102 //@ req (*self).ptr |-> _ &*& (*self).cap |-> _ &*& cap <= isize::MAX;
2103- //@ ens (*self).ptr |-> Unique::from_non_null::<u8>(ptr.ptr ) &*& (*self).cap |-> UsizeNoHighBit::new(cap);
2103+ //@ ens (*self).ptr |-> Unique::from_non_null::<u8>(ptr.as_non_null_ptr() ) &*& (*self).cap |-> UsizeNoHighBit::new(cap);
21042104 {
2105- //@ std::ptr::NonNull_new_as_ptr(ptr.ptr );
2105+ //@ std::ptr::NonNull_new_as_ptr(ptr.as_non_null_ptr() );
21062106 // Allocators currently return a `NonNull<[u8]>` whose length matches
21072107 // the size requested. If that ever changes, the capacity here should
21082108 // change to `ptr.len() / size_of::<T>()`.
@@ -2144,7 +2144,6 @@ impl<A: Allocator> RawVecInner<A> {
21442144 <std::collections::TryReserveError>.own(t, e)
21452145 };
21462146 @*/
2147- //@ safety_proof { assume(false); } // This function should be marked `unsafe`; see https://github.com/rust-lang/rust/pull/145067
21482147 {
21492148 // This is ensured by the calling contexts.
21502149 if cfg ! ( debug_assertions) { //~allow_dead_code // FIXME: The source location associated with a dead `else` branch is the entire `if` statement :-(
@@ -2229,7 +2228,7 @@ impl<A: Allocator> RawVecInner<A> {
22292228 unsafe {
22302229 self . set_ptr_and_cap ( ptr, cap) ;
22312230 //@ let self1 = *self;
2232- //@ std::alloc::alloc_block_in_aligned(ptr.ptr. as_ptr());
2231+ //@ std::alloc::alloc_block_in_aligned(ptr.as_ptr() as *u8 );
22332232 //@ std::num::niche_types::UsizeNoHighBit_as_inner_new(cap);
22342233 //@ mul_zero(elem_layout.size(), cap);
22352234 //@ assert 0 <= self0.cap.as_inner();
@@ -2277,7 +2276,6 @@ impl<A: Allocator> RawVecInner<A> {
22772276 <std::collections::TryReserveError>.own(t, e)
22782277 };
22792278 @*/
2280- //@ safety_proof { assume(false); } // This function should be marked `unsafe`; see https://github.com/rust-lang/rust/pull/145067
22812279 {
22822280 if elem_layout. size ( ) == 0 {
22832281 // Since we return a capacity of `usize::MAX` when the type size is
@@ -2348,7 +2346,7 @@ impl<A: Allocator> RawVecInner<A> {
23482346 //@ mul_mono_l(1, elem_layout.size(), cap);
23492347 self . set_ptr_and_cap ( ptr, cap) ;
23502348 //@ let self1 = *self;
2351- //@ std::alloc::alloc_block_in_aligned(ptr.ptr. as_ptr());
2349+ //@ std::alloc::alloc_block_in_aligned(ptr.as_ptr() as *u8 );
23522350 //@ std::num::niche_types::UsizeNoHighBit_as_inner_new(cap);
23532351 //@ mul_zero(elem_layout.size(), cap);
23542352 //@ assert 0 <= self0.cap.as_inner();
@@ -2537,7 +2535,7 @@ impl<A: Allocator> RawVecInner<A> {
25372535 unsafe {
25382536 //@ std::num::niche_types::UsizeNoHighBit_inv(self01.cap);
25392537 self . set_ptr_and_cap ( ptr, cap) ;
2540- //@ std::alloc::alloc_block_in_aligned(ptr_1.ptr. as_ptr());
2538+ //@ std::alloc::alloc_block_in_aligned(ptr_1.as_ptr() as *u8 );
25412539 //@ mul_zero(cap, elem_layout.size());
25422540 //@ std::alloc::Layout_repeat_size_aligned_intro(elem_layout, cap);
25432541 //@ close RawVecInner(t, *self, elem_layout, alloc_id, _, _);
@@ -2631,8 +2629,8 @@ req thread_token(?t) &*& t == currentThread &*&
26312629ens thread_token(t) &*& *alloc |-> ?alloc1 &*& Allocator(t, alloc1, alloc_id) &*&
26322630 match result {
26332631 Result::Ok(ptr) =>
2634- alloc_block_in(alloc_id, ptr.ptr. as_ptr(), new_layout) &*&
2635- array_at_lft_(alloc_id.lft, ptr.ptr. as_ptr(), new_layout.size(), _) &*&
2632+ alloc_block_in(alloc_id, ptr.as_ptr() as *u8 , new_layout) &*&
2633+ array_at_lft_(alloc_id.lft, ptr.as_ptr() as *u8 , new_layout.size(), _) &*&
26362634 new_layout.size() <= isize::MAX,
26372635 Result::Err(e) =>
26382636 match current_memory {
@@ -2644,7 +2642,6 @@ ens thread_token(t) &*& *alloc |-> ?alloc1 &*& Allocator(t, alloc1, alloc_id) &*
26442642 <std::collections::TryReserveError>.own(currentThread, e)
26452643 };
26462644@*/
2647- //@ safety_proof { assume(false); } // This function should be marked `unsafe`; see https://github.com/rust-lang/rust/pull/145067
26482645{
26492646 let memory = if let Some ( ( ptr, old_layout) ) = current_memory {
26502647 // debug_assert_eq!(old_layout.align(), new_layout.align());
0 commit comments