You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: