fpoli
commented
11 months ago Thank you for the bug report. The panic is due to an unreachable!() in find_impl_of_trait_method_call:
https://github.com/viperproject/prusti-dev/blob/863cd59705a43863eaba75c0dad1f4521de05aff/prusti-interface/src/environment/query.rs#L273-L320
In other words, Prusti fails to find the method that implements the declared #[pure] fn ge(..) -> ..;. I suspect that this is because #[extern_spec] is usually used to attach specifications to items defined in external crates, while the #[derive(PartialOrd)] is actually in the current crate (@Aurel300 is this correct?).
As a workaround, I'd try to define and use in the specifications a method like
impl Frame {
#[pure]
#[trusted]
#[ensures(result == (self.number >= other.number))] // i.e. the implementation of `#[derive(PartialOrd)]`
pub fn ge(&self, other: &Self) -> bool { *self >= *other }
}
Aurel300
Ramla-I
I'm trying to use the basic comparison operators for a type in my specifications, and following advice I found from other issues, I've marked the Ord and PartialOrd required methods as pure using the external spec feature. This still leads to a Prusti error:
[Prusti: invalid specification] use of impure function "std::cmp::PartialOrd::ge" in pure code is not allowedWhen I add the ge() method to my external spec and mark it as pure, I get an unexpected error. I'm wondering if I'm missing something when trying to use external spec for trait methods, or if this actually is an issue for now.
This is the code:
This is the Prusti assistant output when I try to set the ge() method as pure: