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

hang with thread join #2684

Open
matthiaskrgr opened this issue Aug 14, 2023 · 1 comment
Open

hang with thread join #2684

matthiaskrgr opened this issue Aug 14, 2023 · 1 comment
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@matthiaskrgr
Copy link
Contributor

I tried this code:

issue-21291.rs

use std::thread;

#[kani::proof]
fn main() {
    thread::spawn(|| {}).join().unwrap()
}

using the following command line invocation:

kani f.rs

with Kani version: 0.34.0

I expected to see this happen: explanation

Instead, this happened: explanation

warning: Found the following unsupported constructs:
             - caller_location (1)
             - foreign function (29)
             - try (3)

         Verification will fail if one or more of these constructs is reachable.
         See https://model-checking.github.io/kani/rust-feature-support.html for more details.

warning: Kani currently does not support concurrency. The following constructs will be treated as sequential operations:
             - atomic_cxchg_acqrel_relaxed (2)
             - atomic_cxchgweak_relaxed_seqcst (2)
             - atomic_cxchg_acquire_relaxed (2)
             - atomic_cxchg_seqcst_relaxed (2)
             - atomic_cxchg_release_relaxed (2)
             - atomic_store_release (3)
             - atomic_cxchg_relaxed_relaxed (2)
             - atomic_xchg_acquire (1)
             - atomic_fence_release (1)
             - atomic_fence_seqcst (1)
             - atomic_cxchgweak_seqcst_acquire (2)
             - atomic_xsub_seqcst (2)
             - atomic_cxchgweak_acqrel_acquire (2)
             - atomic_load_seqcst (5)
             - atomic_cxchgweak_acquire_acquire (2)
             - atomic_xsub_release (2)
             - atomic_cxchg_seqcst_seqcst (2)
             - atomic_xadd_seqcst (2)
             - atomic_store_relaxed (3)
             - atomic_xadd_release (2)
             - atomic_cxchg_acquire_seqcst (2)
             - atomic_cxchg_acqrel_seqcst (2)
             - atomic_cxchg_release_seqcst (2)
             - atomic_cxchgweak_relaxed_acquire (2)
             - atomic_cxchg_relaxed_seqcst (2)
             - atomic_cxchgweak_release_acquire (2)
             - atomic_xchg_seqcst (1)
             - atomic_xchg_release (1)
             - atomic_store_seqcst (3)
             - atomic_fence_acquire (1)
             - atomic_cxchgweak_seqcst_relaxed (2)
             - atomic_xsub_acqrel (2)
             - atomic_cxchgweak_acqrel_relaxed (2)
             - atomic_xsub_relaxed (2)
             - atomic_cxchgweak_acquire_relaxed (2)
             - atomic_cxchg_seqcst_acquire (2)
             - atomic_xadd_acqrel (2)
             - atomic_cxchg_acqrel_acquire (2)
             - atomic_xadd_relaxed (2)
             - atomic_cxchg_acquire_acquire (2)
             - atomic_load_relaxed (5)
             - atomic_cxchg_release_acquire (2)
             - atomic_cxchgweak_relaxed_relaxed (2)
             - atomic_cxchg_relaxed_acquire (2)
             - atomic_cxchgweak_release_relaxed (2)
             - atomic_xchg_acqrel (1)
             - atomic_fence_acqrel (1)
             - atomic_xchg_relaxed (1)
             - atomic_cxchgweak_seqcst_seqcst (2)
             - atomic_cxchgweak_acqrel_seqcst (2)
             - atomic_xsub_acquire (2)
             - atomic_cxchgweak_acquire_seqcst (2)
             - thread local (replaced by static variable) (15)
             - atomic_cxchgweak_release_seqcst (2)
             - atomic_load_acquire (5)
             - atomic_xadd_acquire (2)

warning: 2 warnings emitted

