Loop invariant might not hold, but there is none

[fpoli]

The following program generates a meaningless verification error, but as a workaround it is possible to wrap the mutable reference modification in a helper method. This is a bug. The original program should verify without raising a verification errors related to an inexistent loop invariant.

Unsupported:

fn client(i: &mut usize) {
    *i = 0;
    while *i < 10 {
        *i += 1; // <---
    }
}

Error message:

[Prusti: verification error] loop invariant might not hold after a loop iteration that preserves the loop condition.

Workaround:

fn client(i: &mut usize) {
    *i = 0;
    while *i < 10 {
        inc(i);
    }
}

fn inc(i: &mut usize) {
    *i += 1;
}

Workaround with contracts:

use prusti_contracts::*;

#[ensures(*i == 10)]
fn client(i: &mut usize) {
    *i = 0;
    while {
        body_invariant!(*i <= 10);
        *i < 10
    } {
        inc(i);
    }
}

#[requires(*i < 10)]
#[ensures(*i == old(*i) + 1)]
fn inc(i: &mut usize) {
    *i += 1;
}

Debugging details: It's because at the end of client we want to exhale the permission for the initial target of i, but the *i += 1 overwrites the field in our encoding with a new target. The _preserve variables in the encoding try to encode that the target remains constant, but it actually changes. By removing the _preserve hack Viper then complains that it doesn't have permission to exhale stuff at the end of client.