Fix atomic compare_exchange to return correct failure status

[tautschnig]

Fix codegen_atomic_cxchg to properly return (current_value, false) when the expected value doesn't match the current value. Previously, the function always returned true as the success indicator, which was incorrect.

Resolves #4537

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[Copilot]

Pull request overview

This PR fixes the lowering of atomic compare-and-exchange intrinsics in the Kani Goto-C backend so that failed compare_exchange/compare_exchange_weak operations correctly report failure (i.e., return the old value with a false success flag), matching Rust’s semantics and resolving #4537.

Changes:

• Fix codegen_atomic_cxchg to return (previous_value, success) instead of always returning success.
• Add regression tests ensuring compare_exchange and compare_exchange_weak return Err(old) when the expected value does not match.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

File	Description
kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs	Corrects the emitted compare-and-exchange code to compute and return the real success flag.
tests/kani/Intrinsics/Atomic/Stable/CompareExchange/compare_exchange_failure.rs	Adds proof harnesses covering failure behavior for compare_exchange and compare_exchange_weak.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.