Pass function for `Thread` as `Send` to `Thread::imp` · model-checking/verify-rust-std@92b604f (original) (raw)

`@@ -561,7 +561,8 @@ impl Builder {

561

`let main = Box::new(main);

562

`// SAFETY: dynamic size and alignment of the Box remain the same. See below for why the

563

`// lifetime change is justified.

564

let main = unsafe { Box::from_raw(Box::into_raw(main) as *mut (dyn FnOnce() + 'static)) };

564

let main =

565

unsafe { Box::from_raw(Box::into_raw(main) as *mut (dyn FnOnce() + Send + 'static)) };

565

566

567

`Ok(JoinInner {

567

568

`// SAFETY:

`@@ -1544,7 +1545,7 @@ struct Packet<'scope, T> {

1544

1545

`` // The type T should already always be Send (otherwise the thread could not

1545

1546

`// have been created) and the Packet is Sync because all access to the

1546

1547

`` // UnsafeCell synchronized (by the join() boundary), and ScopeData is Sync.

1547

unsafe impl<'scope, T: Sync> Sync for Packet<'scope, T> {}

1548

unsafe impl<'scope, T: Send> Sync for Packet<'scope, T> {}

1548

1549

1550

`impl<'scope, T> Drop for Packet<'scope, T> {

1550

1551

`fn drop(&mut self) {

Pass function for Thread as Send to Thread::imp · model-checking/verify-rust-std@92b604f (original) (raw)