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:
trait Stream { type Car; type Cdr: Stream; fn car(&self) -> Self::Car; fn cdr(self) -> Self::Cdr; } impl Stream for () { type Car = (); type Cdr = (); fn car(&self) -> () { () } fn cdr(self) -> () { self } } impl<T,U> Stream for (T, U) where T : Clone, U : Stream { type Car = T; type Cdr = U; fn car(&self) -> T { self.0.clone() } fn cdr(self) -> U { self.1 } } #[kani::proof] fn main() { let p = (22, (44, (66, ()))); assert_eq!(p.car(), 22); }
using the following command line invocation:
kani a.rs
with Kani version: 0.22.0
I expected to see this happen: explanation
Instead, this happened: explanation
thread '<unnamed>' panicked at 'internal error: entered unreachable code', kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:403:21 stack backtrace: 0: 0x7f9f6e4227da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x7f9f6e4227da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x7f9f6e4227da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5 3: 0x7f9f6e4227da - <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: 0x7f9f6e4852ee - core::fmt::write::h27d0bbb767cff1d5 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17 5: 0x7f9f6e412c65 - std::io::Write::write_fmt::hc409ea2bb818fbea at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15 6: 0x7f9f6e4225a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5 7: 0x7f9f6e4225a5 - std::sys_common::backtrace::print::he69ac0980f15620d at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9 8: 0x7f9f6e4252ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22 9: 0x7f9f6e42502b - std::panicking::default_hook::h380e71f8d8d49df7 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9 10: 0x5581493aeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462 11: 0x558149304f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a 12: 0x7f9f6e425b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9 13: 0x7f9f6e425b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13 14: 0x7f9f6e425862 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:577:13 15: 0x7f9f6e422c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18 16: 0x7f9f6e4255b2 - rust_begin_unwind at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5 17: 0x7f9f6e481cd3 - core::panicking::panic_fmt::hbacb72817da3b060 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14 18: 0x7f9f6e481dad - core::panicking::panic::hbb63dcd9a5d7212e at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:111:5 19: 0x5581492bdebc - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_scalar::ha3c3a576ac17f9b2 20: 0x5581492bad73 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_const_value::hb556191d9d37412d 21: 0x5581492ba26d - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::hd73dcdb6f0cd0ad9 22: 0x5581492c8b0b - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h57a2cf71297ecf62 23: 0x5581492d8080 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h4c6e1c8bf226a338 24: 0x55814927f0d1 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35 25: 0x55814930abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6 26: 0x5581493964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6 27: 0x7f9f6c486fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}> 28: 0x7f9f6c486ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen 29: 0x7f9f6c4847a6 - <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>> 30: 0x7f9f6c481a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen 31: 0x7f9f6c480f67 - <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>> 32: 0x7f9f6c47bf88 - 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}> 33: 0x7f9f6c47ba75 - <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>> 34: 0x7f9f6c47b062 - 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>> 35: 0x7f9f6caec49e - <<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} 36: 0x7f9f6dfda2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9 37: 0x7f9f6dfda2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9 38: 0x7f9f6dfda2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64 at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17 39: 0x7f9f69d91bb5 - <unknown> 40: 0x7f9f69e13d90 - <unknown> 41: 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/icemaker/kani/a.rs", function: None, start_line: 26, start_col: Some(1), end_line: 26, end_col: Some(10) } 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:
Fixed with kani 0.40 🎉
Sorry, something went wrong.
We fixed this back in #2366, which is part of all releases since 0.26.0.
JustusAdam
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: