You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
109
89
--> RUSTLIB/alloc/src/sync.rs:LL:CC
110
90
|
@@ -122,23 +102,6 @@ note: inside `main`
122
102
LL | t0.join().unwrap();
123
103
| ^^^^^^^^^
124
104
125
-
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.
126
-
--> RUSTLIB/alloc/src/sync.rs:LL:CC
127
-
|
128
-
LL | if this.inner().weak.compare_exchange(1, usize::MAX, Acquire, Relaxed).is_ok() {
129
-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ GenMC might miss possible behaviors of this code
130
-
|
131
-
= note: BACKTRACE:
132
-
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::is_unique` at RUSTLIB/alloc/src/sync.rs:LL:CC
133
-
= note: inside `std::sync::Arc::<std::thread::Packet<'_, ()>>::get_mut` at RUSTLIB/alloc/src/sync.rs:LL:CC
134
-
= note: inside `std::thread::JoinInner::<'_, ()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
135
-
= note: inside `std::thread::JoinHandle::<()>::join` at RUSTLIB/std/src/thread/mod.rs:LL:CC
Copy file name to clipboardExpand all lines: tests/genmc/pass/intercept/mutex_poison.stderr
-44Lines changed: 0 additions & 44 deletions
Original file line number
Diff line number
Diff line change
@@ -61,50 +61,6 @@ LL | | panic!(); // This will poison the mutex.
61
61
LL | | });
62
62
| |______^
63
63
64
-
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.
0 commit comments