While preparing a Prusti demo last week, I found that the order of the reported errors is a bit counter-intuitive. In the second function below, I'd expect the verification error in the second branch of the implementation to be reported before the verification error of a failing postcondition. Since Silicon only reports one error per function, the result is that verification errors jump around the code when working on it with Prusti. I don't think this was always the case. Was it perhaps the result of some Viper change?
use prusti_contracts::*;
#[ensures(false)]
fn good(b: bool) {
if b {
assert!(false); // <-- an error is reported here, as expected
} else {
assert!(true);
}
}
#[ensures(false)] // <-- an error is reported here
fn bad(b: bool) {
if b {
assert!(true);
} else {
assert!(false); // <-- the expected error is this one
}
}
While preparing a Prusti demo last week, I found that the order of the reported errors is a bit counter-intuitive. In the second function below, I'd expect the verification error in the second branch of the implementation to be reported before the verification error of a failing postcondition. Since Silicon only reports one error per function, the result is that verification errors jump around the code when working on it with Prusti. I don't think this was always the case. Was it perhaps the result of some Viper change?