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:
#![feature(unboxed_closures, tuple_trait)] extern "rust-call" fn foo<T: std::marker::Tuple>(_: T) {} #[kani::proof] fn main() { foo(()); }
using the following command line invocation:
kani file.rs
with Kani version: 0.22.0
I expected to see this happen: explanation
Instead, this happened: explanation
thread '<unnamed>' panicked at 'assertion failed: prev_args.len() == 1', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:271:13 stack backtrace: 0: 0x7feb975667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x7feb975667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x7feb975667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5 3: 0x7feb975667da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:44:22 4: 0x7feb975c92ee - core::fmt::write::h27d0bbb767cff1d5 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17 5: 0x7feb97556c65 - std::io::Write::write_fmt::hc409ea2bb818fbea at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15 6: 0x7feb975665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5 7: 0x7feb975665a5 - std::sys_common::backtrace::print::he69ac0980f15620d at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9 8: 0x7feb975692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22 9: 0x7feb9756902b - std::panicking::default_hook::h380e71f8d8d49df7 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9 10: 0x55f7b1daeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462 11: 0x55f7b1d04f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a 12: 0x7feb97569b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9 13: 0x7feb97569b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13 14: 0x7feb97569862 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:577:13 15: 0x7feb97566c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18 16: 0x7feb975695b2 - rust_begin_unwind at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5 17: 0x7feb975c5cd3 - core::panicking::panic_fmt::hbacb72817da3b060 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14 18: 0x7feb975c5dad - core::panicking::panic::hbb63dcd9a5d7212e at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:111:5 19: 0x55f7b1ce11a9 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::sig_with_untupled_args::hfdda502c3c2a52ea 20: 0x55f7b1ce14b6 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::fn_sig_of_instance::h0957a78432e4811e 21: 0x55f7b1d1b38f - kani_compiler::codegen_cprover_gotoc::context::current_fn::CurrentFnCtx::new::h9e49a62362e43a2c 22: 0x55f7b1c7ffc1 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::declare_function::hcb4ad696d24f1916 23: 0x55f7b1d09b60 - std::thread::local::LocalKey<T>::with::h8c541365775d3b68 24: 0x55f7b1d95f05 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6 25: 0x7feb99a86fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}> 26: 0x7feb99a86ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen 27: 0x7feb99a847a6 - <rustc_interface[aec886e93b1add3f]::passes::QueryContext>::enter::<<rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>> 28: 0x7feb99a81a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen 29: 0x7feb99a80f67 - <rustc_interface[aec886e93b1add3f]::interface::Compiler>::enter::<rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}::{closure#2}, core[6d94cc961ac87456]::result::Result<core[6d94cc961ac87456]::option::Option<rustc_interface[aec886e93b1add3f]::queries::Linker>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>> 30: 0x7feb99a7bf88 - rustc_span[ae2df7aa7c6c667b]::with_source_map::<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}::{closure#0}> 31: 0x7feb99a7ba75 - <scoped_tls[db87656d258d017b]::ScopedKey<rustc_span[ae2df7aa7c6c667b]::SessionGlobals>>::set::<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>> 32: 0x7feb99a7b062 - std[acd1f573e90225f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>> 33: 0x7feb9a0ec49e - <<std[acd1f573e90225f]::thread::Builder>::spawn_unchecked_<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#1} as core[6d94cc961ac87456]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0} 34: 0x7feb9b5da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9 35: 0x7feb9b5da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9 36: 0x7feb9b5da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17 37: 0x7feb97216bb5 - <unknown> 38: 0x7feb97298d90 - <unknown> 39: 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: declare_function: foo::<()> [Kani] current codegen location: Loc { file: "/home/matthias/vcs/github/icemaker/kani/b.rs", function: None, start_line: 3, start_col: Some(1), end_line: 3, end_col: Some(55) } error: /home/matthias/.kani/kani-0.22.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: 0.22.0
I expected to see this happen: explanation
Instead, this happened: explanation
The text was updated successfully, but these errors were encountered: