Incorrect error message for method call on field access

[rayman2000]

The following program should return the error that acc(x.next) is missing

field next: Ref

predicate list(x: Ref){
    x != null ==> acc(x.next) && list(x.next)
}

method reverse(x: Ref)
requires list(x)
ensures list(x)


method test(x: Ref)
{
    reverse(x.next)
}

Carbon does this correctly. Silicon (for me) returns the error that acc(x.next.next) is missing (both the IDE and the master branch).
Strangely, if I reverify the file in the IDE (so with a cache I assume) the error message is correct, it only fails on the first verification attempt.

[rayman2000]

I think the problem is as follows:
When we execute a method call, we create a pve that will transform the formal args of the called method back to the actual args of the caller:

silicon/src/main/scala/rules/Executor.scala

Lines 530 to 531 in 5e3ab01

	val reasonTransformer = (n: viper.silver.verifier.errors.ErrorNode) => n.replace(formalsToActuals)
	val pveCall = CallFailed(call).withReasonNodeTransformed(reasonTransformer)

This is correct if the error is thrown while checking the preconditions of the method.
However, if the error occurs while evaluating the args in the caller context, then this transformation is nonsense, we should do no transformation then. This should only happen if the variable names are related in caller and callee. Indeed, if I rename one of the variables, the error does not occur.

[rayman2000]

So I think here we do not want the transformation:

silicon/src/main/scala/rules/Executor.scala

Line 537 in 5e3ab01

evals(s, eArgs, _ => pveCall, v)((s1, tArgs, v1) => {

But here we do:

silicon/src/main/scala/rules/Executor.scala

Line 555 in 5e3ab01

produces(s4, freshSnap, meth.posts, _ => pveCall, v2)((s5, v3) => {

[marcoeilers]

Thanks for looking into this!