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:
type BuiltIn = for<'a> fn(&str); struct Function { inner: BuiltIn, } impl Function { fn new(subr: BuiltIn) -> Self { Self { inner: subr } } } fn dummy(_: &str) {} #[kani::proof] fn main() { let func1 = Function::new(dummy); let func2 = Function::new(dummy); let inner: fn(&'static _) -> _ = func1.inner; assert!(inner == func2.inner); }
using the following command line invocation:
kani file.rs
with Kani version: 0.46.0
I expected to see this happen: explanation
Instead, this happened: explanation
Kani Rust Verifier 0.46.0 (standalone) thread 'rustc' panicked at compiler/stable_mir/src/mir/body.rs:384:17: assertion `left == right` failed left: Ty { id: 5, kind: RigidTy(FnPtr(Binder { value: FnSig { inputs_and_output: [Ty { id: 4, kind: RigidTy(Ref(Region { kind: ReErased }, Ty { id: 10, kind: RigidTy(Str) }, Not)) }, Ty { id: 6, kind: RigidTy(Tuple([])) }], c_variadic: false, unsafety: Normal, abi: Rust }, bound_vars: [] })) } right: Ty { id: 2, kind: RigidTy(FnPtr(Binder { value: FnSig { inputs_and_output: [Ty { id: 9, kind: RigidTy(Ref(Region { kind: ReBound(0, BoundRegion { var: 0, kind: BrAnon }) }, Ty { id: 10, kind: RigidTy(Str) }, Not)) }, Ty { id: 6, kind: RigidTy(Tuple([])) }], c_variadic: false, unsafety: Normal, abi: Rust }, bound_vars: [Region(BrAnon)] })) } stack backtrace: 0: 0x7f3644d8be86 - std::backtrace_rs::backtrace::libunwind::trace::haa62de98ce20d13c at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5 1: 0x7f3644d8be86 - std::backtrace_rs::backtrace::trace_unsynchronized::h4bc7f582e9f49dbd at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x7f3644d8be86 - std::sys_common::backtrace::_print_fmt::h07d78988ae6e922d at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:68:5 3: 0x7f3644d8be86 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::he72c24e459b4aee4 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:44:22 4: 0x7f3644dde740 - core::fmt::rt::Argument::fmt::h9ff3b213e1468f5f at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/fmt/rt.rs:142:9 5: 0x7f3644dde740 - core::fmt::write::h0ab1f59280077a18 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/fmt/mod.rs:1120:17 6: 0x7f3644d7f7bf - std::io::Write::write_fmt::h2f48f6201433d434 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/io/mod.rs:1810:15 7: 0x7f3644d8bc64 - std::sys_common::backtrace::_print::h710dac96d5446d07 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:47:5 8: 0x7f3644d8bc64 - std::sys_common::backtrace::print::h22982b9f2c94c190 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:34:9 9: 0x7f3644d8e9f7 - std::panicking::default_hook::{{closure}}::h19052586580466eb 10: 0x7f3644d8e759 - std::panicking::default_hook::h9f3f4c25f2a49543 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:292:9 11: 0x557ba698b29d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62bee1eb7956b9f6 12: 0x557ba698aaa3 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h252d31e703366824 13: 0x7f3644d8f146 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h0ebb0eb5cf5e84f1 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2030:9 14: 0x7f3644d8f146 - std::panicking::rust_panic_with_hook::hb83cfb3ac729d1b2 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:785:13 15: 0x7f3644d8ee92 - std::panicking::begin_panic_handler::{{closure}}::hf6588d71adde3329 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:659:13 16: 0x7f3644d8c386 - std::sys_common::backtrace::__rust_end_short_backtrace::hfa69dd6720275711 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys_common/backtrace.rs:171:18 17: 0x7f3644d8ebe4 - rust_begin_unwind at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/panicking.rs:647:5 18: 0x7f3644ddae45 - core::panicking::panic_fmt::h3d775185360585e3 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:72:14 19: 0x7f3644ddb3db - core::panicking::assert_failed_inner::h0e5c67b40620ee84 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/core/src/panicking.rs:342:17 20: 0x7f3648718ca3 - core[2f78b8535a2e64fa]::panicking::assert_failed::<stable_mir[64b791d3cb4792a]::ty::Ty, stable_mir[64b791d3cb4792a]::ty::Ty> 21: 0x7f364871c6a6 - <stable_mir[64b791d3cb4792a]::mir::body::BinOp>::ty 22: 0x7f364871c86c - <stable_mir[64b791d3cb4792a]::mir::body::Rvalue>::ty 23: 0x557ba691e1f9 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h9ef1fd17419243a3 24: 0x557ba69373eb - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h70ea6b1d619c790d 25: 0x557ba69f9e9a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h179e069baadeebc1 26: 0x557ba69b1430 - scoped_tls::ScopedKey<T>::set::h462dbe7b3063cb5c 27: 0x557ba69e91a4 - rustc_smir::rustc_internal::init::hdab7351afa62793a 28: 0x557ba69b4054 - stable_mir::compiler_interface::run::hdc01671daf50c78a 29: 0x557ba69fd62e - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd5728f8a33105c7d 30: 0x7f364986aff0 - rustc_interface[79a3a7c6d29fbb15]::passes::start_codegen 31: 0x7f364986a75c - <rustc_interface[79a3a7c6d29fbb15]::queries::Queries>::codegen_and_build_linker 32: 0x7f3649b7a44a - rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler::<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0} 33: 0x7f3649de5986 - std[da4468a6436061de]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_with_globals<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_pool_with_globals<rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>> 34: 0x7f3649de57b3 - <<std[da4468a6436061de]::thread::Builder>::spawn_unchecked_<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_with_globals<rustc_interface[79a3a7c6d29fbb15]::util::run_in_thread_pool_with_globals<rustc_interface[79a3a7c6d29fbb15]::interface::run_compiler<core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>, rustc_driver_impl[27708ea34d8a9a18]::run_compiler::{closure#0}>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[2f78b8535a2e64fa]::result::Result<(), rustc_span[8cc10a3d00093188]::ErrorGuaranteed>>::{closure#1} as core[2f78b8535a2e64fa]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0} 35: 0x7f3644d98735 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hda2c57e98ef914e1 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2016:9 36: 0x7f3644d98735 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h4c1ca1ffb3984aed at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/alloc/src/boxed.rs:2016:9 37: 0x7f3644d98735 - std::sys::pal::unix::thread::Thread::new::thread_start::h6dfa281031503fa8 at /rustc/7ffc697ce10f19447c0ce338428ae4b9bc0c041c/library/std/src/sys/pal/unix/thread.rs:108:17 38: 0x7f3644a979eb - <unknown> 39: 0x7f3644b1b7cc - <unknown> 40: 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: "issue-91636.rs", function: None, start_line: 16, start_col: Some(1), end_line: 16, end_col: Some(10) } error: /home/matthias/.kani/kani-0.46.0/bin/kani-compiler exited with status exit status: 101
The text was updated successfully, but these errors were encountered:
No branches or pull requests
I tried this code:
using the following command line invocation:
with Kani version: 0.46.0
I expected to see this happen: explanation
Instead, this happened: explanation
The text was updated successfully, but these errors were encountered: