search

viperproject / viperserver

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

Cannot find file #18

Closed ArquintL closed 4 years ago

ArquintL commented 4 years ago

Verification using Viperserver together with Silicon fails with the following error (unless --ignoreFile is provided):

msg=invalid_args_report(tool_signature=Silicon 1.1-SNAPSHOT (0964fff4+), errors=[Command-line interface: Cannot find file '_programID_failing_post.gobra' from 'file' argument. (<no position>)])

Quick fix: I add the --ignoreFile option to all my verification jobs. However, I think this option should automatically be set when verifying an AST instead of a Viper file

WissenIstNacht commented 4 years ago

Hey, thanks for reporting this issue.

I have addressed the problem in the latest commit. Please let me know if it persists, @ArquintL .

aterga commented 4 years ago

Thanks for addresssing the issue on such a short notice, @WissenIstNacht @ArquintL Please let us know if this fixed the problem with Gobra IDE.

ArquintL commented 4 years ago

Thanks a lot for this very fast fix!