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: assertion failed: value <= (0xFFFF_FF00 as usize #2258

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

ICE: assertion failed: value <= (0xFFFF_FF00 as usize #2258

matthiaskrgr opened this issue Mar 2, 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:

// run-pass
#![feature(extern_types)]

use std::mem::{align_of_val, size_of_val};

extern "C" {
    type A;
}

#[kani::proof]
fn main() {
    let x: &A = unsafe { &*(1usize as *const A) };
    let _ = size_of_val(x);
}

using the following command line invocation:

kani file.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

warning: unused import: `align_of_val`
 --> extern-types-size_of_val.rs:4:16
  |
4 | use std::mem::{align_of_val, size_of_val};
  |                ^^^^^^^^^^^^
  |
  = note: `#[warn(unused_imports)]` on by default

thread '<unnamed>' panicked at 'index out of bounds: the len is 0 but the index is 18446744073709551615', /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/compiler/rustc_abi/src/lib.rs:1131:59
stack backtrace:
   0:     0x7f52323667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f52323667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f52323667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7f52323667da - <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:     0x7f52323c92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7f5232356c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7f52323665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7f52323665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7f52323692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7f523236902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x556522faeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x556522f04f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7f5232369b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7f5232369b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7f52323698a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
  15:     0x7f5232366c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7f52323695b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7f52323c5cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x7f52323c5ea2 - core::panicking::panic_bounds_check::hbf14e7c69f92d977
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:147:5
  19:     0x556522e74f51 - <rustc_abi[e7ecad2586626d90]::FieldsShape>::offset
  20:     0x556522eb1551 - kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::size_and_align_of_dst::h702e08173932e15e
  21:     0x556522ea23c5 - kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_intrinsic::h220d0404366aa022
  22:     0x556522edad31 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::hba20b41c6ebc6f6b
  23:     0x556522e7f15d - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  24:     0x556522f0abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  25:     0x556522f964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  26:     0x7f5234886fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  27:     0x7f5234886ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  28:     0x7f52348847a6 - <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>>
  29:     0x7f5234881a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  30:     0x7f5234880f67 - <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>>
  31:     0x7f523487bf88 - 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}>
  32:     0x7f523487ba75 - <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>>
  33:     0x7f523487b062 - 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>>
  34:     0x7f5234eec49e - <<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}
  35:     0x7f52363da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  36:     0x7f52363da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  37:     0x7f52363da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  38:     0x7f523201dbb5 - <unknown>
  39:     0x7f523209fd90 - <unknown>
  40:                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_function: std::mem::size_of_val::<A>
