We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
I tried this code:
#[kani::proof] fn main() { let f: fn() -> ! = || std::process::exit(0); f(); }
using the following command line invocation:
kani file.rs
with Kani version: kani 0.29.0 I expected to see this happen: explanation
kani 0.29.0
Instead, this happened: explanation
thread 'rustc' panicked at 'called `Option::unwrap()` on a `None` value', kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:586:73 stack backtrace: 0: 0x7f1c7b368cc3 - std::backtrace_rs::backtrace::libunwind::trace::h6dd260ccf76e2a16 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x7f1c7b368cc3 - std::backtrace_rs::backtrace::trace_unsynchronized::h60e795a392c2d181 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x7f1c7b368cc3 - std::sys_common::backtrace::_print_fmt::hb92bc719d8e89e18 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:65:5 3: 0x7f1c7b368cc3 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h433d7296fbd4df36 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:44:22 4: 0x7f1c7b3c9c0f - core::fmt::rt::Argument::fmt::hee863a126433a5fe at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/rt.rs:138:9 5: 0x7f1c7b3c9c0f - core::fmt::write::hecf019f127565c17 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/mod.rs:1105:21 6: 0x7f1c7b35bd91 - std::io::Write::write_fmt::h4fdee205f020a023 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/io/mod.rs:1712:15 7: 0x7f1c7b368ad5 - std::sys_common::backtrace::_print::h63f1eb292c01c01d at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:47:5 8: 0x7f1c7b368ad5 - std::sys_common::backtrace::print::h29fa6d106f41082b at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:34:9 9: 0x7f1c7b36b697 - std::panicking::default_hook::{{closure}}::h24c419639c3568dd 10: 0x7f1c7b36b485 - std::panicking::default_hook::hd5faae45a4c2ae6b at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:288:9 11: 0x564149948dfd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62fc73136c5344f5 12: 0x564149975d83 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::he03976a598c31555 13: 0x7f1c7b36bdd5 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h8fd551c79732d109 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1976:9 14: 0x7f1c7b36bdd5 - std::panicking::rust_panic_with_hook::hff0f13fd32920cda at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:695:13 15: 0x7f1c7b36bb02 - std::panicking::begin_panic_handler::{{closure}}::h4b94c172e12e7b79 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:580:13 16: 0x7f1c7b369106 - std::sys_common::backtrace::__rust_end_short_backtrace::h0d54fda82a2d0073 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:150:18 17: 0x7f1c7b36b8a2 - rust_begin_unwind at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:578:5 18: 0x7f1c7b3c5eb3 - core::panicking::panic_fmt::h423e755c13523a61 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:67:14 19: 0x7f1c7b3c5f4d - core::panicking::panic::ha60b73a9d89a544c at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:117:5 20: 0x5641498f5a44 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::hdccc300bfe0c600c 21: 0x5641499070a1 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h976e66498994fa63 22: 0x56414993173e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h72b866e5cefa4cb6 23: 0x5641499356d1 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd63a249ce3b650de 24: 0x7f1c7d7e4e26 - rustc_interface[bc622c2a0f547140]::passes::start_codegen 25: 0x7f1c7d7e2314 - <rustc_middle[913649502f287e96]::ty::context::GlobalCtxt>::enter::<<rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<alloc[ab6e9888d17cae42]::boxed::Box<dyn core[7ab4a128a7734c10]::any::Any>, rustc_span[14f600a439c86087]::ErrorGuaranteed>> 26: 0x7f1c7d7e1098 - <rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen 27: 0x7f1c7d7e087b - <rustc_interface[bc622c2a0f547140]::interface::Compiler>::enter::<rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}::{closure#2}, core[7ab4a128a7734c10]::result::Result<core[7ab4a128a7734c10]::option::Option<rustc_interface[bc622c2a0f547140]::queries::Linker>, rustc_span[14f600a439c86087]::ErrorGuaranteed>> 28: 0x7f1c7d7de86f - rustc_span[14f600a439c86087]::set_source_map::<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}::{closure#0}> 29: 0x7f1c7d7ddf00 - std[f87cae68a756700d]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>> 30: 0x7f1c7d7dd821 - <<std[f87cae68a756700d]::thread::Builder>::spawn_unchecked_<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#1} as core[7ab4a128a7734c10]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0} 31: 0x7f1c7b376305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hdbaea59c5dcd35ae at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9 32: 0x7f1c7b376305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hedf781cff528734a at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9 33: 0x7f1c7b376305 - std::sys::unix::thread::Thread::new::thread_start::h8db1b8acf05cf216 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys/unix/thread.rs:108:17 34: 0x7f1c7b028bb5 - <unknown> 35: 0x7f1c7b0aad90 - <unknown> 36: 0x0 - <unknown> 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/matthias/vcs/github/rust/src/tools/miri/tests/pass/issues/issue-miri-1075.rs", function: None, start_line: 2, start_col: Some(1), end_line: 2, end_col: Some(10) } error: /home/matthias/.kani/kani-0.29.0/bin/kani-compiler exited with status exit status: 101
The text was updated successfully, but these errors were encountered:
Still crashing with 0.40
Sorry, something went wrong.
No branches or pull requests
I tried this code:
using the following command line invocation:
with Kani version:
kani 0.29.0
I expected to see this happen: explanation
Instead, this happened: explanation
The text was updated successfully, but these errors were encountered: