Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
16 changes: 8 additions & 8 deletions tests/coverage/known_issues/variant/expected
Original file line number Diff line number Diff line change
@@ -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| | //! <https://github.com/model-checking/kani/issues/3456>\
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;\
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
.assertion\
__CPROVER_contracts_\
- Status: SUCCESS\
- Description: "ptr NULL or writable up to size"\

VERIFICATION:- SUCCESSFUL
2 changes: 1 addition & 1 deletion tests/expected/panic/arg-error/test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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!("{}")
}

Expand Down
Loading