_RINvNtCshQhm45nWocF_4core3mem11size_of_valNvCshRRJ639Q1Eo_24extern_types_size_of_val1AEBG_
[Kani] current codegen location: Loc { file: "/home/runner/.rustup/toolchains/nightly-2022-12-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/mem/mod.rs", function: None, start_line: 336, start_col: Some(1), end_line: 336, end_col: Some(54) }
warning: 1 warning emitted

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 2, 2023
@zhassan-aws zhassan-aws added the [F] Crash Kani crashed label Mar 2, 2023
@matthiaskrgr matthiaskrgr changed the title ICE: index out of bounds: extern_types ICE: assertion failed: value <= (0xFFFF_FF00 as usize Nov 12, 2023
@matthiaskrgr
Copy link
Contributor Author

with 0.40, this now crashes with

Kani Rust Verifier 0.40.0 (standalone)
warning: unused import: `align_of_val`
 --> a.rs:4:16
  |
4 | use std::mem::{align_of_val, size_of_val};
  |                ^^^^^^^^^^^^
  |
  = note: `#[warn(unused_imports)]` on by default

thread 'rustc' panicked at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/compiler/rustc_target/src/abi/mod.rs:22:1:
assertion failed: value <= (0xFFFF_FF00 as usize)
stack backtrace:
   0:     0x7f4cbeb69cfc - std::backtrace_rs::backtrace::libunwind::trace::h974857262e179b17
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7f4cbeb69cfc - std::backtrace_rs::backtrace::trace_unsynchronized::h6adce2053c056ac9
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f4cbeb69cfc - std::sys_common::backtrace::_print_fmt::hcf2018a5ad956761
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7f4cbeb69cfc - <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:     0x7f4cbebcbf50 - core::fmt::rt::Argument::fmt::hef0ae15422a7f61d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/rt.rs:142:9
   5:     0x7f4cbebcbf50 - core::fmt::write::hf465a4ba34489409
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/mod.rs:1117:17
   6:     0x7f4cbeb5dc1f - std::io::Write::write_fmt::hf34ad5986fa99e89
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/io/mod.rs:1763:15
   7:     0x7f4cbeb69ae4 - std::sys_common::backtrace::_print::h5aa7f1d99916c125
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7f4cbeb69ae4 - std::sys_common::backtrace::print::h036d85b5c81889eb
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7f4cbeb6c777 - std::panicking::default_hook::{{closure}}::h9b311bcc8d2b2a40
  10:     0x7f4cbeb6c4df - std::panicking::default_hook::hd7a03fd029ce4ee2
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:292:9
  11:     0x55f3a5807c0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h270fbeb056d900dc
  12:     0x55f3a5807703 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h410a2f5534eafaf7
  13:     0x7f4cbeb6ceb8 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h079168172b9ee18d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2021:9
  14:     0x7f4cbeb6ceb8 - std::panicking::rust_panic_with_hook::h9ec5267af19ebd61
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:783:13
  15:     0x7f4cbeb6cbd9 - std::panicking::begin_panic_handler::{{closure}}::hded4ae2a191a7bae
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:649:13
  16:     0x7f4cbeb6a1c6 - std::sys_common::backtrace::__rust_end_short_backtrace::h3b03f6ccd27da73f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7f4cbeb6c972 - rust_begin_unwind
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:645:5
  18:     0x7f4cbebc8675 - core::panicking::panic_fmt::h290f6f1be63b094c
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:72:14
  19:     0x7f4cbebc8713 - core::panicking::panic::hac1e457063a02956
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:127:5
  20:     0x55f3a56c1eff - rustc_abi::FieldsShape<FieldIdx>::offset::h9c9ad3465f713119
  21:     0x55f3a56e5a7b - kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::size_and_align_of_dst::hd62e6a7cfa0d5523
  22:     0x55f3a56dab8c - kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_intrinsic::hf2d15a62797da022
  23:     0x55f3a5712855 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator::h3967cbd0413177f5
  24:     0x55f3a56c3fd1 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::h892262db0bd2a271
  25:     0x55f3a57270ec - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hc439f7b37aa26293
  26:     0x55f3a575b10a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::hc367daaf74d3c1cb
  27:     0x55f3a575fcf5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h2ef5769ca04f3bc4
  28:     0x7f4cc3580fd9 - rustc_interface[90d65b0f51490bf6]::passes::start_codegen
  29:     0x7f4cc3580a96 - <rustc_interface[90d65b0f51490bf6]::queries::Queries>::ongoing_codegen
  30:     0x7f4cc3543693 - 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>>
  31:     0x7f4cc3542909 - <<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}
  32:     0x7f4cbeb77c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he310d06a8f297797
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  33:     0x7f4cbeb77c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h69350f715ad37c20
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  34:     0x7f4cbeb77c85 - std::sys::unix::thread::Thread::new::thread_start::h7310dea1d780d6a0
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys/unix/thread.rs:108:17
  35:     0x7f4cbe81f9eb - <unknown>
  36:     0x7f4cbe8a37cc - <unknown>
  37:                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_function: std::mem::size_of_val::<A>
_RINvNtCs5k6HhVuWWKi_4core3mem11size_of_valNvCsaxqAW6SeOYc_1a1AEBG_
[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/mem/mod.rs", function: None, start_line: 342, start_col: Some(1), end_line: 342, end_col: Some(54) }
warning: 1 warning emitted

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