Open matthiaskrgr opened 1 year ago
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 ....
For the record, even with #[kani::unwind(1)], symbolic execution runs for more than 5 minutes without terminating.
#[kani::unwind(1)]
I tried this code:
issue-21291.rs
using the following command line invocation:
with Kani version: 0.34.0
I expected to see this happen: explanation
Instead, this happened: explanation