Skip to content

Commit f4d4a94

Browse files
authored
Upgrade Rust toolchain to 2025-11-16 (#4477)
Relevant upstream PR: - rust-lang/rust#148789 (New format_args!() and fmt::Arguments implementation) Resolves: #4474 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 5c2da86 commit f4d4a94

File tree

4 files changed

+11
-12
lines changed

4 files changed

+11
-12
lines changed

rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2025-11-13"
5+
channel = "nightly-2025-11-17"
66
components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/coverage/known_issues/variant/expected

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,30 +1,30 @@
11
1| | // Copyright Kani Contributors\
22
2| | // SPDX-License-Identifier: Apache-2.0 OR MIT\
3-
3| | \
3+
3| |\
44
4| | //! Checks coverage results in an example with a `match` statement matching on\
55
5| | //! all enum variants. Currently, it does not yield the expected results because\
66
6| | //! it reports the `dir` in the match statement as `UNCOVERED`:\
77
7| | //! <https://github.com/model-checking/kani/issues/3456>\
8-
8| | \
8+
8| |\
99
9| | enum Direction {\
1010
10| | Up,\
1111
11| | Down,\
1212
12| | Left,\
1313
13| | Right,\
1414
14| | }\
15-
15| | \
15+
15| |\
1616
16| 1| fn print_direction(dir: Direction) {\
1717
17| | // For some reason, `dir`'s span is reported as `UNCOVERED` too\
1818
18| 0| match ```dir''' {\
19-
19| 0| Direction::Up => ```println!("Going up!"'''),\
20-
20| 0| Direction::Down => ```println!("Going down!"'''),\
19+
19| 0| Direction::Up => ```println!'''("Going up!"),\
20+
20| 0| Direction::Down => ```println!'''("Going down!"),\
2121
21| 1| Direction::Left => println!("Going left!"),\
22-
22| 0| Direction::Right if 1 == ```1 => println!("Going right!"'''),\
22+
22| 0| Direction::Right if 1 == ```1 => println!'''("Going right!"),\
2323
23| | // This part is unreachable since we cover all variants in the match.\
24-
24| 0| _ => ```println!("Not going anywhere!"'''),\
24+
24| 0| _ => ```println!'''("Not going anywhere!"),\
2525
25| | }\
2626
26| | }\
27-
27| | \
27+
27| |\
2828
28| | #[kani::proof]\
2929
29| 1| fn main() {\
3030
30| 1| let direction = Direction::Left;\
Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
.assertion\
1+
__CPROVER_contracts_\
22
- Status: SUCCESS\
3-
- Description: "ptr NULL or writable up to size"\
43

54
VERIFICATION:- SUCCESSFUL

tests/expected/panic/arg-error/test.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
//! This test checks that Kani processes arguments of panic macros and produces
66
//! a compile error for invalid arguments (e.g. missing argument)
77
8-
const fn my_const_fn(msg: &str) -> ! {
8+
fn my_const_fn(msg: &str) -> ! {
99
core::panic!("{}")
1010
}
1111

0 commit comments

Comments
 (0)