Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

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

Jump to bottom

ICE: internal error: entered unreachable code: Should have generated a fat pointer #2266

Open
matthiaskrgr opened this issue Mar 3, 2023 · 1 comment
Open

ICE: internal error: entered unreachable code: Should have generated a fat pointer #2266

matthiaskrgr opened this issue Mar 3, 2023 · 1 comment
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed

Comments

@matthiaskrgr
Copy link
Contributor

I tried this code:

// check-pass
// edition: 2021

// This test case is meant to demonstrate how close we can get to async
// functions in dyn traits with the current level of dyn* support.

#![feature(dyn_star)]
#![allow(incomplete_features)]

use std::future::Future;

trait DynAsyncCounter {
    fn increment<'a>(&'a mut self) -> dyn* Future<Output = usize> + 'a;
}

struct MyCounter {
    count: usize,
}

impl DynAsyncCounter for MyCounter {
    fn increment<'a>(&'a mut self) -> dyn* Future<Output = usize> + 'a {
        Box::pin(async {
            self.count += 1;
            self.count
        })
    }
}

async fn do_counter(counter: &mut dyn DynAsyncCounter) -> usize {
    counter.increment().await
}

#[kani::proof]
fn main() {
    let mut counter = MyCounter { count: 0 };
    let _ = do_counter(&mut counter);
}

using the following command line invocation:

RUSTFLAGS="--edition=2021" kani dyn-async-trait.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

