ICE: Error in struct_expr; mismatch in number of fields and values #2254
Description
I tried this code:
Note that this code will be rejected by some future rust version, so might be ok
trait Trait {}
trait X {
fn foo(&self)
where
Self: Trait;
}
impl X for () {
fn foo(&self) {}
}
impl Trait for dyn X {}
#[kani::proof]
pub fn main() {
<dyn X as X>::foo(&()); //~ERROR: trying to call something that is not a method
}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
warning: the trait `X` cannot be made into an object
--> a.rs:4:8
|
4 | fn foo(&self)
| ^^^
|
= warning: this was previously accepted by the compiler but is being phased out; it will become a hard error in a future release!
= note: for more information, see issue #51443 <https://github.com/rust-lang/rust/issues/51443>
note: for a trait to be "object safe" it needs to allow building a vtable to allow the call to be resolvable dynamically; for more information visit <https://doc.rust-lang.org/reference/items/traits.html#object-safety>
--> a.rs:4:8
|
3 | trait X {
| - this trait cannot be made into an object...
4 | fn foo(&self)
| ^^^ ...because method `foo` references the `Self` type in its `where` clause
= help: consider moving `foo` to another trait
= note: `#[warn(where_clauses_object_safety)]` on by default
thread '<unnamed>' panicked at 'assertion failed: `(left == right)`
left: `4`,
right: `3`: Error in struct_expr; mismatch in number of fields and values.
StructTag("tag-_93938979532004577::vtable")
[Expr { value: Typecast(Expr { value: AddressOf(Expr { value: Symbol { identifier: "_RINvNtCshQhm45nWocF_4core3ptr13drop_in_placeuECsbvss9KOnXkz_1a" }, typ: Code { parameters: [Parameter { typ: Pointer { typ: StructTag("tag-Unit") }, identifier: Some("_RINvNtCshQhm45nWocF_4core3ptr13drop_in_placeuECsbvss9KOnXkz_1a::1::var_1"), base_name: Some("_RINvNtCshQhm45nWocF_4core3ptr13drop_in_placeuECsbvss9KOnXkz_1a::1::var_1") }], return_type: StructTag("tag-Unit") }, location: None }), typ: Pointer { typ: Code { parameters: [Parameter { typ: Pointer { typ: StructTag("tag-Unit") }, identifier: Some("_RINvNtCshQhm45nWocF_4core3ptr13drop_in_placeuECsbvss9KOnXkz_1a::1::var_1"), base_name: Some("_RINvNtCshQhm45nWocF_4core3ptr13drop_in_placeuECsbvss9KOnXkz_1a::1::var_1") }], return_type: StructTag("tag-Unit") } }, location: None }), typ: Pointer { typ: Code { parameters: [Parameter { typ: Pointer { typ: TypeDef { name: "_93938979532004577Inner", typ: StructTag("tag-Unit") } }, identifier: None, base_name: None }], return_type: StructTag("tag-Unit") } }, location: None }, Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None }, Expr { value: IntConstant(1), typ: CInteger(SizeT), location: None }]', cprover_bindings/src/goto_program/expr.rs:782:9
stack backtrace:
0: 0x7f09b56417da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
1: 0x7f09b56417da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x7f09b56417da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
3: 0x7f09b56417da - <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: 0x7f09b56a42ee - core::fmt::write::h27d0bbb767cff1d5
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
5: 0x7f09b5631c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
6: 0x7f09b56415a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
7: 0x7f09b56415a5 - std::sys_common::backtrace::print::he69ac0980f15620d
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
8: 0x7f09b56442ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
9: 0x7f09b564402b - std::panicking::default_hook::h380e71f8d8d49df7
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
10: 0x561f1c3aeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
11: 0x561f1c304f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
12: 0x7f09b5644b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
13: 0x7f09b5644b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
14: 0x7f09b56448a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
15: 0x7f09b5641c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
16: 0x7f09b56445b2 - rust_begin_unwind
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
17: 0x7f09b56a0cd3 - core::panicking::panic_fmt::hbacb72817da3b060
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
18: 0x7f09b56a11b9 - core::panicking::assert_failed_inner::hac89d137c8eb08b5
19: 0x561f1c2739db - core::panicking::assert_failed::hd65f1d32d0255de4
20: 0x561f1c4e2a15 - cprover_bindings::goto_program::expr::Expr::struct_expr_from_values::hdc18295d005ca189
21: 0x561f1c2d27b3 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_unsized_cast::hdfaf122ad8ca4047
22: 0x561f1c2cfefe - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_pointer_cast::h025efe8e5cfb82f1
23: 0x561f1c2c9e83 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h57a2cf71297ecf62
24: 0x561f1c2d8080 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h4c6e1c8bf226a338
25: 0x561f1c27f0d1 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
26: 0x561f1c30abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
27: 0x561f1c3964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
28: 0x7f09b3686fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
29: 0x7f09b3686ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
30: 0x7f09b36847a6 - <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>>
31: 0x7f09b3681a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
32: 0x7f09b3680f67 - <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>>
33: 0x7f09b367bf88 - 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}>
34: 0x7f09b367ba75 - <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>>
35: 0x7f09b367b062 - 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>>
36: 0x7f09b3cec49e - <<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}
37: 0x7f09b51da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
38: 0x7f09b51da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
39: 0x7f09b51da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
40: 0x7f09b0fafbb5 - <unknown>
41: 0x7f09b1031d90 - <unknown>
42: 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: 16, start_col: Some(1), end_line: 16, end_col: Some(14) }
warning: 1 warning emitted
error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101