viperproject/viperserver

Cannot find file

ArquintL opened this issue · 3 comments

ArquintL commented

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

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

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

Thanks a lot for this very fast fix!