Incorrect error message for method call on field access
rayman2000 opened this issue · 3 comments
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.
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
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.
So I think here we do not want the transformation:
silicon/src/main/scala/rules/Executor.scala
Line 537 in 5e3ab01
But here we do:
silicon/src/main/scala/rules/Executor.scala
Line 555 in 5e3ab01