Incorrect error positions reported

[mschwerhoff]

For the program

method foo() {
  assert false
}

the assertion failure is reported as Assert might fail. Assertion false might not hold. ([email protected]). However line 2, columns 9-10 identify the whitespace between assert and false.

[mschwerhoff]

The problem affects the Viper IDE quite a bit, as illustrated by the screenshot below.

[ArquintL]

A similar issue arises when a precondition of a method does not hold. The error location even depends on whether the method has return parameters or not :

[mschwerhoff]

Further highlighting surprises (all method calls fail due to their precondition):

• difference between ending a line with a semicolon, and not
• difference between a method that returns a value, and doesn't

[fpoli]

@marcoeilers I vaguely remember that you might know the cause. If so, could you drop a hint?

[marcoeilers]

I don't. If I remember correctly, we basically implemented the code for storing parse positions ourselves when we moved to fastparse (the library didn't offer that feature), and then our code broke when we updated the fastparse version, and someone, presumably Fabio, had to fix it to get positions back at all.

The only detail I was involved with was this bit here: https://github.com/viperproject/silver/blob/8122ac2fff788b720f75056b16ce11dcb1316545/src/main/scala/viper/silver/parser/FastParser.scala#L40 That was a hack to get positions back for some specific cases that I put in to fix a test. It's definitely a hack though and shouldn't be necessary at all if the underlying problems were fixed. I could easily imagine that this hack also causes some weird results, like the one in the previous comment.