Open rikosellic opened 1 month ago
I've encountered this issue as well. Constants from imported crates do not appear as the corresponding function definitions in the crate-lifetime.rs
file when logging is enabled, yet they are referenced in the function body of the callers.
// crate-lifetime.rs
...
fn main() {}
fn f31_main(
)
{
let x24_x: u32 = f25_ONE();
}
Verus does recognize constants defined in another verified crate in
spec
mode, but cannot recognize it as anexec
value. For example, suppose I define constantONE
in the library cratemylibrary/lib.rs
and compile it following the instructions in this Zulip conversation.Later when I want to use
ONE
as aspec
value in my main cratemymain/lib.rs
, everything works smoothly :But if I attempt to treat it as an
exec
value, like defining another constant:or using it as a return value:
verus will report an error indicating that it can not find a function:
It seems this problem is that the underlying representation of constants in
exec
mode is not passed between crates, is there a proper solution for this situation?