VerificationWorker should add option --ignoreFile before calling method prepare of SilFrontend
aterga opened this issue · 1 comments
Currently, the trailing option in the list of arguments must be an existing Viper file; otherwise, SilFrontend will complain while checking the command-line options. However, SilFrontend should not care about the existence of a file in the scenario of ViperServer as we already read the file, parsed it, and constructed a Viper AST based on it. Hence, we should tell it to ignore the checks that it normally performs over files. Fortunately, there's already an option for that, called --ignoreFile
.
We should add this option in the execute
method of ViperBackend. It should be the second-last element in the list, where the last element is programID
. This can be done using pattern matching over the structure of the list.
See https://github.com/viperproject/silver/blob/47ede88df9fb7f25092c8a7064b19468bf78b8bb/src/main/scala/viper/silver/frontend/SilFrontEndConfig.scala for more details.
The fix has been confirmed by the Gobra IDE team.