-
Notifications
You must be signed in to change notification settings - Fork 5
FunId undefined: 0x0::vector_iter::range #517
Copy link
Copy link
Closed
Description
public fun f(x: u8): u8 { x }
#[spec(prove)]
public fun f_spec(x: u8): u8 {
f(x)
}
Running sui-prover gives
thread 'main' (50085) panicked at crates/move-model/src/model.rs:4432:53:
FunId undefined: 0x0::vector_iter::range
and a backtrace
stack backtrace:
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
2: core::option::expect_failed
3: move_model::model::ModuleEnv::into_function
4: move_model::model::GlobalEnv::get_function_qid
5: move_prover_boogie_backend::boogie_backend::lib::add_prelude
6: move_prover_boogie_backend::generator::generate_boogie
7: move_prover_boogie_backend::generator::generate_function_bpl
8: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
9: core::iter::adapters::try_process
10: sui_prover::prove::execute_backend_boogie::{{closure}}
11: tokio::runtime::park::CachedParkThread::block_on
12: tokio::runtime::context::runtime::enter_runtime
13: tokio::runtime::runtime::Runtime::block_on
14: sui_prover::main
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels