len() bounds encoded only if there is a call in pure code

[fpoli]

trafficstars

The proper range bounds of <[T]>.len() seem to be encoded only if the len() call happens in pure code.

use prusti_contracts::*;

#[ensures(a.len() * 4 <= isize::MAX as usize)] // This verifies
fn good(a: &[i32], key: i32) {}

fn bad(a: &[i32], key: i32) {
  assert!(a.len() * 4 <= isize::MAX as usize); // This fails, but it should not
}

[fpoli]

Issue 1000! :tada: :tada: :tada:

[fpoli]

The following verifies. Mentioning a.len() in pure code seems enough to generate a more complete encoding:

use prusti_contracts::*;

#[ensures(a.len() * 4 <= isize::MAX as usize)] // This verifies
fn good(a: &[i32]) {}

#[requires(a.len() == 42 || dummy == 42)] // Mention `a.len()` in pure code
fn bad(a: &[i32], dummy: i32) {
  assert!(a.len() * 4 <= isize::MAX as usize); // This verifies
}