search

viperproject / viperserver

HTTP server that manages verification requests to different tools from the Viper tool stack.
Other
10 stars 17 forks source link

VerificationWorker should add option --ignoreFile before calling method prepare of SilFrontend #16

Closed aterga closed 4 years ago

aterga commented 4 years ago

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.

aterga commented 4 years ago

The fix has been confirmed by the Gobra IDE team.