Panic cause by incorrect trusted pure functions

Prusti panics on the following program instead of reporting an error.

use prusti_contracts::*;

#[pure]
#[trusted]
fn test1(x: String) {} // Expected error: argument must be Copy

fn main() {}

thread 'rustc' panicked at 'Local body of `DefId(0:5 ~ 20230130_114818[4d5e]::test1)` was not loaded!', prusti-interface/src/environment/body.rs:61:35
stack backtrace:
   0: rust_begin_unwind
             at /rustc/afaf3e07aaa7ca9873bdb439caec53faffa4230c/library/std/src/panicking.rs:575:5
   1: core::panicking::panic_fmt
             at /rustc/afaf3e07aaa7ca9873bdb439caec53faffa4230c/library/core/src/panicking.rs:64:14
   2: prusti_interface::environment::body::PreLoadedBodies::expect::{{closure}}
   3: core::option::Option<T>::unwrap_or_else
   4: prusti_interface::environment::body::PreLoadedBodies::expect
   5: prusti_interface::environment::body::EnvBody::get_pure_fn_body
   6: <prusti_viper::encoder::encoder::Encoder as prusti_viper::encoder::mir::pure::pure_functions::interface::PureFunctionEncoderInterface>::encode_pure_function_def
   7: prusti_viper::encoder::encoder::Encoder::process_encoding_queue
   8: prusti_viper::verifier::Verifier::verify
   9: prusti_driver::verifier::verify
  10: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis::{{closure}}
  11: rustc_interface::passes::QueryContext::enter::{{closure}}
  12: rustc_middle::ty::context::tls::enter_context::{{closure}}
  13: rustc_middle::ty::context::tls::set_tlv
  14: rustc_interface::passes::QueryContext::enter
  15: rustc_interface::queries::QueryResult<rustc_interface::passes::QueryContext>::enter
  16: <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver::Callbacks>::after_analysis
  17: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
  18: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
  19: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>

The bug is in this error handling branch, which tries to load the MIR body even when encoding bodyless functions: https://github.com/viperproject/prusti-dev/blob/17b071c41c1b502d739ccf414a2445a1bad8a3f6/prusti-viper/src/encoder/mir/pure/pure_functions/interface.rs#L379-L382

viperproject / prusti-dev

Panic cause by incorrect trusted pure functions #1301