thread '<unnamed>' panicked at 'Type dyn* std::future::Future<Output = usize> must be a trait type (a dynamic type)', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:601:9
stack backtrace:
   0:     0x7f4657b667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f4657b667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f4657b667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7f4657b667da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f4657bc92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7f4657b56c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7f4657b665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7f4657b665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7f4657b692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7f4657b6902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x55a9689aeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x55a968904f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7f4657b69b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7f4657b69b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7f4657b698a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
  15:     0x7f4657b66c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7f4657b695b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7f4657bc5cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x55a9688e35aa - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::normalized_trait_name::h895d46c4fb1ec415
  19:     0x55a9688e2c2e - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_trait_data::hd51c10437a5ae95e
  20:     0x55a9688e3dc8 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty::h3a1c4e105629c1cf
  21:     0x55a9688e29c6 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::trait_method_vtable_field_type::ha0d906bfaec8b77c
  22:     0x55a96897b0d3 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h2a20199b30e6eed4
  23:     0x55a9688e936e - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty_ref::h8f0e76378246970b
  24:     0x55a9688e4823 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty::h3a1c4e105629c1cf
  25:     0x55a968931934 - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::h3d27524049e75026
  26:     0x55a968982876 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::he9d1f8227d49a086
  27:     0x55a96888041f - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::declare_function::hcb4ad696d24f1916
  28:     0x55a968909b60 - std::thread::local::LocalKey<T>::with::h8c541365775d3b68
  29:     0x55a968995f05 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  30:     0x7f465a086fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  31:     0x7f465a086ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  32:     0x7f465a0847a6 - <rustc_interface[aec886e93b1add3f]::passes::QueryContext>::enter::<<rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  33:     0x7f465a081a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  34:     0x7f465a080f67 - <rustc_interface[aec886e93b1add3f]::interface::Compiler>::enter::<rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}::{closure#2}, core[6d94cc961ac87456]::result::Result<core[6d94cc961ac87456]::option::Option<rustc_interface[aec886e93b1add3f]::queries::Linker>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  35:     0x7f465a07bf88 - rustc_span[ae2df7aa7c6c667b]::with_source_map::<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  36:     0x7f465a07ba75 - <scoped_tls[db87656d258d017b]::ScopedKey<rustc_span[ae2df7aa7c6c667b]::SessionGlobals>>::set::<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  37:     0x7f465a07b062 - std[acd1f573e90225f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  38:     0x7f465a6ec49e - <<std[acd1f573e90225f]::thread::Builder>::spawn_unchecked_<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#1} as core[6d94cc961ac87456]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  39:     0x7f465bbda2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  40:     0x7f465bbda2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  41:     0x7f465bbda2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  42:     0x7f4657905bb5 - <unknown>
  43:     0x7f4657987d90 - <unknown>
  44:                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: declare_function: do_counter
[Kani] current codegen location: Loc { file: "/tmp/kani/dyn-async-trait.rs", function: None, start_line: 29, start_col: Some(1), end_line: 29, end_col: Some(64) }
error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101
@matthiaskrgr matthiaskrgr added the [C] Bug This is a bug. Something isn't working. label Mar 3, 2023
@zhassan-aws zhassan-aws added the [F] Crash Kani crashed label Mar 4, 2023
@matthiaskrgr matthiaskrgr changed the title ICE: Type dyn* std::future::Future<Output = usize> must be a trait type (a dynamic type) ICE: internal error: entered unreachable code: Should have generated a fat pointer Nov 12, 2023
@matthiaskrgr
Copy link
Contributor Author

with kani 0.40:

Kani Rust Verifier 0.40.0 (standalone)
thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:1220:17:
internal error: entered unreachable code: Should have generated a fat pointer
stack backtrace:
   0:     0x7ff2f8e37cfc - std::backtrace_rs::backtrace::libunwind::trace::h974857262e179b17
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7ff2f8e37cfc - std::backtrace_rs::backtrace::trace_unsynchronized::h6adce2053c056ac9
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7ff2f8e37cfc - std::sys_common::backtrace::_print_fmt::hcf2018a5ad956761
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7ff2f8e37cfc - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h3d39e48ce4d7e36f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7ff2f8e99f50 - core::fmt::rt::Argument::fmt::hef0ae15422a7f61d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/rt.rs:142:9
   5:     0x7ff2f8e99f50 - core::fmt::write::hf465a4ba34489409
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/mod.rs:1117:17
   6:     0x7ff2f8e2bc1f - std::io::Write::write_fmt::hf34ad5986fa99e89
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/io/mod.rs:1763:15
   7:     0x7ff2f8e37ae4 - std::sys_common::backtrace::_print::h5aa7f1d99916c125
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7ff2f8e37ae4 - std::sys_common::backtrace::print::h036d85b5c81889eb
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7ff2f8e3a777 - std::panicking::default_hook::{{closure}}::h9b311bcc8d2b2a40
  10:     0x7ff2f8e3a4df - std::panicking::default_hook::hd7a03fd029ce4ee2
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:292:9
  11:     0x562a67807c0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h270fbeb056d900dc
  12:     0x562a67807703 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h410a2f5534eafaf7
  13:     0x7ff2f8e3aeb8 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h079168172b9ee18d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2021:9
  14:     0x7ff2f8e3aeb8 - std::panicking::rust_panic_with_hook::h9ec5267af19ebd61
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:783:13
  15:     0x7ff2f8e3abd9 - std::panicking::begin_panic_handler::{{closure}}::hded4ae2a191a7bae
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:649:13
  16:     0x7ff2f8e381c6 - std::sys_common::backtrace::__rust_end_short_backtrace::h3b03f6ccd27da73f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7ff2f8e3a972 - rust_begin_unwind
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:645:5
  18:     0x7ff2f8e96675 - core::panicking::panic_fmt::h290f6f1be63b094c
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:72:14
  19:     0x562a6771f0f9 - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty_ref::hc7a33c50facce4c2
  20:     0x562a67719e4d - kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_ty::h5c4ce3ff3166927f
  21:     0x562a67778d15 - core::ops::function::impls::<impl core::ops::function::FnMut<A> for &mut F>::call_mut::hb3913b6f5302be31
  22:     0x562a6774425d - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h96f4de5184c93e21
  23:     0x562a6772545a - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h4c599cf142ad3eae
  24:     0x562a6775aded - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::hc367daaf74d3c1cb
  25:     0x562a6775fcf5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h2ef5769ca04f3bc4
  26:     0x7ff2f7d80fd9 - rustc_interface[90d65b0f51490bf6]::passes::start_codegen
  27:     0x7ff2f7d80a96 - <rustc_interface[90d65b0f51490bf6]::queries::Queries>::ongoing_codegen
  28:     0x7ff2f7d43693 - std[d7fc13cc5242579e]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>
  29:     0x7ff2f7d42909 - <<std[d7fc13cc5242579e]::thread::Builder>::spawn_unchecked_<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#1} as core[53bdee0566a68c19]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  30:     0x7ff2f8e45c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he310d06a8f297797
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  31:     0x7ff2f8e45c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h69350f715ad37c20
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  32:     0x7ff2f8e45c85 - std::sys::unix::thread::Thread::new::thread_start::h7310dea1d780d6a0
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys/unix/thread.rs:108:17
  33:     0x7ff2f31bd9eb - <unknown>
  34:     0x7ff2f32417cc - <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] current codegen item: declare_function: std::ptr::drop_in_place::<dyn* std::future::Future<Output = usize>>
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2023-10-31-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/mod.rs", function: None, start_line: 498, start_col: Some(1), end_line: 498, end_col: Some(56) }
error: /home/matthias/.kani/kani-0.40.0/bin/kani-compiler exited with status exit status: 101
``

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Bug This is a bug. Something isn't working. [F] Crash Kani crashed
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@matthiaskrgr @zhassan-aws