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

SilverPlugin mapVerificationResult #580

Open
dewert99 opened this issue May 20, 2022 · 0 comments
Open

SilverPlugin mapVerificationResult #580

dewert99 opened this issue May 20, 2022 · 0 comments

Comments

@dewert99
Copy link
Contributor

What is the best way for a plugin to override mapVerificationResult? I noticed that the termination and predicate instance plugins each apply the error-transformers to all errors of a specific type. This strategy doesn't stop these plugins from applying the transformers to errors from other plugins. Do we want to support a case where a plugin would want to attach a error-transformer to a Node, but then later decide not to apply that rewriting. If so, a plugin that does this would currently be incompatible with the termination and predicate instance plugins (at least if it used errors of the types those plugins look for), and other new plugins would need to be very carful to only apply error-transformers it created itself. If not, it might be worth having the plugin infrastructure automatically apply all the rewriters in order to simplify the SilverPlugin interface. The SilSuite already does this transformation which currently causes inconsistencies if a plugin doesn't implemented mapVerificationResult properly.

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

No branches or pull requests

1 participant