Insufficient access permission

[nokunish]

Hi! I was wondering why this causes an error?

#[ensures(x == old(x) + 10)]       // or old(x+ 10)
fn inc(mut x: usize) {
    while x < 10 {
        x += 1;
    }
}

this causes: Details: unhandled verification error: Assert might fail. There might be insufficient permission to access usize(_1) (@26.0) [assert.failed:insufficient.permission] AssertMethodPostcondition

However, if we do something similar but by borrowing instead,

#[ensures(result == old(x + 10))]
fn inc_borrow(x: usize) -> usize {

    let mut y = x;

    while y < 10 {
        y += 1;
    }

    y
}

it doesn't produce the same error.

[Aurel300]

We should report a better error for this, but the problem is with the specification. In the postcondition (in the first snippet), the expression x does not make sense, because x is not accessible at the callsite anymore. The fact that the argument is mut is not relevant for a caller, it is more like syntax sugar:

fn foo(mut x: usize) {
    // ...
}
// is the same as
fn foo(x: usize) {
    let mut x = x;
    // ...
}