Checking harness main...
CBMC 5.89.0 (cbmc-5.89.0)
CBMC version 5.89.0 (cbmc-5.89.0) 64-bit x86_64 linux
Reading GOTO program from file /tmp/kani/f_main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 1 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 2 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 3 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 4 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 5 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 6 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 7 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 8 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 9 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 10 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 11 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 12 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 13 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 14 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
Unwinding loop _RNvNtNtCslCQv6bAYqnx_4core5slice6memchr12memchr_naiveCsbvU2WjmIQuJ_1f.0 iteration 15 file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/memchr.rs line 56 column 5 function core::slice::memchr::memchr_naive thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ffi/c_str.rs line 384 column 15 function std::ffi::CStr::from_bytes_with_nul thread 0
aborting path on assume(false) at file /github/home/.cargo/registry/src/index.crates.io-6f17d22bba15001f/libc-0.2.147/src/unix/mod.rs line 540 column 5 function std::sys::unix::os::getenv::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/sys/common/small_c_string.rs line 30 column 44 function std::sys::common::small_c_string::run_with_cstr::<*const i8, [closure@std::sys::unix::os::getenv::{closure#0}]> thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 266 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 259 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 977 column 15 function std::option::Option::<std::io::ErrorKind>::unwrap_or_else::<[closure@std::io::error::repr_bitpacked::decode_repr<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0}]> thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 280 column 13 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]> thread 0
aborting path on assume(false) at  thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::Error> iteration 1
Unwinding recursion std::ptr::drop_in_place::<std::io::error::repr_bitpacked::Repr> iteration 1
Unwinding recursion <std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop iteration 1
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 266 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 259 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 977 column 15 function std::option::Option::<std::io::ErrorKind>::unwrap_or_else::<[closure@std::io::error::repr_bitpacked::decode_repr<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0}]> thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 280 column 13 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]> thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::error::ErrorData<std::boxed::Box<std::io::error::Custom>>> iteration 1
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<std::io::error::Custom>> iteration 1
Unwinding recursion std::ptr::drop_in_place::<std::io::error::Custom> iteration 1
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>> iteration 1
aborting path on assume(false) at  thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::Error> iteration 2
Unwinding recursion std::ptr::drop_in_place::<std::io::error::repr_bitpacked::Repr> iteration 2
Unwinding recursion <std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop iteration 2
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 266 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 259 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 977 column 15 function std::option::Option::<std::io::ErrorKind>::unwrap_or_else::<[closure@std::io::error::repr_bitpacked::decode_repr<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0}]> thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 280 column 13 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]> thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::error::ErrorData<std::boxed::Box<std::io::error::Custom>>> iteration 2
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<std::io::error::Custom>> iteration 2
Unwinding recursion std::ptr::drop_in_place::<std::io::error::Custom> iteration 2
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>> iteration 2
aborting path on assume(false) at  thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::Error> iteration 3
Unwinding recursion std::ptr::drop_in_place::<std::io::error::repr_bitpacked::Repr> iteration 3
Unwinding recursion <std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop iteration 3
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 266 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 259 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 977 column 15 function std::option::Option::<std::io::ErrorKind>::unwrap_or_else::<[closure@std::io::error::repr_bitpacked::decode_repr<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0}]> thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 280 column 13 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]> thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::error::ErrorData<std::boxed::Box<std::io::error::Custom>>> iteration 3
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<std::io::error::Custom>> iteration 3
Unwinding recursion std::ptr::drop_in_place::<std::io::error::Custom> iteration 3
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>> iteration 3
aborting path on assume(false) at  thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::Error> iteration 4
Unwinding recursion std::ptr::drop_in_place::<std::io::error::repr_bitpacked::Repr> iteration 4
Unwinding recursion <std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop iteration 4
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/hint.rs line 105 column 9 function std::hint::unreachable_unchecked thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 266 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 259 column 17 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0} thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs line 977 column 15 function std::option::Option::<std::io::ErrorKind>::unwrap_or_else::<[closure@std::io::error::repr_bitpacked::decode_repr<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]>::{closure#0}]> thread 0
aborting path on assume(false) at file /github/home/.rustup/toolchains/nightly-2023-08-04-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/io/error/repr_bitpacked.rs line 280 column 13 function std::io::error::repr_bitpacked::decode_repr::<std::boxed::Box<std::io::error::Custom>, [closure@<std::io::error::repr_bitpacked::Repr as std::ops::Drop>::drop::{closure#0}]> thread 0
Unwinding recursion std::ptr::drop_in_place::<std::io::error::ErrorData<std::boxed::Box<std::io::error::Custom>>> iteration 4
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<std::io::error::Custom>> iteration 4
Unwinding recursion std::ptr::drop_in_place::<std::io::error::Custom> iteration 4
Unwinding recursion std::ptr::drop_in_place::<std::boxed::Box<dyn std::error::Error + std::marker::Send + std::marker::Sync>> iteration 4
aborting path on assume(false) at  thread 0
....
@matthiaskrgr matthiaskrgr added the [C] Bug This is a bug. Something isn't working. label Aug 14, 2023
@zhassan-aws
Copy link
Contributor

For the record, even with #[kani::unwind(1)], symbolic execution runs for more than 5 minutes without terminating.

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.
Projects
None yet
Milestone
No milestone
Development

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