viperproject / prusti-dev

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

Failing procedural macro of a contract #1480

Open fpoli opened 6 months ago

fpoli commented 6 months ago

The program

use prusti_contracts::*;

#[pure] // <-- ERROR
#[ensures="result > 0"]
fn len(r: i32) -> i32 {
  123
}

fails with

custom attribute panicked
message: internal error: entered unreachable code

However, the correct behaviour is to point out that the postcondition should be #[ensures(...)] instead of #[ensures="..."].