Open
Description
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.