These are the original release notes for the reference:

## What's Changed
* Automatic cargo update to 2024-02-26 by @github-actions in
#3043
* Upgrade rust toolchain to 2024-02-17 by @celinval in
#3040
* Upgrade `windows-targets` crate to version 0.52.4 by @adpaco-aws in
#3049
* Fix `codegen_atomic_binop` for `atomic_ptr` by @qinheping in
#3047
* Upgrade Rust toolchain to `nightly-2024-02-25` by @adpaco-aws in
#3048
* Update s2n-quic submodule by @zhassan-aws in
#3050
* Update s2n-quic submodule weekly through dependabot by @zhassan-aws in
#3053
* Retrieve info for recursion tracker reliably by @feliperodri in
#3045
* Automatic cargo update to 2024-03-04 by @github-actions in
#3055
* Upgrade Rust toolchain to `nightly-2024-03-01` by @adpaco-aws in
#3052
* Add `--use-local-toolchain` to Kani setup by @jaisnan in
#3056
* Replace internal reverse_postorder by a stable one by @celinval in
#3064
* Add option to override `--crate-name` from `kani` by @adpaco-aws in
#3054
* cargo update and fix macos CI by @zhassan-aws in
#3067
* Bump tests/perf/s2n-quic from `d103836` to `1a7faa8` by @dependabot in
#3066
* Upgrade toolchain to 2024-03-11 by @zhassan-aws in
#3071
* Emit `dead` goto-instructions on MIR StatementDead by @karkhaz in
#3063


**Full Changelog**:
kani-0.47.0...kani-0.48.0

Culprit PR: rust-lang/rust#144192

The upstream PR adds a new generic argument `U` for some atomic
intrinsics, so our tests need to include those.

Solely changing the tests to infer the generic argument makes
compilation succeed, but [this `atomic_xor`
harness](https://github.com/model-checking/kani/blob/41849d25092483d1dd92d472cc8c457908903927/tests/kani/Intrinsics/Atomic/Stable/AtomicPtr/main.rs#L70)
fails with this error:

```
thread 'rustc' (1068557) panicked at cprover_bindings/src/goto_program/expr.rs:1147:9:
BinaryOperation Expression does not typecheck 
Bitor 
Expr { value: Dereference(Expr { value: Symbol { identifier: "_RINvNtNtCslIVxtpUQXYK_4core4sync6atomic9atomic_orOxjECs63P9ci4LCSm_4main::1::var_1::dst" }, typ: Pointer { typ: Pointer { typ: Signedbv { width: 64 } } }, location: None, size_of_annotation: None }), typ: Pointer { typ: Signedbv { width: 64 } }, location: None, size_of_annotation: None } 
Expr { value: Symbol { identifier: "_RINvNtNtCslIVxtpUQXYK_4core4sync6atomic9atomic_orOxjECs63P9ci4LCSm_4main::1::var_2::val" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::sync::atomic::atomic_or::<*mut i64, usize>
_RINvNtNtCslIVxtpUQXYK_4core4sync6atomic9atomic_orOxjECs63P9ci4LCSm_4main
[Kani] current codegen location: Loc { file: "/Users/cmzech/.rustup/toolchains/nightly-2025-08-10-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs", function: None, start_line: 4183, start_col: Some(1), end_line: 4183, end_col: Some(81), pragmas: [] }
```

This happens because `codegen_atomic_binop` currently handles the case
where `T` is a pointer by checking if `var2` is a pointer, then casting
`var1` and `var2` to `size_t`:

https://github.com/model-checking/kani/blob/41849d25092483d1dd92d472cc8c457908903927/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs#L241-L245
But rust-lang/rust#144192 makes this change to
`fetch_xor`:

```diff
diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs
index 546f3d91a80..44a6895f90a 100644
--- a/library/core/src/sync/atomic.rs
+++ b/library/core/src/sync/atomic.rs
     pub fn fetch_xor(&self, val: usize, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
-        unsafe { atomic_xor(self.p.get(), core::ptr::without_provenance_mut(val), order).cast() }
+        unsafe { atomic_xor(self.p.get(), val, order).cast() }
     }
 
```
since `var2` is no longer a pointer, we hit the else case, and thus the
solution from #3047 no longer
takes effect.

The solution is to instead check if `var1` is a pointer. We also remove
the cast of `var2` to a size_t, since per the new documentation:

> `U` must be the same as `T` if that is an integer type, or `usize` if
`T` is a pointer type.

`U` is guaranteed to be a `usize` if `T` is a pointer, and we [codegen
usizes as `size_t`s
already](https://github.com/model-checking/kani/blob/41849d25092483d1dd92d472cc8c457908903927/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs#L713
).

Resolves #4284

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