From da8ea865a1b1b90e31b95d849637f6ee4da13c0c Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger <44122567+bruggerl@users.noreply.github.com> Date: Wed, 10 Jul 2024 14:24:31 +0200 Subject: [PATCH] Simplify documentation of TerminationDomainTransformer MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: João Pereira --- .../transformers/TerminationDomainTransformer.scala | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala b/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala index 479f289f3..c4fa13e08 100644 --- a/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala +++ b/src/main/scala/viper/gobra/translator/transformers/TerminationDomainTransformer.scala @@ -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] = {