ICE: Function should've been declared before usage, was: Can't take address of Expr

I tried this code:

#[kani::proof]
fn foo() -> u32 { 42 }

#[kani::proof]
fn main() {
    println!("{:p}", &foo);
    //~^ WARNING taking a reference to a function item does not give a function pointer
}

using the following command line invocation:

kani file.rs

with Kani version: 0.22.0

I expected to see this happen: explanation

Instead, this happened: explanation

warning: taking a reference to a function item does not give a function pointer
 --> a.rs:6:22
  |
6 |     println!("{:p}", &foo);
  |                      ^^^^ help: cast `foo` to obtain a function pointer: `foo as fn() -> _`
  |
  = note: `#[warn(function_item_references)]` on by default

thread '<unnamed>' panicked at 'Can't take address of Expr { value: AddressOf(Expr { value: Symbol { identifier: "_RNvCsbvss9KOnXkz_1a3foo::FnDefSingleton" }, typ: StructTag("tag-_RNvCsbvss9KOnXkz_1a3foo::FnDefStruct"), location: None }), typ: Pointer { typ: StructTag("tag-_RNvCsbvss9KOnXkz_1a3foo::FnDefStruct") }, location: None }', cprover_bindings/src/goto_program/expr.rs:420:9
stack backtrace:
   0:     0x7f25411667da - std::backtrace_rs::backtrace::libunwind::trace::hc84915c67f6fb1e5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
   1:     0x7f25411667da - std::backtrace_rs::backtrace::trace_unsynchronized::h74fef551999c3a2f
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7f25411667da - std::sys_common::backtrace::_print_fmt::h8acfd19c1a6f1d1d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:65:5
   3:     0x7f25411667da - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9271b09f3576b7e0
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7f25411c92ee - core::fmt::write::h27d0bbb767cff1d5
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/fmt/mod.rs:1208:17
   5:     0x7f2541156c65 - std::io::Write::write_fmt::hc409ea2bb818fbea
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/io/mod.rs:1682:15
   6:     0x7f25411665a5 - std::sys_common::backtrace::_print::hfa031a98cf1e4011
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:47:5
   7:     0x7f25411665a5 - std::sys_common::backtrace::print::he69ac0980f15620d
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:34:9
   8:     0x7f25411692ef - std::panicking::default_hook::{{closure}}::h014cf704a69dce2b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:267:22
   9:     0x7f254116902b - std::panicking::default_hook::h380e71f8d8d49df7
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:286:9
  10:     0x557a3c1aeb0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h10f33c4e395bf462
  11:     0x557a3c104f67 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::hf568cc16e5ffa08a
  12:     0x7f2541169b2d - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::hcfa7e50330911a79
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2032:9
  13:     0x7f2541169b2d - std::panicking::rust_panic_with_hook::h483f1ef90c766581
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:692:13
  14:     0x7f25411698a9 - std::panicking::begin_panic_handler::{{closure}}::hd4c7d9116c0ef489
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:579:13
  15:     0x7f2541166c8c - std::sys_common::backtrace::__rust_end_short_backtrace::had27a083c7d7188b
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys_common/backtrace.rs:137:18
  16:     0x7f25411695b2 - rust_begin_unwind
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/panicking.rs:575:5
  17:     0x7f25411c5cd3 - core::panicking::panic_fmt::hbacb72817da3b060
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/core/src/panicking.rs:64:14
  18:     0x557a3c2df7ca - cprover_bindings::goto_program::expr::Expr::address_of::h1636674499f01393
  19:     0x557a3c0c7821 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place_ref::h4b77c777dff90545
  20:     0x557a3c0c8fbb - kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue::h57a2cf71297ecf62
  21:     0x557a3c0d8080 - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h4c6e1c8bf226a338
  22:     0x557a3c07f0d1 - kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::h541ea7f90d847b35
  23:     0x557a3c10abf0 - std::thread::local::LocalKey<T>::with::hb907a536239d23f6
  24:     0x557a3c1964c8 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::heaa499391d53b3f6
  25:     0x7f2543686fa1 - <rustc_session[19dfb3d05ff8562d]::session::Session>::time::<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_interface[aec886e93b1add3f]::passes::start_codegen::{closure#0}>
  26:     0x7f2543686ac9 - rustc_interface[aec886e93b1add3f]::passes::start_codegen
  27:     0x7f25436847a6 - <rustc_interface[aec886e93b1add3f]::passes::QueryContext>::enter::<<rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<alloc[58cfa59ca61fafa9]::boxed::Box<dyn core[6d94cc961ac87456]::any::Any>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  28:     0x7f2543681a46 - <rustc_interface[aec886e93b1add3f]::queries::Queries>::ongoing_codegen
  29:     0x7f2543680f67 - <rustc_interface[aec886e93b1add3f]::interface::Compiler>::enter::<rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}::{closure#2}, core[6d94cc961ac87456]::result::Result<core[6d94cc961ac87456]::option::Option<rustc_interface[aec886e93b1add3f]::queries::Linker>, rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  30:     0x7f254367bf88 - rustc_span[ae2df7aa7c6c667b]::with_source_map::<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  31:     0x7f254367ba75 - <scoped_tls[db87656d258d017b]::ScopedKey<rustc_span[ae2df7aa7c6c667b]::SessionGlobals>>::set::<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  32:     0x7f254367b062 - std[acd1f573e90225f]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>
  33:     0x7f2543cec49e - <<std[acd1f573e90225f]::thread::Builder>::spawn_unchecked_<rustc_interface[aec886e93b1add3f]::util::run_in_thread_pool_with_globals<rustc_interface[aec886e93b1add3f]::interface::run_compiler<core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>, rustc_driver[94a2f0241de75afa]::run_compiler::{closure#1}>::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[6d94cc961ac87456]::result::Result<(), rustc_errors[56887b15c7ec6fbf]::ErrorGuaranteed>>::{closure#1} as core[6d94cc961ac87456]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  34:     0x7f25451da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he955d3e33f115328
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  35:     0x7f25451da2d3 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h32515d9eaa012a19
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/alloc/src/boxed.rs:2000:9
  36:     0x7f25451da2d3 - std::sys::unix::thread::Thread::new::thread_start::h5af9cdd9a5a58d64
                               at /rustc/c6fcdb690609769a240fc8ab0de0ce68d5ea7dba/library/std/src/sys/unix/thread.rs:108:17
  37:     0x7f2540f05bb5 - <unknown>
  38:     0x7f2540f87d90 - <unknown>
  39:                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: <&fn() -> u32 {foo} as std::fmt::Pointer>::fmt
_RNvXsk_NtCshQhm45nWocF_4core3fmtRNvCsbvss9KOnXkz_1a3fooNtB5_7Pointer3fmtBx_
[Kani] current codegen location: Loc { file: "/home/runner/.rustup/toolchains/nightly-2022-12-11-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs", function: None, start_line: 2520, start_col: Some(5), end_line: 2520, end_col: Some(51) }
warning: 1 warning emitted

error: /home/matthias/.kani/kani-0.22.0/bin/kani-compiler exited with status exit status: 101

with kani 0.40, this now crashes with:

Kani Rust Verifier 0.40.0 (standalone)
warning: taking a reference to a function item does not give a function pointer
 --> a.rs:6:22
  |
6 |     println!("{:p}", &foo);
  |                      ^^^^ help: cast `foo` to obtain a function pointer: `foo as fn() -> _`
  |
  = note: `#[warn(function_item_references)]` on by default

thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:720:18:
Function `{func}` should've been declared before usage
stack backtrace:
   0:     0x7fc21e369cfc - std::backtrace_rs::backtrace::libunwind::trace::h974857262e179b17
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/libunwind.rs:104:5
   1:     0x7fc21e369cfc - std::backtrace_rs::backtrace::trace_unsynchronized::h6adce2053c056ac9
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
   2:     0x7fc21e369cfc - std::sys_common::backtrace::_print_fmt::hcf2018a5ad956761
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:67:5
   3:     0x7fc21e369cfc - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h3d39e48ce4d7e36f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:44:22
   4:     0x7fc21e3cbf50 - core::fmt::rt::Argument::fmt::hef0ae15422a7f61d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/rt.rs:142:9
   5:     0x7fc21e3cbf50 - core::fmt::write::hf465a4ba34489409
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/fmt/mod.rs:1117:17
   6:     0x7fc21e35dc1f - std::io::Write::write_fmt::hf34ad5986fa99e89
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/io/mod.rs:1763:15
   7:     0x7fc21e369ae4 - std::sys_common::backtrace::_print::h5aa7f1d99916c125
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:47:5
   8:     0x7fc21e369ae4 - std::sys_common::backtrace::print::h036d85b5c81889eb
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:34:9
   9:     0x7fc21e36c777 - std::panicking::default_hook::{{closure}}::h9b311bcc8d2b2a40
  10:     0x7fc21e36c4df - std::panicking::default_hook::hd7a03fd029ce4ee2
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:292:9
  11:     0x561655807c0d - kani_compiler::session::PANIC_HOOK::{{closure}}::{{closure}}::h270fbeb056d900dc
  12:     0x561655807703 - kani_compiler::codegen_cprover_gotoc::utils::debug::DEFAULT_HOOK::{{closure}}::{{closure}}::h410a2f5534eafaf7
  13:     0x7fc21e36ceb8 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h079168172b9ee18d
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2021:9
  14:     0x7fc21e36ceb8 - std::panicking::rust_panic_with_hook::h9ec5267af19ebd61
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:783:13
  15:     0x7fc21e36cc0e - std::panicking::begin_panic_handler::{{closure}}::hded4ae2a191a7bae
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:657:13
  16:     0x7fc21e36a1c6 - std::sys_common::backtrace::__rust_end_short_backtrace::h3b03f6ccd27da73f
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys_common/backtrace.rs:170:18
  17:     0x7fc21e36c972 - rust_begin_unwind
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/panicking.rs:645:5
  18:     0x7fc21e3c8675 - core::panicking::panic_fmt::h290f6f1be63b094c
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:72:14
  19:     0x7fc21e3c8423 - core::panicking::panic_display::h2c1138d5cf12103e
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:178:5
  20:     0x7fc21e3c8423 - core::panicking::panic_str::h4ec91ecf807e2a19
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/panicking.rs:152:5
  21:     0x7fc21e3c8423 - core::option::expect_failed::hb666b084f64dd703
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/core/src/option.rs:1979:5
  22:     0x5616556f4c6b - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_func_symbol::he115d4854c69882b
  23:     0x5616556f508e - kani_compiler::codegen_cprover_gotoc::codegen::operand::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_fn_item::h1d6f8909544805e9
  24:     0x5616556f5828 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local_fndef::h09dea6bdb887347c
  25:     0x5616556f58cc - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local_fndef::h09dea6bdb887347c
  26:     0x5616556f5b99 - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_local::h3efd492532155a62
  27:     0x5616556f920c - kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::h4dc87b5d60ece886
  28:     0x56165570fa7c - kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement::h67859eadd810316a
  29:     0x5616556c3909 - kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block::h892262db0bd2a271
  30:     0x5616557270ec - kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::hc439f7b37aa26293
  31:     0x56165575b10a - kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::hc367daaf74d3c1cb
  32:     0x56165575fcf5 - <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::h2ef5769ca04f3bc4
  33:     0x7fc222d80fd9 - rustc_interface[90d65b0f51490bf6]::passes::start_codegen
  34:     0x7fc222d80a96 - <rustc_interface[90d65b0f51490bf6]::queries::Queries>::ongoing_codegen
  35:     0x7fc222d43693 - std[d7fc13cc5242579e]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>
  36:     0x7fc222d42909 - <<std[d7fc13cc5242579e]::thread::Builder>::spawn_unchecked_<rustc_interface[90d65b0f51490bf6]::util::run_in_thread_with_globals<rustc_interface[90d65b0f51490bf6]::interface::run_compiler<core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>, rustc_driver_impl[88c66c37425cba72]::run_compiler::{closure#1}>::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[53bdee0566a68c19]::result::Result<(), rustc_span[88faddf4715d2d43]::ErrorGuaranteed>>::{closure#1} as core[53bdee0566a68c19]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  37:     0x7fc21e377c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::he310d06a8f297797
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  38:     0x7fc21e377c85 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h69350f715ad37c20
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/alloc/src/boxed.rs:2007:9
  39:     0x7fc21e377c85 - std::sys::unix::thread::Thread::new::thread_start::h7310dea1d780d6a0
                               at /rustc/31bc7e2c47e82798a392c770611975a6883132c8/library/std/src/sys/unix/thread.rs:108:17
  40:     0x7fc21e1419eb - <unknown>
  41:     0x7fc21e1c57cc - <unknown>
  42:                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: <*const fn() -> u32 {foo} as std::fmt::Pointer>::fmt
_RNvXsg_NtCs5k6HhVuWWKi_4core3fmtPNvCsaxqAW6SeOYc_1a3fooNtB5_7Pointer3fmtBx_
[Kani] current codegen location: Loc { file: "/github/home/.rustup/toolchains/nightly-2023-10-31-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/fmt/mod.rs", function: None, start_line: 2394, start_col: Some(5), end_line: 2394, end_col: Some(51) }
warning: 1 warning emitted

error: /home/matthias/.kani/kani-0.40.0/bin/kani-compiler exited with status exit status: 101
```

This also aborts kani autoharness. Verified against main (de756c9): running kani autoharness -Z autoharness on this reproducer panics at kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs:697 with Function ... should've been declared before usage.

Worth knowing because the blast radius is bigger than the report suggests: with a manual harness this costs you one harness, but under autoharness a single function like this aborts the whole crate sweep, so nothing in the crate gets verified. Adding it to the Autoharness milestone for that reason.

Treat pointer and Box locals of function items as ordinary variables

Treat pointer and `Box` locals of function items as ordinary variables (

Navigation Menu

Repository navigation

ICE: `Function should've been declared before usage`, was: `Can't take address of Expr` #2255

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

ICE: Function should've been declared before usage, was: Can't take address of Expr #2255

Description

Activity

matthiaskrgr commented on Nov 12, 2023

feliperodri commented on Sep 25, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

ICE: `Function should've been declared before usage`, was: `Can't take address of Expr` #2255