search

viperproject / prusti-dev

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

cannot generate fold-unfold Viper statements #1520

Open nishanthkarthik opened 3 months ago

nishanthkarthik commented 3 months ago 
fn external<'a, 'b>(t: &'a mut u32, r: &'a mut u32) -> &'b mut u32
where 'a: 'b {
    if *t == *r { t } else { r }
}

Details: cannot generate fold-unfold Viper statements. The required permission Pred(_1.val_ref, read) cannot be obtained

Prusti version: 0.2.2, commit 0d4a8d4 2024-03-26 13:08:03 UTC, built on 2024-03-26 13:20:57 UTC