Skip to content

Commit

Permalink
Simplify documentation of TerminationDomainTransformer
Browse files Browse the repository at this point in the history
Co-authored-by: João Pereira <[email protected]>
  • Loading branch information
bruggerl and jcp19 committed Jul 10, 2024
1 parent aee8e53 commit da8ea86
Showing 1 changed file with 3 additions and 4 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -18,10 +18,9 @@ import viper.silver.reporter.{NoopReporter, Reporter}
import viper.silver.plugin.standard.predicateinstance.PredicateInstancePlugin
import viper.silver.verifier.AbstractError

// Maybe this class can be removed at some point because the functionality is in principle available in Viper itself.
// However, in Viper, at the moment the plugin transformations encapsulated in this class are done at a stage before
// Gobra starts interacting with the backend verifier, which is why we have to do them manually here and
// cannot remove the class yet.
// This class should be removed in the future because Viper already implements inference of
// imports for termination domains. However, at the moment, Viper performs the inference in
// `beforeVerify`, which is already too late.
class TerminationDomainTransformer extends ViperTransformer {

override def transform(task: BackendVerifier.Task): Either[Seq[AbstractError], BackendVerifier.Task] = {
Expand Down

0 comments on commit da8ea86

Please sign in to comment.