Kani should not print warnings about concurrency primitives (as long as it's single-threaded)

[fzaiser]

As mentioned in https://github.com/model-checking/kani/pull/1452#discussion_r938945779, users will often be greeted by messages of the form Kani does not support concurrency for now. {} in {} treated as a sequential operation.. For instance, if you're compiling tokio, you get the following output:

WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3305 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3306 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3307 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3308 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2960 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2961 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2962 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3028 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3030 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3032 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3033 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3034 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3036 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3037 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3039 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3041 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3042 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3043 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3045 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3046 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3047 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3048 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <<std::sync::Mutex<T> as std::fmt::Debug>::fmt::LockedPlaceholder as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN129_$LT$$LT$std..sync..mutex..Mutex$LT$T$GT$$u20$as$u20$core..fmt..Debug$GT$..fmt..LockedPlaceholder$u20$as$u20$core..fmt..Debug$GT$3fmt17hfa13453a5ad73070E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&usize as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRjNtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <futures_io::Error as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN58_$LT$std..io..error..Error$u20$as$u20$core..fmt..Debug$GT$3fmt17h57fbb5ea577dca77E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::thread::AccessError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN68_$LT$std..thread..local..AccessError$u20$as$u20$core..fmt..Debug$GT$3fmt17h3d116f9f58b0e37fE
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <tokio::loom::std::atomic_usize::AtomicUsize as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXs3_NtNtNtCs43oGvCTZBYr_5tokio4loom3std12atomic_usizeNtB5_11AtomicUsizeNtNtCs4YygHDVoDdI_4core3fmt5Debug3fmt
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <tokio::sync::task::atomic_waker::AtomicWaker as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXs2_NtNtNtCs43oGvCTZBYr_5tokio4sync4task12atomic_wakerNtB5_11AtomicWakerNtNtCs4YygHDVoDdI_4core3fmt5Debug3fmt
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&str as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtReNtB5_5Debug3fmtCs4DXZRR6gaHf_3log
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3305 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3306 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3307 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3308 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2960 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2961 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2962 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3028 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3030 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3032 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3033 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3034 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3036 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3037 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3039 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3041 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3042 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3043 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3045 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3046 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3047 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3048 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN242_$LT$std..error..$LT$impl$u20$core..convert..From$LT$alloc..string..String$GT$$u20$for$u20$alloc..boxed..Box$LT$dyn$u20$std..error..Error$u2b$core..marker..Sync$u2b$core..marker..Send$GT$$GT$..from..StringError$u20$as$u20$core..fmt..Debug$GT$3fmt17h596233209d8b7714E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::fmt::Display>::fmt, attempted lookup for symbol name: _ZN244_$LT$std..error..$LT$impl$u20$core..convert..From$LT$alloc..string..String$GT$$u20$for$u20$alloc..boxed..Box$LT$dyn$u20$std..error..Error$u2b$core..marker..Sync$u2b$core..marker..Send$GT$$GT$..from..StringError$u20$as$u20$core..fmt..Display$GT$3fmt17h3109561963b528c8E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::error::Error>::source, attempted lookup for symbol name: _RNvYNtNvXs1_NtCsfcET2xiHyR1_3std5errorINtNtCsbutnkbugfxH_5alloc5boxed3BoxDNtBa_5ErrorNtNtCs4YygHDVoDdI_4core6marker4SyncNtB1n_4SendEL_EINtNtB1p_7convert4FromNtNtBF_6string6StringE4from11StringErrorB1a_6sourceCs9FYAfFSAVYQ_3mio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::error::Error>::type_id, attempted lookup for symbol name: _RNvYNtNvXs1_NtCsfcET2xiHyR1_3std5errorINtNtCsbutnkbugfxH_5alloc5boxed3BoxDNtBa_5ErrorNtNtCs4YygHDVoDdI_4core6marker4SyncNtB1n_4SendEL_EINtNtB1p_7convert4FromNtNtBF_6string6StringE4from11StringErrorB1a_7type_idCs9FYAfFSAVYQ_3mio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::error::Error>::backtrace, attempted lookup for symbol name: _RNvYNtNvXs1_NtCsfcET2xiHyR1_3std5errorINtNtCsbutnkbugfxH_5alloc5boxed3BoxDNtBa_5ErrorNtNtCs4YygHDVoDdI_4core6marker4SyncNtB1n_4SendEL_EINtNtB1p_7convert4FromNtNtBF_6string6StringE4from11StringErrorB1a_9backtraceCs9FYAfFSAVYQ_3mio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::error::Error>::description, attempted lookup for symbol name: _ZN243_$LT$std..error..$LT$impl$u20$core..convert..From$LT$alloc..string..String$GT$$u20$for$u20$alloc..boxed..Box$LT$dyn$u20$std..error..Error$u2b$core..marker..Sync$u2b$core..marker..Send$GT$$GT$..from..StringError$u20$as$u20$std..error..Error$GT$11description17hf765c17a6ae77acfE
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::error::Error>::cause, attempted lookup for symbol name: _RNvYNtNvXs1_NtCsfcET2xiHyR1_3std5errorINtNtCsbutnkbugfxH_5alloc5boxed3BoxDNtBa_5ErrorNtNtCs4YygHDVoDdI_4core6marker4SyncNtB1n_4SendEL_EINtNtB1p_7convert4FromNtNtBF_6string6StringE4from11StringErrorB1a_5causeCs9FYAfFSAVYQ_3mio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::error::<impl std::convert::From<std::string::String> for std::boxed::Box<(dyn std::error::Error + std::marker::Send + std::marker::Sync + 'static)>>::from::StringError as std::error::Error>::provide, attempted lookup for symbol name: _RNvYNtNvXs1_NtCsfcET2xiHyR1_3std5errorINtNtCsbutnkbugfxH_5alloc5boxed3BoxDNtBa_5ErrorNtNtCs4YygHDVoDdI_4core6marker4SyncNtB1n_4SendEL_EINtNtB1p_7convert4FromNtNtBF_6string6StringE4from11StringErrorB1a_7provideCs9FYAfFSAVYQ_3mio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&std::vec::Vec<u8> as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRINtNtCsbutnkbugfxH_5alloc3vec3VechENtB5_5Debug3fmtCs43oGvCTZBYr_5tokio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&std::time::Duration as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRNtNtB7_4time8DurationNtB5_5Debug3fmtCsaQ5MVki7BDy_7socket2
warning: Found the following unsupported constructs:
             - Rvalue::ThreadLocalRef (6)
             - drop_in_place for drop_unimplemented__RINvNtCs4YygHDVoDdI_4core3ptr13drop_in_placeNtNtNtNtCs43oGvCTZBYr_5tokio4sync4task12atomic_waker11AtomicWakerEBO_ (1)
         
         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.

WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&usize as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRjNtB5_5Debug3fmtCs43Jws2ifaqL_15futures_channel
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&bool as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRbNtB5_5Debug3fmtCs43Jws2ifaqL_15futures_channel
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&std::vec::Vec<u8> as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRINtNtCsbutnkbugfxH_5alloc3vec3VechENtB5_5Debug3fmtCs43oGvCTZBYr_5tokio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&futures_io::Error as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRNtNtNtCsfcET2xiHyR1_3std2io5error5ErrorNtB5_5Debug3fmtCs43oGvCTZBYr_5tokio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&() as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRuNtB5_5Debug3fmtCs4ve6hHYRnOw_16parking_lot_core
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&bytes::BytesMut as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRNtNtCshtrNijB0EoG_5bytes9bytes_mut8BytesMutNtB5_5Debug3fmtCs43oGvCTZBYr_5tokio
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&std::option::Option<usize> as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRINtNtB7_6option6OptionjENtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::sync::Arc<tokio::sync::Semaphore> as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsE_NtCsbutnkbugfxH_5alloc4syncINtB5_3ArcNtNtNtCs43oGvCTZBYr_5tokio4sync9semaphore9SemaphoreENtNtCs4YygHDVoDdI_4core3fmt5Debug3fmtBM_
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&u64 as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRyNtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
warning: Found the following unsupported constructs:
             - Rvalue::ThreadLocalRef (7)
             - drop_in_place for drop_unimplemented__RINvNtCs4YygHDVoDdI_4core3ptr13drop_in_placeNtNtNtCsfcET2xiHyR1_3std2io5error5ErrorECs9FYAfFSAVYQ_3mio (1)
             - try (1)
         
         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: `tokio-test` (lib) generated 1 warning
warning: `tokio-util` (lib) generated 4 warnings
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&u32 as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRmNtB5_5Debug3fmtCs4DXZRR6gaHf_3log
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&() as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRuNtB5_5Debug3fmtCs4ve6hHYRnOw_16parking_lot_core
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&&str as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRReNtB5_5Debug3fmtCs4DXZRR6gaHf_3log
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&u8 as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRhNtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&i32 as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRlNtB5_5Debug3fmtCse9dO0SfHQET_4libc
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&std::option::Option<usize> as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRINtNtB7_6option6OptionjENtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&bool as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRbNtB5_5Debug3fmtCs4ve6hHYRnOw_16parking_lot_core
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&std::option::Option<u32> as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRINtNtB7_6option6OptionmENtB5_5Debug3fmtCs4DXZRR6gaHf_3log
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::thread::AccessError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN68_$LT$std..thread..local..AccessError$u20$as$u20$core..fmt..Debug$GT$3fmt17h3d116f9f58b0e37fE
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::cell::BorrowError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN60_$LT$core..cell..BorrowError$u20$as$u20$core..fmt..Debug$GT$3fmt17h4c4d5842ef5efbd5E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::cell::BorrowMutError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN63_$LT$core..cell..BorrowMutError$u20$as$u20$core..fmt..Debug$GT$3fmt17h8a41a0130d49cfbdE
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::string::FromUtf8Error as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN65_$LT$alloc..string..FromUtf8Error$u20$as$u20$core..fmt..Debug$GT$3fmt17h3948c6a593737b3aE
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::ffi::NulError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN64_$LT$alloc..ffi..c_str..NulError$u20$as$u20$core..fmt..Debug$GT$3fmt17h18e4eb7c84a81c03E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::io::Error as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN58_$LT$std..io..error..Error$u20$as$u20$core..fmt..Debug$GT$3fmt17h57fbb5ea577dca77E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <! as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN42_$LT$$u21$$u20$as$u20$core..fmt..Debug$GT$3fmt17h7731a922cd7e8301E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <std::num::TryFromIntError as std::fmt::Debug>::fmt, attempted lookup for symbol name: _ZN70_$LT$core..num..error..TryFromIntError$u20$as$u20$core..fmt..Debug$GT$3fmt17h699ff305d5b9c9e8E
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&usize as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRjNtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
WARN kani_compiler::codegen_cprover_gotoc::codegen::rvalue Unable to find vtable symbol for virtual function <&u64 as std::fmt::Debug>::fmt, attempted lookup for symbol name: _RNvXsV_NtCs4YygHDVoDdI_4core3fmtRyNtB5_5Debug3fmtCsb2tXkiy4HHk_6memchr
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3305 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3306 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3307 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_fence_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3308 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2995 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2991 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2992 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2993 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2994 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2995 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2991 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2992 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2993 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xadd_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2994 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xor_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3155 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xor_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3151 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xor_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3152 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xor_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3153 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xor_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3154 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2960 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2961 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2962 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2960 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2961 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2962 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2960 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2961 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_load_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2962 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2979 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2975 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2976 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2977 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2978 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2979 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2975 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2976 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2977 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2978 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2979 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2975 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2976 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2977 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_xchg_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2978 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_store_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2946 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_store_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2947 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_store_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2948 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_store_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2946 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_store_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2947 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_store_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:2948 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3028 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3030 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3032 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3033 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3034 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3036 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3037 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3039 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3041 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3042 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3043 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3045 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3046 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3047 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3048 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3028 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3030 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_relaxed_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3032 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3033 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3034 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acquire_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3036 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3037 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3039 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_release_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3041 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3042 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3043 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_acqrel_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3045 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3046 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3047 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchg_seqcst_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3048 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_relaxed_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3070 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_relaxed_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3072 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_relaxed_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3074 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_acquire_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3075 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_acquire_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3076 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_acquire_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3078 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_release_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3079 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_release_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3081 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_release_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3083 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_acqrel_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3084 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_acqrel_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3085 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_acqrel_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3087 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_seqcst_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3088 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_seqcst_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3089 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_cxchgweak_seqcst_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3090 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_or_relaxed` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3140 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_or_seqcst` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3136 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_or_acquire` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3137 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_or_release` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3138 treated as a sequential operation.
WARN kani_compiler::codegen_cprover_gotoc::codegen::intrinsic Kani does not support concurrency for now. `atomic_or_acqrel` in /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs:3139 treated as a sequential operation.

This causes several problems:

• it's very noisy: the user does not get actionable feedback from it. They can do nothing to silence the warnings
• it lowers user trust: users might think that Kani does not actually support the program or that the analysis is unsound but
• Kani's analysis is still sound because it only supports single-threaded execution for now

I agree that we have to be careful about this if/when we introduce multi-threading, but printing warnings all the time does not seem to be the best path forward to me.

[celinval]

I'm not sure we should remove them, but we should definitely merge the warning messages like we did with unsupported constructs.

[tedinski]

Could we merge this into the unsupported constructs mechanism? e.g. just report "concurrency" as the unsupported feature (but not need to codegen unimplemented.)

[celinval]

I'm thinking about implementing a very similar mechanism to print a summary at the end