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:
enum Foo { A(u32), Bar([u16; 4]), C } static FOO: Foo = Foo::C; #[kani::proof] fn main() { let x = &FOO; }
using the following command line invocation:
kani file.rs
with Kani version: kani 0.29.0 I expected to see this happen: explanation
Instead, this happened: explanation
warning: unused variable: `x` --> /home/matthias/vcs/github/rust/tests/ui/consts/const-adt-align-mismatch.rs:11:6 | 11 | let x = &FOO; | ^ help: if this is intentional, prefix it with an underscore: `_x` | = note: `#[warn(unused_variables)]` on by default warning: variants `A` and `Bar` are never constructed --> /home/matthias/vcs/github/rust/tests/ui/consts/const-adt-align-mismatch.rs:2:5 | 1 | enum Foo { | --- variants in this enum 2 | A(u32), | ^ 3 | Bar([u16; 4]), | ^^^ | = note: `#[warn(dead_code)]` on by default thread 'rustc' panicked at 'assertion failed: `(left == right)` left: `96`, right: `80`', cprover_bindings/src/goto_program/expr.rs:884:9 stack backtrace: 0: 0x7f7f98b68cc3 - std::backtrace_rs::backtrace::libunwind::trace::h6dd260ccf76e2a16 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x7f7f98b68cc3 - std::backtrace_rs::backtrace::trace_unsynchronized::h60e795a392c2d181 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x7f7f98b68cc3 - std::sys_common::backtrace::_print_fmt::hb92bc719d8e89e18 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:65:5 3: 0x7f7f98b68cc3 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h433d7296fbd4df36 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:44:22 4: 0x7f7f98bc9c0f - core::fmt::rt::Argument::fmt::hee863a126433a5fe at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/rt.rs:138:9 5: 0x7f7f98bc9c0f - core::fmt::write::hecf019f127565c17 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/mod.rs:1105:21 6: 0x7f7f98b5bd91 - std::io::Write::write_fmt::h4fdee205f020a023 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/io/mod.rs:1712:15 7: 0x7f7f98b68ad5 - std::sys_common::backtrace::_print::h63f1eb292c01c01d at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:47:5 8: 0x7f7f98b68ad5 - std::sys_common::backtrace::print::h29fa6d106f41082b at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:34:9 9: 0x7f7f98b6b697 - std::panicking::default_hook::{{closure}}::h24c419639c3568dd 10: 0x7f7f98b6b485 - std::panicking::default_hook::hd5faae45a4c2ae6b at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:288:9 11: 0x563829f48dfd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62fc73136c5344f5 12: 0x563829f75d83 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::he03976a598c31555 13: 0x7f7f98b6bdd5 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h8fd551c79732d109 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1976:9 14: 0x7f7f98b6bdd5 - std::panicking::rust_panic_with_hook::hff0f13fd32920cda at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:695:13 15: 0x7f7f98b6bb49 - std::panicking::begin_panic_handler::{{closure}}::h4b94c172e12e7b79 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:582:13 16: 0x7f7f98b69106 - std::sys_common::backtrace::__rust_end_short_backtrace::h0d54fda82a2d0073 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:150:18 17: 0x7f7f98b6b8a2 - rust_begin_unwind at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:578:5 18: 0x7f7f98bc5eb3 - core::panicking::panic_fmt::h423e755c13523a61 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:67:14 19: 0x7f7f98bc636f - core::panicking::assert_failed_inner::h8ca5b0e75c0ef7cc 20: 0x563829ea06eb - core::panicking::assert_failed::h37c3a022f8797b4d 21: 0x56382a12b030 - cprover_bindings::goto_program::expr::Expr::transmute_to::hcdc155aa980bca12 22: 0x563829edccad - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_alloc_in_memory::hbfcb21a06d5fa843 23: 0x563829f07f4e - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hc74d90f0f114a03d 24: 0x563829f31804 - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h72b866e5cefa4cb6 25: 0x563829f356d1 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd63a249ce3b650de 26: 0x7f7f9afe4e26 - rustc_interface[bc622c2a0f547140]::passes::start_codegen 27: 0x7f7f9afe2314 - <rustc_middle[913649502f287e96]::ty::context::GlobalCtxt>::enter::<<rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<alloc[ab6e9888d17cae42]::boxed::Box<dyn core[7ab4a128a7734c10]::any::Any>, rustc_span[14f600a439c86087]::ErrorGuaranteed>> 28: 0x7f7f9afe1098 - <rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen 29: 0x7f7f9afe087b - <rustc_interface[bc622c2a0f547140]::interface::Compiler>::enter::<rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}::{closure#2}, core[7ab4a128a7734c10]::result::Result<core[7ab4a128a7734c10]::option::Option<rustc_interface[bc622c2a0f547140]::queries::Linker>, rustc_span[14f600a439c86087]::ErrorGuaranteed>> 30: 0x7f7f9afde86f - rustc_span[14f600a439c86087]::set_source_map::<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}::{closure#0}> 31: 0x7f7f9afddf00 - std[f87cae68a756700d]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>> 32: 0x7f7f9afdd821 - <<std[f87cae68a756700d]::thread::Builder>::spawn_unchecked_<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#1} as core[7ab4a128a7734c10]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0} 33: 0x7f7f98b76305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hdbaea59c5dcd35ae at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9 34: 0x7f7f98b76305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hedf781cff528734a at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9 35: 0x7f7f98b76305 - std::sys::unix::thread::Thread::new::thread_start::h8db1b8acf05cf216 at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys/unix/thread.rs:108:17 36: 0x7f7f987cfbb5 - <unknown> 37: 0x7f7f98851d90 - <unknown> 38: 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:13 ~ const_adt_align_mismatch[b916]::FOO) [Kani] current codegen location: Loc { file: "/home/matthias/vcs/github/rust/tests/ui/consts/const-adt-align-mismatch.rs", function: None, start_line: 7, start_col: Some(1), end_line: 7, end_col: Some(16) } warning: 2 warnings emitted error: /home/matthias/.kani/kani-0.29.0/bin/kani-compiler exited with status exit status: 101
The text was updated successfully, but these errors were encountered:
Still crashes with 0.40
Sorry, something went wrong.
No branches or pull requests
I tried this code:
using the following command line invocation:
with Kani version:
kani 0.29.0
I expected to see this happen: explanation
Instead, this happened: explanation
The text was updated successfully, but these errors were encountered: