From eb908b8cdbb9bec2e53ceea40e97ce8caa919476 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 17 Nov 2025 12:09:33 +0000 Subject: [PATCH] Upgrade Rust toolchain to 2025-11-16 Relevant upstream PR: - https://github.com/rust-lang/rust/pull/148789 (New format_args!() and fmt::Arguments implementation) Resolves: #4474 --- rust-toolchain.toml | 2 +- tests/coverage/known_issues/variant/expected | 16 ++++++++-------- .../function-contract/modifies/zst_pass.expected | 3 +-- tests/expected/panic/arg-error/test.rs | 2 +- 4 files changed, 11 insertions(+), 12 deletions(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0791fdfc4aa0..0055275b02f9 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2025-11-13" +channel = "nightly-2025-11-17" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/coverage/known_issues/variant/expected b/tests/coverage/known_issues/variant/expected index a42769c39f40..715a5440e0ae 100644 --- a/tests/coverage/known_issues/variant/expected +++ b/tests/coverage/known_issues/variant/expected @@ -1,30 +1,30 @@ 1| | // Copyright Kani Contributors\ 2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\ - 3| | \ + 3| |\ 4| | //! Checks coverage results in an example with a `match` statement matching on\ 5| | //! all enum variants. Currently, it does not yield the expected results because\ 6| | //! it reports the `dir` in the match statement as `UNCOVERED`:\ 7| | //! \ - 8| | \ + 8| |\ 9| | enum Direction {\ 10| | Up,\ 11| | Down,\ 12| | Left,\ 13| | Right,\ 14| | }\ - 15| | \ + 15| |\ 16| 1| fn print_direction(dir: Direction) {\ 17| | // For some reason, `dir`'s span is reported as `UNCOVERED` too\ 18| 0| match ```dir''' {\ - 19| 0| Direction::Up => ```println!("Going up!"'''),\ - 20| 0| Direction::Down => ```println!("Going down!"'''),\ + 19| 0| Direction::Up => ```println!'''("Going up!"),\ + 20| 0| Direction::Down => ```println!'''("Going down!"),\ 21| 1| Direction::Left => println!("Going left!"),\ - 22| 0| Direction::Right if 1 == ```1 => println!("Going right!"'''),\ + 22| 0| Direction::Right if 1 == ```1 => println!'''("Going right!"),\ 23| | // This part is unreachable since we cover all variants in the match.\ - 24| 0| _ => ```println!("Not going anywhere!"'''),\ + 24| 0| _ => ```println!'''("Not going anywhere!"),\ 25| | }\ 26| | }\ - 27| | \ + 27| |\ 28| | #[kani::proof]\ 29| 1| fn main() {\ 30| 1| let direction = Direction::Left;\ diff --git a/tests/expected/function-contract/modifies/zst_pass.expected b/tests/expected/function-contract/modifies/zst_pass.expected index ba2a8eb7decd..ba0e5dba530f 100644 --- a/tests/expected/function-contract/modifies/zst_pass.expected +++ b/tests/expected/function-contract/modifies/zst_pass.expected @@ -1,5 +1,4 @@ -.assertion\ +__CPROVER_contracts_\ - Status: SUCCESS\ -- Description: "ptr NULL or writable up to size"\ VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/panic/arg-error/test.rs b/tests/expected/panic/arg-error/test.rs index 504dcf87c481..78c6c8a591d2 100644 --- a/tests/expected/panic/arg-error/test.rs +++ b/tests/expected/panic/arg-error/test.rs @@ -5,7 +5,7 @@ //! This test checks that Kani processes arguments of panic macros and produces //! a compile error for invalid arguments (e.g. missing argument) -const fn my_const_fn(msg: &str) -> ! { +fn my_const_fn(msg: &str) -> ! { core::panic!("{}") }