search

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 103 forks source link

External specification for std::cmp::Ord crashing Prusti #1425

Closed nokunish closed 9 months ago

nokunish commented 12 months ago

Hi! I just noticed that providing 

#[extern_spec]
impl std::cmp::Ord for i32 {

    fn max(self, other: i32) -> i32;
    fn min(self, other: i32) -> i32;
}

crashes Prusti, and the only function for the std::cmp::Ord that does not crash is cmp(..).

Aurel300 commented 9 months ago

The reason for this is the same as discussed in #1436. Both max and min are methods provided by the Ord trait by default: there is no implementation of these methods by i32, so the extern spec is not "well-formed".