Example that fails with more complete exhale

[fpoli]

The following program:

• does not verify in Prusti,
• verifies if the parameter b is commented out,
• alternatively, it verifies if PRUSTI_USE_MORE_COMPLETE_EXHALE is false.

use prusti_contracts::*;

const N : usize = 2;
const M : usize = 4;

#[requires(forall(|i:usize| i < N ==> (a[i] < M)))]
fn f(a : &[usize; N]
    , b: &[usize; N] // succeeds if this is commented
)
{
    let mut c: [usize; M] = [0; M];
    let mut i: usize = 0;
    while i < N {
        body_invariant!(i < N);
        body_invariant!(a[i] < M);
        let j = a[i];
        c[j] = 0;
        i = i + 1;
    }
}

fn main(){}

[alexanderjsummers]

Thanks! I suspect that we can generate a similar issue for Silicon just by setting up similar predicates at the Viper level. I assume this behaviour is not expected with the flag set.

[vakaras]

This looks like a well-known incompleteness in the more complete exhale.

[alexanderjsummers]

@vakaras ah thanks - is there an issue to link to?

[vakaras]

@vakaras ah thanks - is there an issue to link to?

https://github.com/viperproject/silicon/issues/387