Skip to content

assertion failure: ref to enum static #2498

Closed as not planned
Closed as not planned

Description

@matthiaskrgr

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

Activity

  1. matthiaskrgr commented on Nov 12, 2023

    @matthiaskrgr
    ContributorAuthor

    Still crashes with 0.40

  2. added theissue type on Apr 1, 2026
  3. feliperodri commented on Sep 25, 2026

    @feliperodri
    Member

    Triaged against main (de756c9, nightly-2026-09-23, Kani 0.68.0). kani code.rs → Complete - 1 successfully verified harnesses, 0 failures, 1 total.

    Closing as no longer reproducible — please reopen if you can still hit it on main.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    [C] BugThis is a bug. Something isn't working.

    Type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions