silver icon indicating copy to clipboard operation
silver copied to clipboard

Incorrect positions in Method AST nodes

Open aterga opened this issue 5 years ago • 0 comments

SilFrontend generates AST nodes with incorrect positions. In particular, the start position of methods is wrong (seems to be the same as their end position for some reason).

This is a critical bug because currently, the soundness of the caching mechanism in ViperServer (hence, also in Viper IDE and all of the frontend verifiers that use ViperServer) depends on the method position information.

To reproduce the problem, simply execute sbt testOnly *AstPositionsTests to run the test defined in src/test/scala/AstPositionsTests.scala.

aterga avatar Dec 25 '20 15:12 aterga