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
Expected constant allocation for
, but got a mutable instead
I tried this code:
static mut FOO: Foo = Foo { field: &mut [42] as *mut [i32] as *mut i32, }; struct Foo { field: *mut i32, } unsafe impl Sync for Foo {} #[kani::proof] fn main() { assert_eq!(unsafe { *FOO.field = 69; *FOO.field }, 69); }
using the following command line invocation:
RUSTFLAGS="-Zmir-opt-level=2" RUST_BACKTRACE=full RUSTC_WRAPPER="" cargo kani
with Kani version: 0.35.0
I expected to see this happen: explanation
Instead, this happened: explanation
Kani Rust Verifier 0.35.0 (cargo plugin) Compiling kani v0.1.0 (/tmp/kani) thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:548:9: assertion `left == right` failed: Expected constant allocation for `Some("kani.d1f1d340b3a1dad::kani::alloc4")`, but got a mutable instead left: Mut right: Not error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:548:9: assertion `left == right` failed: Expected constant allocation for `Some("kani.d1f1d340b3a1dad::kani::alloc4")`, but got a mutable instead left: Mut right: Not. stack backtrace: 0: 0x7f4811b6329c - std::backtrace_rs::backtrace::libunwind::trace::h28e11dce06475f43 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x7f4811b6329c - std::backtrace_rs::backtrace::trace_unsynchronized::h21f22a3bfa3fb013 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x7f4811b6329c - std::sys_common::backtrace::_print_fmt::hafc6985e93f76ae0 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:67:5 3: 0x7f4811b6329c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h36c63275fbd3f0f8 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:44:22 4: 0x7f4811bc93ec - core::fmt::rt::Argument::fmt::h9b33518f8511caca at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/fmt/rt.rs:138:9 5: 0x7f4811bc93ec - core::fmt::write::h67226f5192a09eca at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/fmt/mod.rs:1094:21 6: 0x7f4811b55d2e - std::io::Write::write_fmt::h744b3076c6ca0e52 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/io/mod.rs:1714:15 7: 0x7f4811b63084 - std::sys_common::backtrace::_print::h4bcc2e79e4348aa6 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:47:5 8: 0x7f4811b63084 - std::sys_common::backtrace::print::h74142c12abe5e25d at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:34:9 9: 0x7f4811b6617a - std::panicking::panic_hook_with_disk_dump::{{closure}}::h7d3e65abd6cf3378 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:278:22 10: 0x7f4811b65e67 - std::panicking::panic_hook_with_disk_dump::h5bbd6ac133545f46 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:312:9 11: 0x55711b33f2dd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h5067a4a6926df452 12: 0x55711b33f5cd - kani_compiler::session::JSON_PANIC_HOOK::{{closure}}::{{closure}}::h449e03c79d4f70ea 13: 0x55711b33e463 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hbc7dbed47af55a6e 14: 0x7f4811b66a20 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hbc8f8f631658dcc9 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2021:9 15: 0x7f4811b66a20 - std::panicking::rust_panic_with_hook::h7b16b439ec100c23 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:733:13 16: 0x7f4811b667a7 - std::panicking::begin_panic_handler::{{closure}}::hd03f21e4b251a35c at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:621:13 17: 0x7f4811b637c6 - std::sys_common::backtrace::__rust_end_short_backtrace::he8aad725f5dd71ab at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys_common/backtrace.rs:170:18 18: 0x7f4811b664f2 - rust_begin_unwind at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/panicking.rs:617:5 19: 0x7f4811bc57f3 - core::panicking::panic_fmt::h37323eb5862b87ad at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/core/src/panicking.rs:67:14 20: 0x7f4811bc5d15 - core::panicking::assert_failed_inner::h203d73c9cdc85fdd 21: 0x55711b29ecff - core::panicking::assert_failed::h0dcfd4d42a3f4717 22: 0x55711b2e15f9 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_const_allocation::hfaf842eacfa5715e 23: 0x55711b2e0415 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_alloc_pointer::hc11591ed759f1d32 24: 0x55711b2e2a40 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_allocation_data::hd4d00d7c36cc76bd 25: 0x55711b2e198b - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_alloc_in_memory::h0613f33a5f8d3759 26: 0x55711b30ba04 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hb78fbbf93858f04a 27: 0x55711b3ceb75 - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h71130359840cd186 28: 0x55711b3d35a5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h25888e407b1b3e70 29: 0x7f481400d3c2 - <rustc_session[a6bdf9a4b51671a9]::session::Session>::time::<alloc[10a91b7ea9db36b6]::boxed::Box<dyn core[3ec4812ddef0ef93]::any::Any>, rustc_interface[39ac7ec62dd85acc]::passes::start_codegen::{closure#0}> 30: 0x7f481400cf1b - rustc_interface[39ac7ec62dd85acc]::passes::start_codegen 31: 0x7f4814007bba - <rustc_middle[9074e8ddcc94940f]::ty::context::GlobalCtxt>::enter::<<rustc_interface[39ac7ec62dd85acc]::queries::Queries>::ongoing_codegen::{closure#0}, core[3ec4812ddef0ef93]::result::Result<alloc[10a91b7ea9db36b6]::boxed::Box<dyn core[3ec4812ddef0ef93]::any::Any>, rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>> 32: 0x7f4814007066 - <rustc_interface[39ac7ec62dd85acc]::interface::Compiler>::enter::<rustc_driver_impl[e8f28f10c524a0ae]::run_compiler::{closure#1}::{closure#2}, core[3ec4812ddef0ef93]::result::Result<core[3ec4812ddef0ef93]::option::Option<rustc_interface[39ac7ec62dd85acc]::queries::Linker>, rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>> 33: 0x7f4814004338 - std[98f21c237d3a11b9]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[39ac7ec62dd85acc]::util::run_in_thread_pool_with_globals<rustc_interface[39ac7ec62dd85acc]::interface::run_compiler<core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>, rustc_driver_impl[e8f28f10c524a0ae]::run_compiler::{closure#1}>::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>> 34: 0x7f4814003ac5 - <<std[98f21c237d3a11b9]::thread::Builder>::spawn_unchecked_<rustc_interface[39ac7ec62dd85acc]::util::run_in_thread_pool_with_globals<rustc_interface[39ac7ec62dd85acc]::interface::run_compiler<core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>, rustc_driver_impl[e8f28f10c524a0ae]::run_compiler::{closure#1}>::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[3ec4812ddef0ef93]::result::Result<(), rustc_span[7b07eadf6d8a61c8]::ErrorGuaranteed>>::{closure#1} as core[3ec4812ddef0ef93]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0} 35: 0x7f4811b71225 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h5d092cb8decc581e at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2007:9 36: 0x7f4811b71225 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h88f1cce7655d0913 at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/alloc/src/boxed.rs:2007:9 37: 0x7f4811b71225 - std::sys::unix::thread::Thread::new::thread_start::h775d92d70f807a4c at /rustc/d06ca0ffaf4ac72732665f99dd9ad962194cd0b3/library/std/src/sys/unix/thread.rs:108:17 38: 0x7f481168c9eb - <unknown> 39: 0x7f4811710dfc - <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_static: DefId(0:3 ~ kani[0d1f]::FOO) [Kani] current codegen location: Loc { file: "/tmp/kani/src/main.rs", function: None, start_line: 1, start_col: Some(1), end_line: 1, end_col: Some(20) } error: could not compile `kani` (bin "kani") error: Failed to compile `kani` due to an internal compiler error.: error: internal compiler error: Kani unexpectedly panicked at panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:548:9: assertion `left == right` failed: Expected constant allocation for `Some("kani.d1f1d340b3a1dad::kani::alloc4")`, but got a mutable instead left: Mut right: Not.
The text was updated successfully, but these errors were encountered:
Thanks @matthiaskrgr ! Adding the "Crash" label to this issue.
Sorry, something went wrong.
triage: still crashing with 0.40
No branches or pull requests
I tried this code:
using the following command line invocation:
with Kani version: 0.35.0
I expected to see this happen: explanation
Instead, this happened: explanation
The text was updated successfully, but these errors were encountered: