Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

A crash when calling a closure with a struct involving the never type #3034

Closed
zhassan-aws opened this issue Feb 20, 2024 · 0 comments · Fixed by #3040
Closed

A crash when calling a closure with a struct involving the never type #3034

zhassan-aws opened this issue Feb 20, 2024 · 0 comments · Fixed by #3040
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed Z-Kani Compiler Issues that require some changes to the compiler

Comments

@zhassan-aws
Copy link
Contributor

I tried this code:

#![feature(never_type)]

pub struct Foo {
    _x: i32,
    _never: !,
}

#[cfg_attr(kani, kani::proof)]
fn main() {
    let res = Result::<i32, Foo>::Ok(3);
    let _x = res.unwrap_or_else(|_f| 5);
}

using the following command line invocation:

kani nv.rs

with Kani version: 6bea131

I expected to see this happen: Verification passes

Instead, this happened:

$ kani nv.rs 
Kani Rust Verifier 0.46.0 (standalone)
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:689:9:
Function call does not type check:
func params: []
args: [Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_RINvMNtCs4A47zemGJJh_4core6resultINtB3_6ResultlNtCslwEuWiA9yWG_2nv3FooE14unwrap_or_elseNCNvBL_4main0EBL_::1::var_7" }, typ: StructTag("tag-_133682644016529668577290331323904023019"), location: None, size_of_annotation: None }, field: "0" }, typ: StructTag("tag-_247671360278137032517711891165892296272"), location: None, size_of_annotation: None }]
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: std::result::Result::<i32, Foo>::unwrap_or_else::<{[email protected]:11:33: 11:37}>
_RINvMNtCs4A47zemGJJh_4core6resultINtB3_6ResultlNtCslwEuWiA9yWG_2nv3FooE14unwrap_or_elseNCNvBL_4main0EBL_
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2024-02-09-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs", function: None, start_line: 1423, start_col: Some(5), end_line: 1423, end_col: Some(63) }
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101
@zhassan-aws zhassan-aws added [C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed Z-Kani Compiler Issues that require some changes to the compiler labels Feb 20, 2024
zhassan-aws added a commit to zhassan-aws/kani that referenced this issue Feb 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed Z-Kani Compiler Issues that require some changes to the compiler
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant