[ThomasMayerl]

Delegation edges have a problem as seen in the following example:

let mut x = 3;
let r_x = &mut x;
let p_x = r_x as *mut i32;
x = x + 1;
unsafe { *p_x = *p_x + 1 };

Here, the PCG will not drop the borrow r_x for the write to x, since a delegation edge with *r_x exists at this point, and we are still using *p_x (that the delegation edge is connected to) at a later point. Therefore, the PCG prints an error: PCG Assertion Failed : [main] No capability for x

However, we expect another error from Prusti: The write to x should be possible and drop the borrow r_x regardless. Therefore, Prusti will exhale the permission for r_x (and p_x) at that point, printing correctly an error in the last line that we do not have permission to access *p_x. Therefore, a delegation must generally stay alive as long as we use the raw pointer but it must forcefully be cut if we try to access a place that is lent out to another place that (nestedly) contains such a delegation. This PR fixes this issue by cutting the delegation edges appropriately.

Disclaimer: Claude Code was used to write the changes in this PR.

[JonasAlaif]

This might be fixed by #190 also, but if that doesn't get merged soon we can just rebase that PR on top of this one

[zgrannan]

Looks good to me!