generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 141
Open
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.
Description
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
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.