panic: uninit checks: FieldsShape::Primitive with a different ABI than ValueAbi::Scalar #4855

RUST_BACKTRACE=full  RUSTFLAGS="--edition=2021 --cap-lints=warn"  kani autoharness -Zautoharness code.rs --run-sanity-checks  -Zunstable-options   -Zuninit-checks  -Zuninit-checks

Kani Rust Verifier 0.68.0 (standalone)
CBMC 6.11.0
warning: unused variable: `f`
 --> code.rs:8:9
  |
8 |     let f = Foo { a: 2 };
  |         ^ help: if this is intentional, prefix it with an underscore: `_f`
  |
  = note: `#[warn(unused_variables)]` (part of `#[warn(unused)]`) on by default

warning: enum `Never` is never used
 --> code.rs:2:6
  |
2 | enum Never {}
  |      ^^^^^
  |
  = note: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default

warning: union `Foo` is never used
 --> code.rs:3:7
  |
3 | union Foo {
  |       ^^^

warning: function `main` is never used
 --> code.rs:7:4
  |
7 | fn main() {
  |    ^^^^

warning: use of an unstable feature
 --> <crate attribute>:1:12
  |
1 | #![feature(register_tool)]
  |            ^^^^^^^^^^^^^
  |
  = note: requested on the command line with `--force-warn unstable-features`


thread 'rustc' (3682933) panicked at kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs:191:18:
internal error: entered unreachable code: FieldsShape::Primitive with a different ABI than ValueAbi::Scalar
stack backtrace:
   0:     0x7f4f50ec53f6 - <<std[b8564071bfb80320]::sys::backtrace::BacktraceLock>::print::DisplayBacktrace as core[b218925afaf52552]::fmt::Display>::fmt
   1:     0x7f4f5160aca3 - core[b218925afaf52552]::fmt::write
   2:     0x7f4f50edaa1c - <std[b8564071bfb80320]::sys::stdio::unix::Stderr as core[b218925afaf52552]::io::write::Write>::write_fmt
   3:     0x7f4f50e9868a - std[b8564071bfb80320]::panicking::default_hook::{closure#0}
   4:     0x7f4f50eb96a3 - std[b8564071bfb80320]::panicking::default_hook
   5:     0x563c55b87f40 - kani_compiler[980edcef3ed27b2]::session::PANIC_HOOK::{closure#0}::{closure#0}
   6:     0x563c55b883a0 - kani_compiler[980edcef3ed27b2]::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{closure#0}::{closure#0}
   7:     0x7f4f50eb9b42 - std[b8564071bfb80320]::panicking::panic_with_hook
   8:     0x7f4f50e98774 - std[b8564071bfb80320]::panicking::panic_handler::{closure#0}
   9:     0x7f4f50e903a9 - std[b8564071bfb80320]::sys::backtrace::__rust_end_short_backtrace::<std[b8564071bfb80320]::panicking::panic_handler::{closure#0}, !>
  10:     0x7f4f50e9a14d - __rustc[f325e6f53f8e9f03]::rust_begin_unwind
  11:     0x7f4f4dacb57c - core[b218925afaf52552]::panicking::panic_fmt
  12:     0x563c55bc0ecd - kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::data_bytes_for_ty
  13:     0x563c559d40a9 - <alloc[1fd94160f0f4009f]::vec::into_iter::IntoIter<rustc_public[982db8fb9120de79]::ty::def::FieldDef> as core[b218925afaf52552]::iter::traits::iterator::Iterator>::try_fold::<alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>, core[b218925afaf52552]::iter::adapters::map::map_try_fold<rustc_public[982db8fb9120de79]::ty::def::FieldDef, core[b218925afaf52552]::result::Result<alloc[1fd94160f0f4009f]::vec::Vec<bool>, kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::LayoutComputationError>, alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>, core[b218925afaf52552]::ops::control_flow::ControlFlow<core[b218925afaf52552]::result::Result<alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>, !>, alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>>, <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::PointeeInfo>::from_ty::{closure#0}, <core[b218925afaf52552]::iter::adapters::GenericShunt<core[b218925afaf52552]::iter::adapters::map::Map<alloc[1fd94160f0f4009f]::vec::into_iter::IntoIter<rustc_public[982db8fb9120de79]::ty::def::FieldDef>, <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::PointeeInfo>::from_ty::{closure#0}>, core[b218925afaf52552]::result::Result<core[b218925afaf52552]::convert::Infallible, kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::LayoutComputationError>> as core[b218925afaf52552]::iter::traits::iterator::Iterator>::try_fold<alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>, alloc[1fd94160f0f4009f]::vec::in_place_collect::write_in_place_with_drop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>::{closure#0}, core[b218925afaf52552]::result::Result<alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>, !>>::{closure#0}>::{closure#0}, core[b218925afaf52552]::ops::control_flow::ControlFlow<core[b218925afaf52552]::result::Result<alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>, !>, alloc[1fd94160f0f4009f]::vec::in_place_drop::InPlaceDrop<alloc[1fd94160f0f4009f]::vec::Vec<bool>>>>
  14:     0x563c55b5ce60 - alloc[1fd94160f0f4009f]::vec::in_place_collect::from_iter_in_place::<core[b218925afaf52552]::iter::adapters::GenericShunt<core[b218925afaf52552]::iter::adapters::map::Map<alloc[1fd94160f0f4009f]::vec::into_iter::IntoIter<rustc_public[982db8fb9120de79]::ty::def::FieldDef>, <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::PointeeInfo>::from_ty::{closure#0}>, core[b218925afaf52552]::result::Result<core[b218925afaf52552]::convert::Infallible, kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::LayoutComputationError>>, alloc[1fd94160f0f4009f]::vec::Vec<bool>>
  15:     0x563c55bb7ac3 - <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ty_layout::PointeeInfo>::from_ty
  16:     0x563c55bd86d3 - <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ptr_uninit::uninit_visitor::CheckUninitVisitor as rustc_public[982db8fb9120de79]::mir::visit::MirVisitor>::super_basic_block
  17:     0x563c55bcbe5b - <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ptr_uninit::uninit_visitor::CheckUninitVisitor as kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::TargetFinder>::find_all
  18:     0x563c55ade123 - <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::UninitInstrumenter>::run::<kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ptr_uninit::uninit_visitor::CheckUninitVisitor>
  19:     0x563c55bcadb8 - <kani_compiler[980edcef3ed27b2]::kani_middle::transform::check_uninit::ptr_uninit::UninitPass as kani_compiler[980edcef3ed27b2]::kani_middle::transform::TransformPass>::transform
  20:     0x563c5599b500 - <kani_compiler[980edcef3ed27b2]::kani_middle::transform::BodyTransformation>::body_ref
  21:     0x563c55ad2026 - <kani_compiler[980edcef3ed27b2]::kani_middle::reachability::MonoItemsCollector>::reachable_items
  22:     0x563c55ad68f8 - kani_compiler[980edcef3ed27b2]::kani_middle::reachability::collect_reachable_items
  23:     0x563c55a1ab28 - <kani_compiler[980edcef3ed27b2]::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items
  24:     0x563c55a183fd - <kani_compiler[980edcef3ed27b2]::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa[6aa05fb22a8957d5]::traits::backend::CodegenBackend>::codegen_crate::{closure#0}
  25:     0x563c55a87c15 - rustc_public[982db8fb9120de79]::compiler_interface::run::<rustc_public[982db8fb9120de79]::rustc_internal::run<<kani_compiler[980edcef3ed27b2]::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa[6aa05fb22a8957d5]::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc[1fd94160f0f4009f]::boxed::Box<dyn core[b218925afaf52552]::any::Any>>::{closure#0}, alloc[1fd94160f0f4009f]::boxed::Box<dyn core[b218925afaf52552]::any::Any>>
  26:     0x563c55ba07c5 - rustc_public[982db8fb9120de79]::rustc_internal::run::<<kani_compiler[980edcef3ed27b2]::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa[6aa05fb22a8957d5]::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc[1fd94160f0f4009f]::boxed::Box<dyn core[b218925afaf52552]::any::Any>>
  27:     0x563c55a24bb9 - <kani_compiler[980edcef3ed27b2]::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa[6aa05fb22a8957d5]::traits::backend::CodegenBackend>::codegen_crate
  28:     0x7f4f5294db8c - <rustc_interface[4089758db528eb1a]::queries::Linker>::codegen_and_build_linker
  29:     0x7f4f5294448a - rustc_interface[4089758db528eb1a]::interface::run_compiler::<(), rustc_driver_impl[f578478d149be60]::run_compiler::{closure#0}>::{closure#2}
  30:     0x7f4f529c1e64 - std[b8564071bfb80320]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[4089758db528eb1a]::util::run_in_thread_with_globals<rustc_interface[4089758db528eb1a]::util::run_in_thread_pool_with_globals<rustc_interface[4089758db528eb1a]::interface::run_compiler<(), rustc_driver_impl[f578478d149be60]::run_compiler::{closure#0}>::{closure#2}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>
  31:     0x7f4f529c1c2d - <std[b8564071bfb80320]::thread::lifecycle::spawn_unchecked<rustc_interface[4089758db528eb1a]::util::run_in_thread_with_globals<rustc_interface[4089758db528eb1a]::util::run_in_thread_pool_with_globals<rustc_interface[4089758db528eb1a]::interface::run_compiler<(), rustc_driver_impl[f578478d149be60]::run_compiler::{closure#0}>::{closure#2}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>::{closure#1} as core[b218925afaf52552]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  32:     0x7f4f529bf907 - <std[b8564071bfb80320]::sys::thread::unix::Thread>::new::thread_start
  33:     0x7f4f4bc980a2 - <unknown>
  34:     0x7f4f4bd2080c - <unknown>
  35:                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] no current codegen item.
[Kani] no current codegen location.
warning: 5 warnings emitted

error: /home/matthias/.kani/kani-0.68.0/bin/kani-compiler exited with status exit status: 101