Open matthiaskrgr opened 1 year ago
This following program is sufficient to produce a crash:
#[kani::proof]
fn main() {
struct Foo(u32);
let f1 = Foo(0x600);
}
when run as follows:
$ RUSTFLAGS="-Zmir-opt-level=2" kani iss2725.rs
Kani Rust Verifier 0.35.0 (standalone)
warning: unused variable: `f1`
--> iss2725.rs:4:9
|
4 | let f1 = Foo(0x600);
| ^^ help: if this is intentional, prefix it with an underscore: `_f1`
|
= note: `#[warn(unused_variables)]` on by default
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs:54:17:
Unhandled VarDebugInfoContents::Composite
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: main
main
[Kani] current codegen location: Loc { file: "/home/ubuntu/examples/iss2725.rs", function: None, start_line: 2, start_col: Some(1), end_line: 2, end_col: Some(10) }
warning: 1 warning emitted
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101
This crash is different from the original one though (requires handling VarDebugInfoContents::Composite
here).
triage: still crashing with 0.40
I tried this code:
using the following command line invocation:
with Kani version: 0.35.0
I expected to see this happen: explanation
Instead, this happened: explanation