ICE Function {func} should've been declared before usage

[matthiaskrgr]

I tried this code:

use std::convert;
#[kani::proof]
fn main() {
    let iterator = [[0, 1], [2, 3], [4, 5]].iter();
    let _ = iterator.flat_map(convert::identity);
}

using the following command line invocation:
kani file.rs

<command>

with Kani version:
0.29.0

I expected to see this happen: explanation

Instead, this happened: explanation

thread 'rustc' panicked at 'Function `{func}` should've been declared before usage', kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:713:18
stack backtrace:
   0:     0x7fb3c9768cc3 - std::backtrace_rs::backtrace::libunwind::trace::h6dd260ccf76e2a16
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7fb3c9768cc3 - std::backtrace_rs::backtrace::trace_unsynchronized::h60e795a392c2d181
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fb3c9768cc3 - std::sys_common::backtrace::_print_fmt::hb92bc719d8e89e18
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7fb3c9768cc3 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h433d7296fbd4df36
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fb3c97c9c0f - core::fmt::rt::Argument::fmt::hee863a126433a5fe
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/rt.rs:138:9
   5:     0x7fb3c97c9c0f - core::fmt::write::hecf019f127565c17
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/fmt/mod.rs:1105:21
   6:     0x7fb3c975bd91 - std::io::Write::write_fmt::h4fdee205f020a023
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/io/mod.rs:1712:15
   7:     0x7fb3c9768ad5 - std::sys_common::backtrace::_print::h63f1eb292c01c01d
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7fb3c9768ad5 - std::sys_common::backtrace::print::h29fa6d106f41082b
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7fb3c976b697 - std::panicking::default_hook::{{closure}}::h24c419639c3568dd
  10:     0x7fb3c976b485 - std::panicking::default_hook::hd5faae45a4c2ae6b
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:288:9
  11:     0x5596f8b48dfd - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h62fc73136c5344f5
  12:     0x5596f8b75d83 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::he03976a598c31555
  13:     0x7fb3c976bdd5 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h8fd551c79732d109
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1976:9
  14:     0x7fb3c976bdd5 - std::panicking::rust_panic_with_hook::hff0f13fd32920cda
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:695:13
  15:     0x7fb3c976bb49 - std::panicking::begin_panic_handler::{{closure}}::h4b94c172e12e7b79
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:582:13
  16:     0x7fb3c9769106 - std::sys_common::backtrace::__rust_end_short_backtrace::h0d54fda82a2d0073
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys_common/backtrace.rs:150:18
  17:     0x7fb3c976b8a2 - rust_begin_unwind
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/panicking.rs:578:5
  18:     0x7fb3c97c5eb3 - core::panicking::panic_fmt::h423e755c13523a61
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:67:14
  19:     0x7fb3c97c5c33 - core::panicking::panic_display::h01cf4a7ce4385c77
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:150:5
  20:     0x7fb3c97c5c33 - core::panicking::panic_str::hdd6b73dc916395d6
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/panicking.rs:134:5
  21:     0x7fb3c97c5c33 - core::option::expect_failed::ha0d44cf5519131f2
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/core/src/option.rs:1952:5
  22:     0x5596f8adef0d - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_func_symbol::hfdfa70778fe18c25
  23:     0x5596f8adf28b - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_fn_item::h71825e7c5fcc0189
  24:     0x5596f8adfaa9 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local_fndef::h726060b199e24099
  25:     0x5596f8adfd6e - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local::hc48f55ce59684ce4
  26:     0x5596f8ae2af0 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::h86a6ec769a929295
  27:     0x5596f8ad7412 - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_operand::h1cf8df7b9c8d9784
  28:     0x5596f8b9aa37 - <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold::hab8f04c70ce6eef4
  29:     0x5596f8bbf295 - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::h0f58122ed8acec60
  30:     0x5596f8ae3fc0 - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h1127b89cb2c9781c
  31:     0x5596f8af1148 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::hf245d0e3b1ff69c3
  32:     0x5596f8b06f80 - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::h976e66498994fa63
  33:     0x5596f8b3173e - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::h72b866e5cefa4cb6
  34:     0x5596f8b356d1 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::hd63a249ce3b650de
  35:     0x7fb3cbbe4e26 - rustc_interface[bc622c2a0f547140]::passes::start_codegen
  36:     0x7fb3cbbe2314 - <rustc_middle[913649502f287e96]::ty::context::GlobalCtxt>::enter::<<rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<alloc[ab6e9888d17cae42]::boxed::Box<dyn core[7ab4a128a7734c10]::any::Any>, rustc_span[14f600a439c86087]::ErrorGuaranteed>>
  37:     0x7fb3cbbe1098 - <rustc_interface[bc622c2a0f547140]::queries::Queries>::ongoing_codegen
  38:     0x7fb3cbbe087b - <rustc_interface[bc622c2a0f547140]::interface::Compiler>::enter::<rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}::{closure#2}, core[7ab4a128a7734c10]::result::Result<core[7ab4a128a7734c10]::option::Option<rustc_interface[bc622c2a0f547140]::queries::Linker>, rustc_span[14f600a439c86087]::ErrorGuaranteed>>
  39:     0x7fb3cbbde86f - rustc_span[14f600a439c86087]::set_source_map::<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  40:     0x7fb3cbbddf00 - std[f87cae68a756700d]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>
  41:     0x7fb3cbbdd821 - <<std[f87cae68a756700d]::thread::Builder>::spawn_unchecked_<rustc_interface[bc622c2a0f547140]::util::run_in_thread_pool_with_globals<rustc_interface[bc622c2a0f547140]::interface::run_compiler<core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>, rustc_driver_impl[91ccd4f5692da35d]::run_compiler::{closure#1}>::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[7ab4a128a7734c10]::result::Result<(), rustc_span[14f600a439c86087]::ErrorGuaranteed>>::{closure#1} as core[7ab4a128a7734c10]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  42:     0x7fb3c9776305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hdbaea59c5dcd35ae
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9
  43:     0x7fb3c9776305 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::hedf781cff528734a
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/alloc/src/boxed.rs:1962:9
  44:     0x7fb3c9776305 - std::sys::unix::thread::Thread::new::thread_start::h8db1b8acf05cf216
                               at /rustc/f4956053816439a5884cb2ad1247835858f92218/library/std/src/sys/unix/thread.rs:108:17
  45:     0x7fb3c9428bb5 - <unknown>
  46:     0x7fb3c94aad90 - <unknown>
  47:                0x0 - <unknown>

Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::iter::Map::<std::slice::Iter<'_, [i32; 2]>, fn(&[i32; 2]) -> &[i32; 2] {std::convert::identity::<&[i32; 2]>}>::new
_RNvMNtNtNtCsg38raRqfonS_4core4iter8adapters3mapINtB2_3MapINtNtNtB8_5slice4iter4IterAlj2_EINvNtB8_7convert8identityRB1j_EE3newCslRPOMfBE18J_17flat_map_identity
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2023-04-29-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs", function: None, start_line: 68, start_col: Some(5), end_line: 68, end_col: Some(59) }
error: /home/matthias/.kani/kani-0.29.0/bin/kani-compiler exited with status exit status: 101

[matthiaskrgr]

Still crashing with 0.40