Upgrade Rust toolchain to nightly-2026-08-01

[feliperodri]

Description

Bumps rust-toolchain.toml from nightly-2026-07-01 to nightly-2026-08-01, the first 1.99 nightly. 91 compile errors came with it.

1. Statement/Terminator carry a SourceInfo, not a bare Span (78 of the 91 errors)

// nightly-2026-07-01
pub struct Statement<'tcx> { pub source_info: SourceInfo, .. }   // Terminator: span only
// nightly-2026-08-01 -- both carry SourceInfo (span + source scope)

A new helper in transform/body.rs keeps the choice of scope in one documented place rather than spreading a bare scope: 0 across ~78 sites:

/// The `SourceInfo` for a statement or terminator that Kani synthesizes at `span`.
///
/// As of nightly-2026-08-01 `Statement` and `Terminator` carry a `SourceInfo` (span plus source
/// scope) instead of a bare `Span`. Kani-synthesized MIR does not belong to any inlined scope, so
/// it uses the outermost one -- scope 0, which `Body::new` always allocates.
pub fn synthetic_source_info(span: Span) -> SourceInfo {
    SourceInfo { span, scope: 0 }
}

Reads become .source_info.span.

2. predicates_of became clauses_of

Returns GenericClauses (parent + clauses) instead of GenericPredicates (parent + predicates). Same shape and same instantiate, so this is a rename at four call sites — three in codegen_units.rs from #4706/#4718, one in the LLBC backend.

3. ty::FnDef's generic args are bound

Three Instance::{try,expect}_resolve call sites need .skip_binder().

4. ValueAbi::ScalarPair became a struct variant

With a new b_offset field.

5. Two new enum variants

• AssertMessage::NullReferenceConstructed — handled like NullPointerDereference: same property class, description taken from rustc_public rather than hardcoded.
• InstanceKind::LlvmIntrinsic — codegens like any other item, and has no Rust body for reachability to collect.

Plus LocalModDefId renamed to LocalModId, and Region::new_early_param moving to the RegionExt extension trait.

Test changes (5 files)

std::intrinsics::{size_of,align_of} are now comptime fns and cannot be called at runtime, which affected four tests:

• tests/kani/DynTrait/{nested_boxes,vtable_size_align_drop}.rs used size_of incidentally, to compare a vtable field against a type's size — switched to std::mem::size_of.
• tests/kani/Intrinsics/ConstEval/{size_of,align_of}.rs exist to check the intrinsics themselves, so each call is bound to a const — which is what that directory is about, and the only way now legal.

expected/issue-3571 — a genuine behaviour change worth flagging. Constructing a null reference (&*(0 as *const u32)) used to report null pointer dereference occurred; rustc now distinguishes constructing a null reference from dereferencing a null pointer and reports null reference produced. rustc also emits a new misaligned pointer to reference cast check at the same site. The UB is still caught and the harness still fails — only the wording is more precise — so the expectation follows rustc's message rather than pinning the old one.

No other test needed adjusting, and no verification behaviour changed.

Testing

Local, macOS aarch64, CBMC 6.10.0 (cbmc-6.9.0-214-g45436eea34), on the stack rebased onto current main (which now includes #4760):

Suite	Result
kani	607 passed, 0 failed
cargo-kani	71 passed, 0 failed
cargo-ui	30 passed, 0 failed
expected	471 passed, 2 failed — see below
ui	151 passed, 2 failed — environmental, see below

Also clean: both the CPROVER and LLBC builds, cargo clippy --workspace --tests -- -D warnings, RUSTFLAGS="--cfg=kani_sysroot" cargo clippy --workspace -- -D warnings, and ./scripts/kani-fmt.sh --check.

The two expected failures were run before the fix above and are accounted for:

• expected/issue-3571 — the null-reference wording change; fixed in this PR, verified passing.
• expected/shadow/slices/slice_split — I interrupted this one to let the suite finish. It is not an 08-01 regression: I timed it on the 07-01 branch as a control and it is equally slow there (>20 min in CBMC's SAT solver on both), so it is a slow test on this machine rather than anything this upgrade introduced. CI covers it.

The two ui failures are solver-attribute/cadical and solver-option/cadical, both expecting Solving with CaDiCaL. My local CBMC build reports The specified solver, 'cadical', is not available. The default solver will be used instead. — a missing solver in my environment, independent of the Rust toolchain.

• Was this change tested? Yes
• Is this a breaking change? No

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