Skip to content

Fix missing caller substitution in apply_wands#176

Open
rgwohlbold wants to merge 3 commits into
Aurel300:rewrite-2023from
rgwohlbold:fix-missing-substitution-in-apply-wands
Open

Fix missing caller substitution in apply_wands#176
rgwohlbold wants to merge 3 commits into
Aurel300:rewrite-2023from
rgwohlbold:fix-missing-substitution-in-apply-wands

Conversation

@rgwohlbold
Copy link
Copy Markdown

@rgwohlbold rgwohlbold commented May 16, 2026

When applying a magic wand containing generic arguments, generic parameters were identity-substituted, leading to a "local variable not found in consistency check" error. Consider the following code snippet:

fn reborrow<U>(x: &mut U) -> &mut U {
    x
}

fn caller<T>(mut v: T) {
    let _ = reborrow(&mut v);
}

When the borrow expires, the following wand is applied in the caller:

  apply acc(p_Param(old[post1](p_Ref_mutable_snap(_2p, T$0)).s_Ref_mutable_0,
    U$0), write) --*
    acc(p_Param(old[pre0](p_Ref_mutable_snap(_3p, T$0)).s_Ref_mutable_0, U$0), write)

Notice the U$0 which has not been substituted.
This PR introduces caller substitution for apply_wand.
Running the doctests shows that this change eliminates this error category, see https://prusti-stdlib-support.rgwohlbold.de/.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant