Rustup

rust-version

@@ -1 +1 @@
-402ce0ef07d5db9ba26ae5c37ce6aff0c9002052
+96fe3c31c2ec385f3d3263346bcdde3d118cdaf6

tests/genmc/pass/std/arc.check_count.stderr

@@ -6,20 +6,8 @@ LL |                 intrinsics::atomic_cxchgweak::<T, { AO::Relaxed }, { AO::Re
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u64>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
-   = note: inside `std::sync::atomic::AtomicU64::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
-   = note: inside `std::thread::ThreadId::new` at RUSTLIB/std/src/thread/mod.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/thread/current.rs:LL:CC
-   = note: inside `std::option::Option::<std::thread::ThreadId>::unwrap_or_else::<{closure@std::thread::current::id::get_or_init::{closure#0}}>` at RUSTLIB/core/src/option.rs:LL:CC
-   = note: inside `std::thread::current::id::get_or_init` at RUSTLIB/std/src/thread/current.rs:LL:CC
-   = note: inside `std::thread::current_id` at RUSTLIB/std/src/thread/current.rs:LL:CC
-   = note: inside `std::rt::init` at RUSTLIB/std/src/rt.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
-   = note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
-   = note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
-   = note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
-   = note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
-   = note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
 
 warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
   --> RUSTLIB/alloc/src/sync.rs:LL:CC
@@ -28,7 +16,6 @@ LL |             match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acq
    |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
 note: inside `main`
   --> tests/genmc/pass/std/arc.rs:LL:CC
    |
@@ -42,7 +29,6 @@ LL |             match this.inner().weak.compare_exchange_weak(cur, cur + 1, Acq
    |                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sync::Arc::<i32>::downgrade` at RUSTLIB/alloc/src/sync.rs:LL:CC
 note: inside `main`
   --> tests/genmc/pass/std/arc.rs:LL:CC
    |
@@ -59,15 +45,7 @@ LL | |                 .compare_exchange_weak(state, state + READ_LOCKED, Acquir
    | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
-   = note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
-   = note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
-   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
-   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
-   = note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
-   = note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
-   = note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
 note: inside `main`
   --> tests/genmc/pass/std/arc.rs:LL:CC
@@ -88,15 +66,7 @@ LL | |                 .compare_exchange_weak(state, state + READ_LOCKED, Acquir
    | |____________________________________________________________________________________^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sys::sync::PLATFORM::futex::RwLock::read` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
-   = note: inside `std::sync::RwLock::<()>::read` at RUSTLIB/std/src/sync/poison/rwlock.rs:LL:CC
-   = note: inside `std::sys::env::PLATFORM::env_read_lock` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
-   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr_stack::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
-   = note: inside `std::sys::pal::PLATFORM::small_c_string::run_with_cstr::<std::option::Option<std::ffi::OsString>>` at RUSTLIB/std/src/sys/pal/PLATFORM/small_c_string.rs:LL:CC
-   = note: inside `std::sys::env::PLATFORM::getenv` at RUSTLIB/std/src/sys/env/PLATFORM.rs:LL:CC
-   = note: inside `std::env::_var_os` at RUSTLIB/std/src/env.rs:LL:CC
-   = note: inside `std::env::var_os::<&str>` at RUSTLIB/std/src/env.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/thread/mod.rs:LL:CC
 note: inside `main`
   --> tests/genmc/pass/std/arc.rs:LL:CC
@@ -114,10 +84,6 @@ LL |         if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relax
    |            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
-   = note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
-   = note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
-   = note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
 note: inside `main`
   --> tests/genmc/pass/std/arc.rs:LL:CC
    |
@@ -131,17 +97,7 @@ LL |                 intrinsics::atomic_cxchgweak::<T, { AO::Acquire }, { AO::Ac
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sync::atomic::atomic_compare_exchange_weak::<u32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
-   = note: inside `std::sync::atomic::AtomicU32::compare_exchange_weak` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
-   = note: inside `std::sys::sync::PLATFORM::futex::Once::call` at RUSTLIB/std/src/sys/sync/PLATFORM/futex.rs:LL:CC
-   = note: inside `std::sync::Once::call_once::<{closure@std::rt::cleanup::{closure#0}}>` at RUSTLIB/std/src/sync/poison/once.rs:LL:CC
-   = note: inside `std::rt::cleanup` at RUSTLIB/std/src/rt.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
-   = note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
-   = note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
-   = note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
-   = note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
-   = note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
 
 warning: GenMC currently does not model the failure ordering for `compare_exchange`. Due to success ordering 'Acquire', the failure ordering 'Relaxed' is treated like 'Acquire'. Miri with GenMC might miss bugs related to this memory access.
   --> RUSTLIB/core/src/sync/atomic.rs:LL:CC
@@ -150,14 +106,6 @@ LL |                 intrinsics::atomic_cxchg::<T, { AO::Acquire }, { AO::Relaxe
    |                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
    |
    = note: BACKTRACE:
-   = note: inside `std::sync::atomic::atomic_compare_exchange::<*mut i32>` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
-   = note: inside `std::sync::atomic::AtomicPtr::<i32>::compare_exchange` at RUSTLIB/core/src/sync/atomic.rs:LL:CC
-   = note: inside `std::sys::exit_guard::unique_thread_exit` at RUSTLIB/std/src/sys/exit_guard.rs:LL:CC
    = note: inside closure at RUSTLIB/std/src/rt.rs:LL:CC
-   = note: inside `std::panicking::catch_unwind::do_call::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panicking.rs:LL:CC
-   = note: inside `std::panicking::catch_unwind::<isize, {closure@std::rt::lang_start_internal::{closure#0}}>` at RUSTLIB/std/src/panicking.rs:LL:CC
-   = note: inside `std::panic::catch_unwind::<{closure@std::rt::lang_start_internal::{closure#0}}, isize>` at RUSTLIB/std/src/panic.rs:LL:CC
-   = note: inside `std::rt::lang_start_internal` at RUSTLIB/std/src/rt.rs:LL:CC
-   = note: inside `std::rt::lang_start::<()>` at RUSTLIB/std/src/rt.rs:LL:CC
 
 Verification complete with 4 executions. No errors found.

tests/genmc/pass/std/arc.rs

@@ -1,5 +1,6 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
 //@revisions: check_count try_upgrade
+//@normalize-stderr-test: "\n *= note: inside `std::.*" -> ""
 
 // Check that various operations on `std::sync::Arc` are handled properly in GenMC mode.
 //