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

Plugin input with --plugin in customArguments does not work #165

Closed
totoyoyo opened this issue Aug 15, 2023 · 0 comments · Fixed by #186
Closed

Plugin input with --plugin in customArguments does not work #165

totoyoyo opened this issue Aug 15, 2023 · 0 comments · Fixed by #186

Comments

@totoyoyo
Copy link

totoyoyo commented Aug 15, 2023

Using the --plugin option in verificationBackends customArguments does not load the plugin. I looked into the code and there seems to be a ASTGenerator class that loads all the plugins prior to any verifier. However, this means the verifier args like --plugin are not considered, and only the default plugins in Silver are loaded.

For example:

"viperSettings.verificationBackends": [
        {
            "v": "674a514867b1",
            "name": "silicon",
            "type": "silicon",
            "paths": [],
            "engine": "ViperServer",
            "timeout": 100000,
            "stages": [
                {
                    "name": "verify",
                    "isVerification": true,
                    "mainMethod": "viper.silicon.SiliconRunner",
                    "customArguments": "--plugin someRandomPluginClass --z3Exe $z3Exe$ $disableCaching$ $fileToVerify$"
                }
            ],
            "stoppingTimeout": 5000
        }]

The argument provided to --plugin is ignored entirely. Even providing a non-existent class does not have an effect, and there are no error messages.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

1 participant