You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Note that this code will be rejected by some future rust version, so might be ok
traitTrait{}traitX{fnfoo(&self)whereSelf:Trait;}implXfor(){fnfoo(&self){}}implTraitfordynX{}#[kani::proof]pubfnmain(){
<dynXasX>::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
The text was updated successfully, but these errors were encountered:
I tried this code:
Note that this code will be rejected by some future rust version, so might be ok
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: