Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
aterga opened this issue Aug 27, 2020 · 1 comment
Assignees
Labels
bug Something isn't working

Comments

@aterga
Copy link
Member

aterga commented Aug 27, 2020

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 aterga added the bug Something isn't working label Aug 27, 2020
WissenIstNacht pushed a commit that referenced this issue Aug 27, 2020
WissenIstNacht pushed a commit that referenced this issue Sep 2, 2020
@aterga
Copy link
Member Author

aterga commented Sep 3, 2020

The fix has been confirmed by the Gobra IDE team.

@aterga aterga closed this as completed Sep 3, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

2 participants