From 020506faf6bdbdb7b390b02777a4eccad0cc8846 Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Wed, 18 Feb 2026 12:35:52 +0100
Subject: [PATCH 01/12] First push. Lots of dead code and commented out code

---
 carbon                                        |  2 +-
 silicon                                       |  2 +-
 .../frontends/lsp/ClientCoordinator.scala     | 16 ++++-
 .../viper/server/frontends/lsp/Common.scala   |  3 +
 .../server/frontends/lsp/DataProtocol.scala   | 36 ++++++++++-
 .../viper/server/frontends/lsp/Receiver.scala | 61 ++++++++++++++++++-
 .../server/frontends/lsp/file/Manager.scala   | 45 +++++++++++++-
 .../frontends/lsp/file/ProjectManager.scala   |  2 +
 .../frontends/lsp/file/Verification.scala     | 54 ++++++++++++++--
 .../lsp/file/utility/Containers.scala         | 31 ++++++++++
 .../lsp/file/utility/Conversions.scala        | 22 ++++++-
 11 files changed, 259 insertions(+), 15 deletions(-)

diff --git a/carbon b/carbon
index 7c5c1df4..0a62400e 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 7c5c1df49844ce2cd27d42d4d95859bbc3ad0142
+Subproject commit 0a62400e7140ef0570306be4ffd80dc1f7636fe7
diff --git a/silicon b/silicon
index bcef73bb..bc190326 160000
--- a/silicon
+++ b/silicon
@@ -1 +1 @@
-Subproject commit bcef73bb48e4158b7c1c55c5db8eb1060a50c664
+Subproject commit bc19032696f2da1307710e5f47e033a6410057c1
diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index b3d59ad8..8a2c5bb3 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -7,7 +7,7 @@
 package viper.server.frontends.lsp
 
 import ch.qos.logback.classic.Logger
-import org.eclipse.lsp4j.Range
+import org.eclipse.lsp4j.{Range, Diagnostic}
 import viper.server.core.VerificationExecutionContext
 
 import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
@@ -16,6 +16,7 @@ import scala.jdk.CollectionConverters._
 import scala.jdk.FutureConverters._
 import viper.server.frontends.lsp.file.FileManager
 import viper.server.frontends.lsp.file.VerificationManager
+import viper.silicon.interfaces.SiliconAbductionFailureContext
 
 /** Manages per-client state and interacts with the server instance (which is shared among all clients).
  *  It owns one `FileManager` per open file, the two main components of a file
@@ -62,6 +63,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   private def getFile(uri: String): Option[FileManager] = Option(_files.get(uri))
   private var _vprFileEndings: Option[Array[String]] = None
   private var _previousFile: Option[String] = None
+  private var inferenceResultsCache: Map[Diagnostic, Seq[viper.silicon.biabduction.InferenceResult]] = Map.empty
 
   def client: Option[IdeLanguageClient] = {
     _client
@@ -195,6 +197,18 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     }
   }
 
+  def updateInferenceResults(diag: Diagnostic, fix: Seq[viper.silicon.biabduction.InferenceResult]): Unit = {
+    try{
+      inferenceResultsCache += (diag -> fix)
+    } catch {
+      case e: Throwable => logger.debug(s"Error while updating inference results: $e")
+    }
+  }
+
+  def getInferenceResults(diag: Diagnostic): Seq[viper.silicon.biabduction.InferenceResult] = {
+    inferenceResultsCache.getOrElse(diag, Seq.empty)
+  }
+
   /** Notifies the client about a state change
     *
     * If state change is related to a particular file, its manager's state is also updated.
diff --git a/src/main/scala/viper/server/frontends/lsp/Common.scala b/src/main/scala/viper/server/frontends/lsp/Common.scala
index e576bef0..18705d36 100644
--- a/src/main/scala/viper/server/frontends/lsp/Common.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Common.scala
@@ -39,6 +39,9 @@ object Common {
   }
   def toLocation(sp: ast.AbstractSourcePosition): Location =
     new Location(sp.file.toUri().toString(), toRange(sp))
+  def toHasLineColumn(pos: Position): ast.HasLineColumn = {
+    new ast.LineColumnPosition(pos.getLine + 1, pos.getCharacter + 1)
+  }
 
   def comparePosition(a: Position, b: Position): Int = {
     if (a == null && b == null) return 0
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index cd3c3850..4e875877 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -81,11 +81,13 @@ case class BackendProperties(
 
 case class VerifyParams (
               uri: String,                  // file to verify
-              content: String,             // contents of file to verify
+              content: String,              // contents of file to verify
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
-              customArgs: String)            // contains the path of the file that should be verified
+              customArgs: String,           // contains the path of the file that should be verified
+              enableInference: Boolean)     // determines whether inference should be performed on verification error
+
 
 case class ReformatParams (uri: String)
 
@@ -176,7 +178,35 @@ case class StateChangeParams(
               verificationNeeded: Double = -1,
               uri: String = null,
               stage: String = null,
-              error: String = null)
+              error: String = null,
+              inferenceResults: InferenceResultsParams = null)
+
+/**
+ * Result of specification inference for a single line in a file.
+ * @param line The line number the result refers to.
+ * @param action The action to be performed (add = 0, remove = 1, edit = 2).
+ *  - Add: The inferred specification should be added.
+ *  - Remove: The inferred specification should be removed.
+ *  - Edit: The inferred specification should replace an existing one.
+ * @param content The content of the inferred specification.
+ */
+case class InferenceResult (
+              line: Int,
+              action: Int,
+              content: String)
+
+
+/**
+ * Contains results of specification inference for a file. Sent from the server to the client after inference is
+ * complete.
+ * @param uri The URI of the file the inference results refer to.
+ * @param results The list of [[InferenceResult inference results]] for the file.
+ * @param success Whether the inference process was successful.
+ */
+case class InferenceResultsParams (
+              uri: String,
+              results: Array[InferenceResult],
+              success: Boolean)
 
 case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int)
 
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 4d4fdbe6..4907fd93 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -20,6 +20,17 @@ import scala.concurrent.duration.DurationInt
 import scala.jdk.CollectionConverters._
 import scala.jdk.FutureConverters._
 import scala.language.postfixOps
+import akka.actor.{Actor, PoisonPill, Props, Status}
+import viper.server.frontends.lsp
+import viper.server.frontends.lsp.VerificationState._
+import viper.server.frontends.lsp.VerificationSuccess._
+import viper.silver.ast
+import viper.silver.reporter._
+import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage}
+import viper.server.frontends.lsp.file.ProgressCoordinator
+import viper.silver.parser._
+import viper.silicon.Config.InferenceMode.OnError
+import viper.silicon.verifier.Verifier
 
 trait StandardReceiver {
   val coordinator: ClientCoordinator
@@ -314,8 +325,45 @@ trait TextDocumentReceiver extends StandardReceiver with TextDocumentService {
   }
 
   override def codeAction(params: CodeActionParams) = {
-    // TODO
-    CompletableFuture.completedFuture(Nil.asJava)
+    coordinator.logger.info(s"[Req: textDocument/codeAction] ${params.toString()}")
+    val uri = params.getTextDocument.getUri
+    val ctxt = params.getContext
+    var diags = Seq.empty[Diagnostic]
+    ctxt.getDiagnostics.asScala.foreach(diag => diags = diags :+ diag)
+    //ctxt.getDiagnostics.asScala.map(diag => coordinator.getRoot(uri).getCodeAction(uri, diag).map(cact => (cact.map(icact => Either.forRight[Command, CodeAction](icact))).asJava)).asJava
+    coordinator.getRoot(uri).getCodeAction(uri, diags).map(cacts => cacts.map(cact => Either.forRight[Command, CodeAction](cact)).asJava).asJava.toCompletableFuture
+    /*
+    var res = Seq[Either[Command, CodeAction]]()
+    ctxt.getDiagnostics.asScala.foreach(diag =>
+      coordinator.getRoot(uri).getCodeAction(uri, diag).foreach(cact => {
+        coordinator.logger.info(s"[CACT:] ${cact.toString()}")
+        coordinator.logger.info(s"[RESPRE:] ${res.toString()}")
+        res = res :+ Either.forRight[Command, CodeAction](cact)
+        coordinator.logger.info(s"[RESPOST:] ${res.toString()}")
+      }))
+    //coordinator.logger.info(s"[Infer specifications on error] ${Verifier.config.inferenceMode() == OnError}")
+    //ctxt.getDiagnostics.asScala.foreach(diag => res = res +: Either.forRight[Command, CodeAction]())
+*/
+    /*
+      ctxt.getDiagnostics.asScala.foreach(diag =>
+        coordinator.getInferenceResults(diag).foreach(infres => {
+          val irca = new CodeAction(infres.getEdit)
+          val editmap: Map[String, java.util.List[TextEdit]] = Map(uri -> Seq(new TextEdit(
+            new Range(
+              new Position(infres.start.line - 1, infres.start.column - 1),
+              new Position(infres.end.line - 1, infres.end.column - 1)
+            ), infres.newText)).asJava)
+          irca.setKind(CodeActionKind.QuickFix)
+          irca.setEdit(new WorkspaceEdit(editmap.asJava))
+          irca.setDiagnostics(Seq(diag).asJava)
+          //irca.setCommand(new Command("Verify after specification inference", "viper.verify"))
+          res = res :+ Either.forRight[Command, CodeAction](irca)
+          coordinator.logger.info(s"[Res: textDocument/codeAction] ${irca.toString()}")
+        }))
+      coordinator.logger.info(s"[Info: textDocument/codeAction] ${res.toString()}")
+  */
+
+    //CompletableFuture.completedFuture(res.asJava)
   }
 
   override def formatting(params: DocumentFormattingParams) = {
@@ -410,7 +458,16 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
 
   @JsonNotification(C2S_Commands.Verify)
   def onVerify(data: VerifyParams): Unit = {
+    //DEBUG-------------------------------------------------------------------------
+    /*
+    if(data.enableInference){
+      coordinator.client.get.notifyStateChanged(lsp.StateChangeParams(6, 50, 4, 1, 0, "TEST", "carbon", 42, 0, data.uri, "TESTSTAGE", "TESTERROR", lsp.InferenceResultsParams(data.uri, Array(lsp.InferenceResult(1, 0, "TESTCODE")), true)))
+      return
+    }
+    */
+    //DEBUG-------------------------------------------------------------------------
     coordinator.logger.debug("On verifying")
+    //coordinator.updateInferenceResults(data.uri, Seq.empty)
     if (coordinator.canVerificationBeStarted(data.uri, data.content, data.manuallyTriggered)) {
       // stop all other verifications because the backend crashes if multiple verifications are run in parallel
       coordinator.logger.trace("verification can be started - all running verifications are now going to be stopped")
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
index bf017d40..71f0a486 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
@@ -14,16 +14,30 @@ import scala.jdk.CollectionConverters._
 import scala.collection.mutable.ArrayBuffer
 import viper.server.frontends.lsp.file.FileContent
 import viper.server.frontends.lsp.Lsp4jSemanticHighlight
-
 import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.Common
+import viper.silicon.biabduction.InferenceResult
 
 case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends lsp.HasRangePositions with lsp.BelongsToFile {
   override def rangePositions: Seq[lsp.RangePosition] = Seq(position)
   override def file: Path = position.file
 }
 
+case class CodeAction(backendClassName: Option[String],
+                      title: String,
+                      kind: String,
+                      diags: Seq[Diagnostic],
+                      command: Option[(String, String)],
+                      edit: Option[Seq[InferenceResult]],
+                      diagkey: Option[lsp4j.Diagnostic],
+                      fileinfo: PathInfo
+                     ) extends lsp.HasRangePositions with lsp.BelongsToFile with utility.HasKey[lsp4j.Diagnostic] {
+  override def rangePositions: Seq[lsp.RangePosition] = diags.map(_.position)
+  override def file: Path = fileinfo.path
+  override val key: lsp4j.Diagnostic = diagkey.orNull
+}
+
 trait Manager {
   val file: PathInfo
   val content: FileContent
@@ -33,6 +47,12 @@ trait Manager {
   def addContainer(c: utility.LspContainer[_, _, _, _, _]): Unit
   def resetContainers(first: Boolean): Unit
 
+  //def toLspCommand(title: String, command: String, args: Option[Seq[AnyRef]]): lsp4j.Command
+  //def toLspWorkspaceEdit(edits: Seq[viper.silicon.biabduction.InferenceResult]): lsp4j.WorkspaceEdit
+
+  def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction]
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit
+
   def getCodeLens(): Seq[lsp4j.CodeLens]
   def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit
 
@@ -71,6 +91,7 @@ trait Manager {
 }
 
 /** Stores and handles all aspects relating the the lsp features:
+ *  - CodeAction
  *  - CodeLens
  *  - Diagnostic
  *  - DocumentSymbol
@@ -103,6 +124,28 @@ trait StandardManager extends Manager {
   }
 
 
+
+  //def toLspWorkspaceEdit(edits: Seq[viper.silicon.biabduction.InferenceResult]): lsp4j.WorkspaceEdit = {
+  //  new lsp4j.WorkspaceEdit((Map(file.file_uri -> edits.map(edit => new lsp4j.TextEdit(new lsp4j.Range(Common.toPosition(edit.start), Common.toPosition(edit.end)), edit.newText)).asJava)).asJava)
+  //}
+
+  // CodeAction
+  type CodeActionContainer = utility.StageMapContainer.MapContainer[CodeAction, lsp4j.Diagnostic, lsp4j.CodeAction]
+  val codeActionContainer: CodeActionContainer = utility.LspContainer(utility.CodeActionTranslator, () => {})
+  private def initCodeActionKey(codeAction: CodeAction): Seq[CodeAction] = {
+    var cas: Seq[CodeAction] = Seq.empty
+    codeAction.diags.foreach(diag => {
+      cas = cas :+ new CodeAction(codeAction.backendClassName, codeAction.title, codeAction.kind, Seq(diag), codeAction.command, codeAction.edit, Some(diagnosticContainer.translator.translate(diag)()), codeAction.fileinfo)
+    })
+    //codeAction.key = diagnosticContainer.translator.translate(codeAction.diag)()
+    cas
+  }
+  containers.addOne(codeActionContainer)
+
+  //def getCodeAction() = codeActionContainer.get(())
+  def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] = codeActionContainer.get(diag)//CodeAction.fromDiag.getOrElse(diag, Seq.empty).map(cact => utility.CodeActionTranslator.translate(cact)())
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = add(codeActionContainer, first, vs.map(v => initCodeActionKey(v)).flatten)//vs.map(v => v.addToMap()))
+
   // CodeLens
   type CodeLensContainer = utility.StageArrayContainer.ArrayContainer[lsp.CodeLens, lsp4j.CodeLens]
   val codeLensContainer: CodeLensContainer = utility.LspContainer(utility.CodeLensTranslator, if (coordinator.client.isDefined) coordinator.client.get.refreshCodeLenses else () => {})
diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
index 18d9fc90..d9f7482e 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
@@ -236,6 +236,8 @@ trait ProjectManager extends ProjectAware {
     }
   }
 
+  def getCodeAction(uri: String, diags: Seq[lsp4j.Diagnostic]): Future[Seq[lsp4j.CodeAction]] =
+    Future.successful(diags.map(diag => getInProject(uri).getCodeAction(diag)).flatten)
   // Can force a refresh in the future if we get new ones, so return immediately
   def getCodeLens(uri: String): Future[Seq[lsp4j.CodeLens]] =
     Future.successful(getInProject(uri).getCodeLens())
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index bd83ee61..930c187a 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -8,23 +8,30 @@ package viper.server.frontends.lsp.file
 
 import ch.qos.logback.classic.Logger
 import viper.server.frontends.lsp
+
 import scala.concurrent.Future
+import scala.jdk.CollectionConverters._
 import viper.server.core.ViperBackendConfig
 import viper.server.vsi.{AstJobId, VerJobId}
+
 import scala.concurrent.ExecutionContext
 import akka.actor.Props
-
 import viper.server.frontends.lsp.VerificationSuccess._
 import viper.server.frontends.lsp.VerificationState._
-
 import viper.silver.verifier.AbstractError
+
 import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
 import org.eclipse.lsp4j
+import viper.server.frontends.lsp.Common
 import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
+import viper.silicon.interfaces._
+import viper.silver.verifier._
+import viper.silicon.Config.InferenceMode.OnError
+import viper.silicon.verifier.Verifier
 
 case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) {
   private var waitingOn: Option[Either[AstJobId, VerJobId]] = None
@@ -265,6 +272,7 @@ trait VerificationManager extends ManagesLeaf {
   def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = {
     val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("")
     val files = HashSet[String]()
+    var cas: Seq[CodeAction] = Seq.empty
 
     val diags = errors.map(err => {
       coordinator.logger.info(s"Handling error ${err.toString()}")
@@ -306,19 +314,55 @@ trait VerificationManager extends ManagesLeaf {
       }
       files.add(rp.file.toUri().toString())
 
-      val errFullId = if(err.fullId != null) s"[${err.fullId}] " else ""
+      val errFullId = if (err.fullId != null) s"[${err.fullId}] " else ""
       val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else ""
       coordinator.logger.debug(s"$errorType:$backendString $errFullId" +
         s"${range.getStart.getLine + 1}:${range.getStart.getCharacter + 1} $errMsgPrefixWithWhitespace${err.readableMessage}s")
 
-      val cachFlag: String = if(err.cached) " (cached)" else ""
+      val cachFlag: String = if (err.cached) " (cached)" else ""
       val message = s"$errMsgPrefixWithWhitespace${err.readableMessage}$cachFlag"
-      (phase, Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix))
+      val diagnostic = Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix)
+      coordinator.logger.info(s"[ERRORTYPE] ${errorType}")
+      coordinator.logger.info(s"[TAKE BRANCH?] ${errorType == "Verification error"}")
+      if (errorType == "Verification error"){
+        coordinator.logger.info(s"[BRANCH TAKEN WITH ERROR:] ${err.toString()}")
+        err match {
+        case g: VerificationError =>
+          g.failureContexts.foreach { h =>
+            h match {
+              case h1: SiliconAbductionFailureContext =>
+                h1.fix match {
+                  case Some(irs) =>
+                    if (Verifier.config.inferenceMode() == OnError) {
+                      //coordinator.updateInferenceResults(lspdiag, irs)
+                      //val edits = new lsp4j.WorkspaceEdit((Map(file.file_uri -> irs.map(edit => new lsp4j.TextEdit(new lsp4j.Range(Common.toPosition(edit.start), Common.toPosition(edit.end)), edit.newText)).asJava)).asJava)
+                      //irs.foreach(ir => {cas = cas :+ CodeAction(backendClassName, ir.getEdit, "quickfix", Seq(diagnostic), None, Some(edits), None, this.file)
+                      cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
+                      //coordinator.logger.info(s"[CAS] ${cas.toString()}")})
+                      coordinator.logger.info(s"[IR] ${irs.toString()}")
+                      //coordinator.logger.info(s"[EDITS] ${edits.toString()}")
+                    }
+                  case None =>
+                    coordinator.logger.info(s"[IR] ${Seq.empty.toString()}")
+                }
+              case _ =>
+                coordinator.logger.info("NOT ABDUCTION FAILURE")
+            }
+          }
+          coordinator.logger.info(s"[ERROR CONTEXTS:] ${g.failureContexts.toString()}")
+        case _ =>
+          coordinator.logger.info("NOT VERIFICATION ERROR")
+      }
+      }
+      (phase, diagnostic)
     })
     diagnosticCount += errors.size
     errorCount += diags.count(_._2.severity == lsp4j.DiagnosticSeverity.Error)
     diags.groupBy(d => d._1).foreach { case (phase, diags) =>
       this.addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2))
     }
+    this.root.addCodeAction(true)(cas)
+    coordinator.logger.info(s"CODE ACTIONS: ${cas.toString()}")
+    //coordinator.logger.info(s"THIS ROOT CODE ACTIONS: ${this.root.getCodeAction.toString()}")
   }
 }
diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala
index d37028f7..d6ac3b30 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala
@@ -17,6 +17,10 @@ import viper.silver.ast.utility.lsp
 import viper.silver.ast.utility.lsp.SelectionBoundScopeTrait
 import viper.silver.ast.utility.lsp.SelectionBoundKeywordTrait
 
+trait HasKey[K] {
+  val key: K
+}
+
 trait StageContainer[K, V, I] {
   var resetCount: Int = 0
   def reset(): Unit = {
@@ -54,6 +58,33 @@ object StageArrayContainer {
   implicit def default[V]: () => StageArrayContainer[V] = () => StageArrayContainer()
 }
 
+case class StageMapContainer[K, V <: HasKey[K]]() extends StageContainer[K, V, K]{
+  private val map: HashMap[K, Seq[V]] = HashMap()
+
+  override protected def innerReset(): Unit = map.clear()
+  override protected def innerAdd(v: V): K = {
+    map.put(v.key, map.getOrElse(v.key, Seq.empty) :+ v)
+    v.key
+  }
+  override def get(k: K): Seq[V] = {
+    map.getOrElse(k, Seq.empty)
+  }
+  override protected def innerUpdate(i: K, f: V => V): Boolean = {
+    if (!map.contains(i)) {
+      false
+    } else {
+      map.put(i, map(i).map(v => f(v)))
+      true
+    }
+  }
+  override def all(): Iterator[V] = map.values.flatten.iterator
+  override def filterInPlace(p: V => Boolean): Unit = map.values.map(vs => vs.filter(p))
+}
+object StageMapContainer {
+  type MapContainer[V <: HasRangePositions with BelongsToFile with HasKey[K], K, U] = LspContainer[StageMapContainer[K, V], K, V, K, U]
+  implicit def default[K, V <: HasKey[K]]: () => StageMapContainer[K, V] = () => StageMapContainer()
+}
+
 case class StageRangeContainer[V <: SelectableInBound]() extends StageContainer[(Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean), V, (Option[String], Int)] {
   // Has a `scope` bound
   val localKeyword: HashMap[String, ArrayBuffer[V]] = HashMap()
diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
index ece3667b..3c920ba0 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
@@ -10,8 +10,10 @@ import org.eclipse.lsp4j
 import org.eclipse.lsp4j.jsonrpc.messages.Either
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.{Common, Lsp4jSemanticHighlight}
-import viper.server.frontends.lsp.file.{Diagnostic, FindReferences}
+import viper.server.frontends.lsp.file.{CodeAction, Diagnostic, FindReferences}
 import ch.qos.logback.classic.Logger
+import org.eclipse.lsp4j.Command
+import org.eclipse.lsp4j.WorkspaceEdit
 
 import scala.jdk.CollectionConverters._
 import scala.collection.mutable.ArrayBuffer
@@ -21,6 +23,24 @@ trait Translates[-T, +U, I] {
   def translate(t: Seq[T])(i: I)(implicit @annotation.unused log: Logger): Seq[U] = t.map(translate(_)(i))
 }
 
+case object CodeActionTranslator extends Translates[CodeAction, lsp4j.CodeAction, lsp4j.Diagnostic] {
+  override def translate(cact: CodeAction)(i: lsp4j.Diagnostic): lsp4j.CodeAction = {
+    val lspca = new lsp4j.CodeAction(cact.title)
+    lspca.setKind(cact.kind)
+    lspca.setDiagnostics(Seq(cact.key).asJava)
+    lspca.setEdit(
+      cact.edit match {
+        case Some(e) => new WorkspaceEdit((Map(cact.fileinfo.file_uri -> e.map(edit => new lsp4j.TextEdit(new lsp4j.Range(Common.toPosition(edit.start), Common.toPosition(edit.end)), edit.newText)).asJava)).asJava)
+        case None => null
+      })
+    lspca.setCommand(cact.command match {
+      case Some(e) => new Command(e._1, e._2)
+      case None => null
+    })
+    lspca
+  }
+}
+
 case object CodeLensTranslator extends Translates[lsp.CodeLens, lsp4j.CodeLens, Unit] {
   override def translate(lens: lsp.CodeLens)(i: Unit): lsp4j.CodeLens = {
     val range = Common.toRange(lens.range)

From 3703c3b2f4e2c2434cca42221240f883ab6ad953 Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Thu, 26 Feb 2026 15:49:39 +0100
Subject: [PATCH 02/12] Code cleanup

---
 .../frontends/lsp/ClientCoordinator.scala     | 16 +------
 .../viper/server/frontends/lsp/Common.scala   |  3 --
 .../server/frontends/lsp/DataProtocol.scala   | 30 +-----------
 .../viper/server/frontends/lsp/Receiver.scala | 46 +-----------------
 .../server/frontends/lsp/file/Manager.scala   | 14 +-----
 .../frontends/lsp/file/Verification.scala     | 48 +++++++------------
 6 files changed, 21 insertions(+), 136 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index 8a2c5bb3..b3d59ad8 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -7,7 +7,7 @@
 package viper.server.frontends.lsp
 
 import ch.qos.logback.classic.Logger
-import org.eclipse.lsp4j.{Range, Diagnostic}
+import org.eclipse.lsp4j.Range
 import viper.server.core.VerificationExecutionContext
 
 import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
@@ -16,7 +16,6 @@ import scala.jdk.CollectionConverters._
 import scala.jdk.FutureConverters._
 import viper.server.frontends.lsp.file.FileManager
 import viper.server.frontends.lsp.file.VerificationManager
-import viper.silicon.interfaces.SiliconAbductionFailureContext
 
 /** Manages per-client state and interacts with the server instance (which is shared among all clients).
  *  It owns one `FileManager` per open file, the two main components of a file
@@ -63,7 +62,6 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   private def getFile(uri: String): Option[FileManager] = Option(_files.get(uri))
   private var _vprFileEndings: Option[Array[String]] = None
   private var _previousFile: Option[String] = None
-  private var inferenceResultsCache: Map[Diagnostic, Seq[viper.silicon.biabduction.InferenceResult]] = Map.empty
 
   def client: Option[IdeLanguageClient] = {
     _client
@@ -197,18 +195,6 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     }
   }
 
-  def updateInferenceResults(diag: Diagnostic, fix: Seq[viper.silicon.biabduction.InferenceResult]): Unit = {
-    try{
-      inferenceResultsCache += (diag -> fix)
-    } catch {
-      case e: Throwable => logger.debug(s"Error while updating inference results: $e")
-    }
-  }
-
-  def getInferenceResults(diag: Diagnostic): Seq[viper.silicon.biabduction.InferenceResult] = {
-    inferenceResultsCache.getOrElse(diag, Seq.empty)
-  }
-
   /** Notifies the client about a state change
     *
     * If state change is related to a particular file, its manager's state is also updated.
diff --git a/src/main/scala/viper/server/frontends/lsp/Common.scala b/src/main/scala/viper/server/frontends/lsp/Common.scala
index 18705d36..e576bef0 100644
--- a/src/main/scala/viper/server/frontends/lsp/Common.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Common.scala
@@ -39,9 +39,6 @@ object Common {
   }
   def toLocation(sp: ast.AbstractSourcePosition): Location =
     new Location(sp.file.toUri().toString(), toRange(sp))
-  def toHasLineColumn(pos: Position): ast.HasLineColumn = {
-    new ast.LineColumnPosition(pos.getLine + 1, pos.getCharacter + 1)
-  }
 
   def comparePosition(a: Position, b: Position): Int = {
     if (a == null && b == null) return 0
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index 4e875877..32795722 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -178,35 +178,7 @@ case class StateChangeParams(
               verificationNeeded: Double = -1,
               uri: String = null,
               stage: String = null,
-              error: String = null,
-              inferenceResults: InferenceResultsParams = null)
-
-/**
- * Result of specification inference for a single line in a file.
- * @param line The line number the result refers to.
- * @param action The action to be performed (add = 0, remove = 1, edit = 2).
- *  - Add: The inferred specification should be added.
- *  - Remove: The inferred specification should be removed.
- *  - Edit: The inferred specification should replace an existing one.
- * @param content The content of the inferred specification.
- */
-case class InferenceResult (
-              line: Int,
-              action: Int,
-              content: String)
-
-
-/**
- * Contains results of specification inference for a file. Sent from the server to the client after inference is
- * complete.
- * @param uri The URI of the file the inference results refer to.
- * @param results The list of [[InferenceResult inference results]] for the file.
- * @param success Whether the inference process was successful.
- */
-case class InferenceResultsParams (
-              uri: String,
-              results: Array[InferenceResult],
-              success: Boolean)
+              error: String = null)
 
 case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int)
 
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 4907fd93..cdb92a08 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -20,17 +20,6 @@ import scala.concurrent.duration.DurationInt
 import scala.jdk.CollectionConverters._
 import scala.jdk.FutureConverters._
 import scala.language.postfixOps
-import akka.actor.{Actor, PoisonPill, Props, Status}
-import viper.server.frontends.lsp
-import viper.server.frontends.lsp.VerificationState._
-import viper.server.frontends.lsp.VerificationSuccess._
-import viper.silver.ast
-import viper.silver.reporter._
-import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage}
-import viper.server.frontends.lsp.file.ProgressCoordinator
-import viper.silver.parser._
-import viper.silicon.Config.InferenceMode.OnError
-import viper.silicon.verifier.Verifier
 
 trait StandardReceiver {
   val coordinator: ClientCoordinator
@@ -325,45 +314,12 @@ trait TextDocumentReceiver extends StandardReceiver with TextDocumentService {
   }
 
   override def codeAction(params: CodeActionParams) = {
-    coordinator.logger.info(s"[Req: textDocument/codeAction] ${params.toString()}")
+    coordinator.logger.trace(s"[Req: textDocument/codeAction] ${params.toString()}")
     val uri = params.getTextDocument.getUri
     val ctxt = params.getContext
     var diags = Seq.empty[Diagnostic]
     ctxt.getDiagnostics.asScala.foreach(diag => diags = diags :+ diag)
-    //ctxt.getDiagnostics.asScala.map(diag => coordinator.getRoot(uri).getCodeAction(uri, diag).map(cact => (cact.map(icact => Either.forRight[Command, CodeAction](icact))).asJava)).asJava
     coordinator.getRoot(uri).getCodeAction(uri, diags).map(cacts => cacts.map(cact => Either.forRight[Command, CodeAction](cact)).asJava).asJava.toCompletableFuture
-    /*
-    var res = Seq[Either[Command, CodeAction]]()
-    ctxt.getDiagnostics.asScala.foreach(diag =>
-      coordinator.getRoot(uri).getCodeAction(uri, diag).foreach(cact => {
-        coordinator.logger.info(s"[CACT:] ${cact.toString()}")
-        coordinator.logger.info(s"[RESPRE:] ${res.toString()}")
-        res = res :+ Either.forRight[Command, CodeAction](cact)
-        coordinator.logger.info(s"[RESPOST:] ${res.toString()}")
-      }))
-    //coordinator.logger.info(s"[Infer specifications on error] ${Verifier.config.inferenceMode() == OnError}")
-    //ctxt.getDiagnostics.asScala.foreach(diag => res = res +: Either.forRight[Command, CodeAction]())
-*/
-    /*
-      ctxt.getDiagnostics.asScala.foreach(diag =>
-        coordinator.getInferenceResults(diag).foreach(infres => {
-          val irca = new CodeAction(infres.getEdit)
-          val editmap: Map[String, java.util.List[TextEdit]] = Map(uri -> Seq(new TextEdit(
-            new Range(
-              new Position(infres.start.line - 1, infres.start.column - 1),
-              new Position(infres.end.line - 1, infres.end.column - 1)
-            ), infres.newText)).asJava)
-          irca.setKind(CodeActionKind.QuickFix)
-          irca.setEdit(new WorkspaceEdit(editmap.asJava))
-          irca.setDiagnostics(Seq(diag).asJava)
-          //irca.setCommand(new Command("Verify after specification inference", "viper.verify"))
-          res = res :+ Either.forRight[Command, CodeAction](irca)
-          coordinator.logger.info(s"[Res: textDocument/codeAction] ${irca.toString()}")
-        }))
-      coordinator.logger.info(s"[Info: textDocument/codeAction] ${res.toString()}")
-  */
-
-    //CompletableFuture.completedFuture(res.asJava)
   }
 
   override def formatting(params: DocumentFormattingParams) = {
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
index 71f0a486..6683e0d3 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
@@ -47,9 +47,6 @@ trait Manager {
   def addContainer(c: utility.LspContainer[_, _, _, _, _]): Unit
   def resetContainers(first: Boolean): Unit
 
-  //def toLspCommand(title: String, command: String, args: Option[Seq[AnyRef]]): lsp4j.Command
-  //def toLspWorkspaceEdit(edits: Seq[viper.silicon.biabduction.InferenceResult]): lsp4j.WorkspaceEdit
-
   def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction]
   def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit
 
@@ -124,11 +121,6 @@ trait StandardManager extends Manager {
   }
 
 
-
-  //def toLspWorkspaceEdit(edits: Seq[viper.silicon.biabduction.InferenceResult]): lsp4j.WorkspaceEdit = {
-  //  new lsp4j.WorkspaceEdit((Map(file.file_uri -> edits.map(edit => new lsp4j.TextEdit(new lsp4j.Range(Common.toPosition(edit.start), Common.toPosition(edit.end)), edit.newText)).asJava)).asJava)
-  //}
-
   // CodeAction
   type CodeActionContainer = utility.StageMapContainer.MapContainer[CodeAction, lsp4j.Diagnostic, lsp4j.CodeAction]
   val codeActionContainer: CodeActionContainer = utility.LspContainer(utility.CodeActionTranslator, () => {})
@@ -137,14 +129,12 @@ trait StandardManager extends Manager {
     codeAction.diags.foreach(diag => {
       cas = cas :+ new CodeAction(codeAction.backendClassName, codeAction.title, codeAction.kind, Seq(diag), codeAction.command, codeAction.edit, Some(diagnosticContainer.translator.translate(diag)()), codeAction.fileinfo)
     })
-    //codeAction.key = diagnosticContainer.translator.translate(codeAction.diag)()
     cas
   }
   containers.addOne(codeActionContainer)
 
-  //def getCodeAction() = codeActionContainer.get(())
-  def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] = codeActionContainer.get(diag)//CodeAction.fromDiag.getOrElse(diag, Seq.empty).map(cact => utility.CodeActionTranslator.translate(cact)())
-  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = add(codeActionContainer, first, vs.map(v => initCodeActionKey(v)).flatten)//vs.map(v => v.addToMap()))
+  def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] = codeActionContainer.get(diag)
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = add(codeActionContainer, first, vs.map(v => initCodeActionKey(v)).flatten)
 
   // CodeLens
   type CodeLensContainer = utility.StageArrayContainer.ArrayContainer[lsp.CodeLens, lsp4j.CodeLens]
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index 930c187a..c6e4bbde 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -10,7 +10,6 @@ import ch.qos.logback.classic.Logger
 import viper.server.frontends.lsp
 
 import scala.concurrent.Future
-import scala.jdk.CollectionConverters._
 import viper.server.core.ViperBackendConfig
 import viper.server.vsi.{AstJobId, VerJobId}
 
@@ -24,7 +23,6 @@ import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
 import org.eclipse.lsp4j
-import viper.server.frontends.lsp.Common
 import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
@@ -322,37 +320,25 @@ trait VerificationManager extends ManagesLeaf {
       val cachFlag: String = if (err.cached) " (cached)" else ""
       val message = s"$errMsgPrefixWithWhitespace${err.readableMessage}$cachFlag"
       val diagnostic = Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix)
-      coordinator.logger.info(s"[ERRORTYPE] ${errorType}")
-      coordinator.logger.info(s"[TAKE BRANCH?] ${errorType == "Verification error"}")
+      //If error contains inference results and inference mode is on error, create code action for inference results
       if (errorType == "Verification error"){
-        coordinator.logger.info(s"[BRANCH TAKEN WITH ERROR:] ${err.toString()}")
         err match {
-        case g: VerificationError =>
-          g.failureContexts.foreach { h =>
-            h match {
-              case h1: SiliconAbductionFailureContext =>
-                h1.fix match {
-                  case Some(irs) =>
-                    if (Verifier.config.inferenceMode() == OnError) {
-                      //coordinator.updateInferenceResults(lspdiag, irs)
-                      //val edits = new lsp4j.WorkspaceEdit((Map(file.file_uri -> irs.map(edit => new lsp4j.TextEdit(new lsp4j.Range(Common.toPosition(edit.start), Common.toPosition(edit.end)), edit.newText)).asJava)).asJava)
-                      //irs.foreach(ir => {cas = cas :+ CodeAction(backendClassName, ir.getEdit, "quickfix", Seq(diagnostic), None, Some(edits), None, this.file)
-                      cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
-                      //coordinator.logger.info(s"[CAS] ${cas.toString()}")})
-                      coordinator.logger.info(s"[IR] ${irs.toString()}")
-                      //coordinator.logger.info(s"[EDITS] ${edits.toString()}")
-                    }
-                  case None =>
-                    coordinator.logger.info(s"[IR] ${Seq.empty.toString()}")
-                }
-              case _ =>
-                coordinator.logger.info("NOT ABDUCTION FAILURE")
+          case g: VerificationError =>
+            g.failureContexts.foreach { h =>
+              h match {
+                case h1: SiliconAbductionFailureContext =>
+                  h1.fix match {
+                    case Some(irs) =>
+                      if (Verifier.config.inferenceMode() == OnError) {
+                        cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
+                      }
+                    case None => ()
+                  }
+                case _ => ()
+              }
             }
-          }
-          coordinator.logger.info(s"[ERROR CONTEXTS:] ${g.failureContexts.toString()}")
-        case _ =>
-          coordinator.logger.info("NOT VERIFICATION ERROR")
-      }
+          case _ => ()
+        }
       }
       (phase, diagnostic)
     })
@@ -362,7 +348,5 @@ trait VerificationManager extends ManagesLeaf {
       this.addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2))
     }
     this.root.addCodeAction(true)(cas)
-    coordinator.logger.info(s"CODE ACTIONS: ${cas.toString()}")
-    //coordinator.logger.info(s"THIS ROOT CODE ACTIONS: ${this.root.getCodeAction.toString()}")
   }
 }

From 3e679988ef01331e1a69fc9daf0a6515c16e6a1a Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Tue, 10 Mar 2026 14:39:48 +0100
Subject: [PATCH 03/12] first commit

---
 .../viper/server/frontends/lsp/Receiver.scala     |  9 ---------
 .../server/frontends/lsp/ast/ParseAstLsp.scala    |  6 +++++-
 .../frontends/lsp/ast/utility/CodeLens.scala      |  6 +++++-
 .../server/frontends/lsp/file/FileManager.scala   |  1 +
 .../frontends/lsp/file/ProjectManager.scala       |  3 +++
 .../server/frontends/lsp/file/Verification.scala  | 15 +++++++--------
 .../frontends/lsp/file/utility/Conversions.scala  |  5 +++--
 7 files changed, 24 insertions(+), 21 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index cdb92a08..9c8c1e24 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -414,16 +414,7 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
 
   @JsonNotification(C2S_Commands.Verify)
   def onVerify(data: VerifyParams): Unit = {
-    //DEBUG-------------------------------------------------------------------------
-    /*
-    if(data.enableInference){
-      coordinator.client.get.notifyStateChanged(lsp.StateChangeParams(6, 50, 4, 1, 0, "TEST", "carbon", 42, 0, data.uri, "TESTSTAGE", "TESTERROR", lsp.InferenceResultsParams(data.uri, Array(lsp.InferenceResult(1, 0, "TESTCODE")), true)))
-      return
-    }
-    */
-    //DEBUG-------------------------------------------------------------------------
     coordinator.logger.debug("On verifying")
-    //coordinator.updateInferenceResults(data.uri, Seq.empty)
     if (coordinator.canVerificationBeStarted(data.uri, data.content, data.manuallyTriggered)) {
       // stop all other verifications because the backend crashes if multiple verifications are run in parallel
       coordinator.logger.trace("verification can be started - all running verifications are now going to be stopped")
diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
index 1c2518cf..7e68c3b9 100644
--- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
@@ -10,9 +10,13 @@ import viper.silver.ast.utility.lsp._
 import viper.silver.ast.LineColumnPosition
 import viper.silver.parser.PStringLiteral
 import viper.silver.plugin.standard.adt._
+import viper.silicon.{Config, Map}
 
 object HasCodeLens {
-  def apply(p: PProgram): Seq[CodeLens] = p.deepCollect(PartialFunction.empty).flatten
+  def apply(p: PProgram): Seq[CodeLens] = p.deepCollect({
+    case m: PMethod =>
+      Some(CodeLens(RangePosition(m).get, "Infer Specifications", Some("viper.verify"), Some(m.idndef.name))).toSeq
+  }).flatten
 }
 
 object HasDocumentSymbol {
diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala
index a9df9379..3bad234e 100644
--- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala
@@ -13,8 +13,12 @@ trait HasCodeLens {
 case class CodeLens(
     /** The range in which this code lens is valid. Should only span a single line. */
     range: RangePosition,
+    /** The text this code lens displays. */
+    title: String,
     /** The command this code lens represents. */
-    command: String,
+    command: Option[String] = None,
+    /** The command this code lens represents. */
+    data: Option[Any] = None
 ) extends HasRangePositions with BelongsToFile {
   override def rangePositions: Seq[RangePosition] = Seq(range)
   override def file = range.file
diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
index 2b6d7b18..cb9427d5 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
@@ -40,6 +40,7 @@ trait ManagesLeaf {
   def resetDiagnostics(first: Boolean): Unit
   def resetContainers(first: Boolean): Unit
   def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit
 
   def getInFuture[T](f: => T): Future[T]
 }
diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
index d9f7482e..6224e5d3 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
@@ -142,6 +142,9 @@ trait ProjectManager extends ProjectAware {
     grouped foreach (g => toC(g._1)(g._2))
   }
 
+  override def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit =
+    addBtf(uri => getInProject(uri).addCodeAction(first), vs)
+
   def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit =
     addBtf(uri => getInProject(uri).addCodeLens(first), vs)
 
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index c6e4bbde..2864ed0e 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -23,7 +23,7 @@ import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
 import org.eclipse.lsp4j
-import viper.silver.ast.utility.lsp.RangePosition
+import viper.silver.ast.utility.lsp.{CodeLens, RangePosition}
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
 import viper.silicon.interfaces._
@@ -329,15 +329,14 @@ trait VerificationManager extends ManagesLeaf {
                 case h1: SiliconAbductionFailureContext =>
                   h1.fix match {
                     case Some(irs) =>
-                      if (Verifier.config.inferenceMode() == OnError) {
-                        cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
-                      }
-                    case None => ()
+                      cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
+                    case None => coordinator.logger.info("No inference results for error")
                   }
-                case _ => ()
+                case _ => coordinator.logger.info("No SilAbdFailureContext for error")
               }
             }
-          case _ => ()
+            if(g.failureContexts.isEmpty) coordinator.logger.info("No failure contexts for error")
+          case _ => coordinator.logger.info("No VerificationError for error")
         }
       }
       (phase, diagnostic)
@@ -347,6 +346,6 @@ trait VerificationManager extends ManagesLeaf {
     diags.groupBy(d => d._1).foreach { case (phase, diags) =>
       this.addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2))
     }
-    this.root.addCodeAction(true)(cas)
+    this.addCodeAction(true)(cas)
   }
 }
diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
index 3c920ba0..c9105abb 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
@@ -44,8 +44,9 @@ case object CodeActionTranslator extends Translates[CodeAction, lsp4j.CodeAction
 case object CodeLensTranslator extends Translates[lsp.CodeLens, lsp4j.CodeLens, Unit] {
   override def translate(lens: lsp.CodeLens)(i: Unit): lsp4j.CodeLens = {
     val range = Common.toRange(lens.range)
-    val command = new lsp4j.Command(lens.command, "")
-    new lsp4j.CodeLens(range, command, null)
+    val command = new lsp4j.Command(lens.title, lens.command.getOrElse(""))
+    val data = lens.data.orNull
+    new lsp4j.CodeLens(range, command, data)
   }
 }
 

From 66063a97b8d06fe41c2bf2235329881c658adf1e Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Mon, 23 Mar 2026 12:43:18 +0100
Subject: [PATCH 04/12] Cache working

---
 carbon                                        |  2 +-
 silicon                                       |  2 +-
 src/main/scala/viper/server/ViperConfig.scala |  7 ++++++
 .../scala/viper/server/core/ViperCache.scala  | 16 ++++++++----
 .../frontends/lsp/ast/ParseAstLsp.scala       |  6 ++---
 .../server/frontends/lsp/file/Manager.scala   |  4 +--
 .../frontends/lsp/file/RelayActor.scala       |  5 ++--
 .../frontends/lsp/file/Verification.scala     | 25 ++++++++++---------
 8 files changed, 40 insertions(+), 27 deletions(-)

diff --git a/carbon b/carbon
index 0a62400e..4761f900 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 0a62400e7140ef0570306be4ffd80dc1f7636fe7
+Subproject commit 4761f900b66fc7b395c628f0b5c20a5fb1389cbd
diff --git a/silicon b/silicon
index bc190326..59b6a35b 160000
--- a/silicon
+++ b/silicon
@@ -1 +1 @@
-Subproject commit bc19032696f2da1307710e5f47e033a6410057c1
+Subproject commit 59b6a35b210f6841c218be25542d2e38e76e2a76
diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala
index 37a23162..9ee10535 100644
--- a/src/main/scala/viper/server/ViperConfig.scala
+++ b/src/main/scala/viper/server/ViperConfig.scala
@@ -46,6 +46,13 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
     }
   }
 
+  val methodInference: ScallopOption[Boolean] = opt[Boolean]("methodInference",
+    descr = "Toggle option to infer specifications for methods.",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
   val backendSpecificCache: ScallopOption[Boolean] = opt[Boolean]("backendSpecificCache",
     descr = "Use a separate cache for each backend?",
     default = Some(false),
diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala
index 4679f420..ad6379ee 100644
--- a/src/main/scala/viper/server/core/ViperCache.scala
+++ b/src/main/scala/viper/server/core/ViperCache.scala
@@ -13,12 +13,14 @@ import net.liftweb.json.JsonAST.JObject
 import viper.server.core.ViperCache.logger
 import viper.server.vsi._
 import viper.silver.{ast => vpr}
-import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, Sub, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm}
+import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, FilePosition, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, IdentifierPosition, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LineColumnPosition, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, SourcePosition, Sub, TranslatedPosition, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm}
 import viper.silver.utility.CacheHelper
 import viper.silver.verifier.errors.{ApplyFailed, CallFailed, ContractNotWellformed, FoldFailed, HeuristicsFailed, IfFailed, InhaleFailed, Internal, LetWandFailed, UnfoldFailed, _}
-import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors}
+import viper.silver.verifier.{AbstractVerificationError, FailureContext, VerificationError, errors}
 import net.liftweb.json.Serialization.{read, write}
 import net.liftweb.json.{DefaultFormats, Formats, JArray, JField, JInt, JString, MappingException, ShortTypeHints}
+import viper.silicon.interfaces.SiliconAbductionFailureContext
+import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.verifier.reasons.{AssertionFalse, DivisionByZero, EpsilonAsParam, FeatureUnsupported, InsufficientPermission, InternalReason, InvalidPermMultiplication, LabelledStateNotReached, MagicWandChunkNotFound, MapKeyNotContained, NegativePermission, QPAssertionNotInjective, ReceiverNull, SeqIndexExceedsLength, SeqIndexNegative, UnexpectedNode}
 
 import java.nio.charset.StandardCharsets
@@ -84,6 +86,7 @@ object ViperCache extends Cache {
           logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName")
           // set cached flag:
           val cachedErrors = content.errors.map(setCached)
+          cachedErrors.foreach(e => e.failureContexts = content.failureContextsMap.toMap.getOrElse(e, Seq.empty[FailureContext]))
           CacheResult(concerning_method, cachedErrors)
         } catch {
           case e: Throwable =>
@@ -303,11 +306,12 @@ object ViperCache extends Cache {
         backendName: String, file: String,
         p: Program,
         errors: List[AbstractVerificationError]): SerializedViperCacheContent = {
+    val failureContextCacheMap = errors.map(e => setCached(e) -> (e.failureContexts.filter(c => c.isInstanceOf[SiliconAbductionFailureContext])))
 
     val key: String = getKey(file = file, backendName = backendName)
 
     implicit val formats: Formats = DefaultFormats.withHints(ViperCacheHelper.errorNodeHints(p, key))
-    SerializedViperCacheContent(write(ViperCacheContent(errors)))
+    SerializedViperCacheContent(write(ViperCacheContent(errors, failureContextCacheMap)))
   }
 }
 
@@ -521,7 +525,9 @@ object ViperCacheHelper {
     classOf[InternalReason], classOf[FeatureUnsupported], classOf[UnexpectedNode], classOf[AssertionFalse], classOf[EpsilonAsParam],
     classOf[ReceiverNull], classOf[DivisionByZero], classOf[NegativePermission], classOf[InsufficientPermission], classOf[InvalidPermMultiplication],
     classOf[MagicWandChunkNotFound], classOf[QPAssertionNotInjective], classOf[LabelledStateNotReached], classOf[SeqIndexNegative],
-    classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained]
+    classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained], classOf[SiliconAbductionFailureContext], classOf[LineColumnPosition],
+    classOf[FilePosition], classOf[RangePosition], classOf[IdentifierPosition], classOf[SourcePosition], classOf[TranslatedPosition],
+    classOf[IdentifierPosition]
   )) {
 
     override def serialize: PartialFunction[Any, JObject] = {
@@ -556,7 +562,7 @@ case class SerializedViperCacheContent(content: String) extends CacheContent
 /** Class containing the verification results of a viper verification run
   *
   */
-case class ViperCacheContent(errors: List[AbstractVerificationError])
+case class ViperCacheContent(errors: List[AbstractVerificationError], failureContextsMap: List[(AbstractVerificationError, Seq[FailureContext])])
 
 /** An access path holds a List of Numbers
   *
diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
index 7fab0da3..7eeaacc8 100644
--- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
@@ -10,12 +10,10 @@ import viper.silver.ast.utility.lsp._
 import viper.silver.ast.LineColumnPosition
 import viper.silver.parser.PStringLiteral
 import viper.silver.plugin.standard.adt._
-import viper.silicon.{Config, Map}
 
 object HasCodeLens {
-  def apply(p: PProgram): Seq[CodeLens] = p.deepCollect({
-    case m: PMethod =>
-      Some(CodeLens(RangePosition(m).get, "Infer Specifications", Some("viper.verify"), Some(m.idndef.name))).toSeq
+  def apply(p: PProgram, methodInference: Boolean): Seq[CodeLens] = p.deepCollect({
+    case m: PMethod if methodInference => Some(CodeLens(RangePosition(m).get, "Infer Specifications", Some("viper.verify"), Some(m.idndef.name))).toSeq
   }).flatten
 }
 
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
index 6683e0d3..f4730738 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
@@ -17,7 +17,7 @@ import viper.server.frontends.lsp.Lsp4jSemanticHighlight
 import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.Common
-import viper.silicon.biabduction.InferenceResult
+import viper.silicon.biabduction.ProgramEdit
 
 case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends lsp.HasRangePositions with lsp.BelongsToFile {
   override def rangePositions: Seq[lsp.RangePosition] = Seq(position)
@@ -29,7 +29,7 @@ case class CodeAction(backendClassName: Option[String],
                       kind: String,
                       diags: Seq[Diagnostic],
                       command: Option[(String, String)],
-                      edit: Option[Seq[InferenceResult]],
+                      edit: Option[Seq[ProgramEdit]],
                       diagkey: Option[lsp4j.Diagnostic],
                       fileinfo: PathInfo
                      ) extends lsp.HasRangePositions with lsp.BelongsToFile with utility.HasKey[lsp4j.Diagnostic] {
diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
index f88ca68c..4957ab67 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
@@ -12,7 +12,7 @@ import viper.server.frontends.lsp.VerificationState._
 import viper.server.frontends.lsp.VerificationSuccess._
 import viper.silver.ast
 import viper.silver.reporter._
-import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage}
+import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage, VerificationError}
 import viper.server.frontends.lsp.file.ProgressCoordinator
 import viper.silver.parser._
 
@@ -130,7 +130,8 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends
         task.lastPhase = Some(phase)
 
         val beginnerMode = coordinator.server.config.beginnerMode()
-        task.addCodeLens(true)(HasCodeLens(pProgram))
+        val methodInference = coordinator.server.config.methodInference()
+        task.addCodeLens(true)(HasCodeLens(pProgram, methodInference))
         task.addDocumentSymbol(true)(HasDocumentSymbol(pProgram).toSeq)
         task.addHoverHint(true)(HasHoverHints(pProgram))
         task.addGotoDefinition(true)(HasGotoDefinitions(pProgram))
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index 607fa831..7aca10fa 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -338,19 +338,20 @@ trait VerificationManager extends ManagesLeaf {
       if (errorType == "Verification error"){
         err match {
           case g: VerificationError =>
-            g.failureContexts.foreach { h =>
-              h match {
-                case h1: SiliconAbductionFailureContext =>
-                  h1.fix match {
-                    case Some(irs) =>
-                      cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
-                    case None => coordinator.logger.info("No inference results for error")
-                  }
-                case _ => coordinator.logger.info("No SilAbdFailureContext for error")
-              }
+            g.failureContexts.foreach {
+              case h1: SiliconAbductionFailureContext =>
+                h1.fix match {
+                  case Some(irs) =>
+                    cas = cas :+ CodeAction(backendClassName, irs.map(ir =>
+                      if (ir.newText.equals(""))
+                        "remove: Line " + ir.start.line + ", Col " + ir.start.column + " to Line " + ir.end.line + ", Col " + ir.end.column
+                      else
+                        "insert: " + ir.newText).foldLeft("")((cur: String, next: String) => if (cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
+                  case None => ()
+                }
+              case _ => ()
             }
-            if(g.failureContexts.isEmpty) coordinator.logger.info("No failure contexts for error")
-          case _ => coordinator.logger.info("No VerificationError for error")
+          case _ => ()
         }
       }
       (phase, diagnostic)

From f62dec594e56e8f85f1ae0f0ff57d13b5262c09a Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Mon, 23 Mar 2026 14:19:21 +0100
Subject: [PATCH 05/12] Cache working

---
 carbon                                        |  2 +-
 silicon                                       |  2 +-
 .../scala/viper/server/core/ViperCache.scala  | 16 ++++--
 .../server/frontends/lsp/DataProtocol.scala   |  3 +-
 .../viper/server/frontends/lsp/Receiver.scala |  9 ----
 .../frontends/lsp/file/FileManager.scala      |  2 +
 .../server/frontends/lsp/file/Manager.scala   |  5 +-
 .../frontends/lsp/file/ProjectManager.scala   |  2 +
 .../frontends/lsp/file/Verification.scala     | 50 ++++++++++++-------
 9 files changed, 52 insertions(+), 39 deletions(-)

diff --git a/carbon b/carbon
index 0a62400e..4761f900 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 0a62400e7140ef0570306be4ffd80dc1f7636fe7
+Subproject commit 4761f900b66fc7b395c628f0b5c20a5fb1389cbd
diff --git a/silicon b/silicon
index bc190326..59b6a35b 160000
--- a/silicon
+++ b/silicon
@@ -1 +1 @@
-Subproject commit bc19032696f2da1307710e5f47e033a6410057c1
+Subproject commit 59b6a35b210f6841c218be25542d2e38e76e2a76
diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala
index 4679f420..ad6379ee 100644
--- a/src/main/scala/viper/server/core/ViperCache.scala
+++ b/src/main/scala/viper/server/core/ViperCache.scala
@@ -13,12 +13,14 @@ import net.liftweb.json.JsonAST.JObject
 import viper.server.core.ViperCache.logger
 import viper.server.vsi._
 import viper.silver.{ast => vpr}
-import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, Sub, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm}
+import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, FilePosition, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, IdentifierPosition, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LineColumnPosition, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, SourcePosition, Sub, TranslatedPosition, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm}
 import viper.silver.utility.CacheHelper
 import viper.silver.verifier.errors.{ApplyFailed, CallFailed, ContractNotWellformed, FoldFailed, HeuristicsFailed, IfFailed, InhaleFailed, Internal, LetWandFailed, UnfoldFailed, _}
-import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors}
+import viper.silver.verifier.{AbstractVerificationError, FailureContext, VerificationError, errors}
 import net.liftweb.json.Serialization.{read, write}
 import net.liftweb.json.{DefaultFormats, Formats, JArray, JField, JInt, JString, MappingException, ShortTypeHints}
+import viper.silicon.interfaces.SiliconAbductionFailureContext
+import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.verifier.reasons.{AssertionFalse, DivisionByZero, EpsilonAsParam, FeatureUnsupported, InsufficientPermission, InternalReason, InvalidPermMultiplication, LabelledStateNotReached, MagicWandChunkNotFound, MapKeyNotContained, NegativePermission, QPAssertionNotInjective, ReceiverNull, SeqIndexExceedsLength, SeqIndexNegative, UnexpectedNode}
 
 import java.nio.charset.StandardCharsets
@@ -84,6 +86,7 @@ object ViperCache extends Cache {
           logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName")
           // set cached flag:
           val cachedErrors = content.errors.map(setCached)
+          cachedErrors.foreach(e => e.failureContexts = content.failureContextsMap.toMap.getOrElse(e, Seq.empty[FailureContext]))
           CacheResult(concerning_method, cachedErrors)
         } catch {
           case e: Throwable =>
@@ -303,11 +306,12 @@ object ViperCache extends Cache {
         backendName: String, file: String,
         p: Program,
         errors: List[AbstractVerificationError]): SerializedViperCacheContent = {
+    val failureContextCacheMap = errors.map(e => setCached(e) -> (e.failureContexts.filter(c => c.isInstanceOf[SiliconAbductionFailureContext])))
 
     val key: String = getKey(file = file, backendName = backendName)
 
     implicit val formats: Formats = DefaultFormats.withHints(ViperCacheHelper.errorNodeHints(p, key))
-    SerializedViperCacheContent(write(ViperCacheContent(errors)))
+    SerializedViperCacheContent(write(ViperCacheContent(errors, failureContextCacheMap)))
   }
 }
 
@@ -521,7 +525,9 @@ object ViperCacheHelper {
     classOf[InternalReason], classOf[FeatureUnsupported], classOf[UnexpectedNode], classOf[AssertionFalse], classOf[EpsilonAsParam],
     classOf[ReceiverNull], classOf[DivisionByZero], classOf[NegativePermission], classOf[InsufficientPermission], classOf[InvalidPermMultiplication],
     classOf[MagicWandChunkNotFound], classOf[QPAssertionNotInjective], classOf[LabelledStateNotReached], classOf[SeqIndexNegative],
-    classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained]
+    classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained], classOf[SiliconAbductionFailureContext], classOf[LineColumnPosition],
+    classOf[FilePosition], classOf[RangePosition], classOf[IdentifierPosition], classOf[SourcePosition], classOf[TranslatedPosition],
+    classOf[IdentifierPosition]
   )) {
 
     override def serialize: PartialFunction[Any, JObject] = {
@@ -556,7 +562,7 @@ case class SerializedViperCacheContent(content: String) extends CacheContent
 /** Class containing the verification results of a viper verification run
   *
   */
-case class ViperCacheContent(errors: List[AbstractVerificationError])
+case class ViperCacheContent(errors: List[AbstractVerificationError], failureContextsMap: List[(AbstractVerificationError, Seq[FailureContext])])
 
 /** An access path holds a List of Numbers
   *
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index 32795722..d73638e5 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -85,8 +85,7 @@ case class VerifyParams (
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
-              customArgs: String,           // contains the path of the file that should be verified
-              enableInference: Boolean)     // determines whether inference should be performed on verification error
+              customArgs: String)     // determines whether inference should be performed on verification error
 
 
 case class ReformatParams (uri: String)
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index cdb92a08..9c8c1e24 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -414,16 +414,7 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
 
   @JsonNotification(C2S_Commands.Verify)
   def onVerify(data: VerifyParams): Unit = {
-    //DEBUG-------------------------------------------------------------------------
-    /*
-    if(data.enableInference){
-      coordinator.client.get.notifyStateChanged(lsp.StateChangeParams(6, 50, 4, 1, 0, "TEST", "carbon", 42, 0, data.uri, "TESTSTAGE", "TESTERROR", lsp.InferenceResultsParams(data.uri, Array(lsp.InferenceResult(1, 0, "TESTCODE")), true)))
-      return
-    }
-    */
-    //DEBUG-------------------------------------------------------------------------
     coordinator.logger.debug("On verifying")
-    //coordinator.updateInferenceResults(data.uri, Seq.empty)
     if (coordinator.canVerificationBeStarted(data.uri, data.content, data.manuallyTriggered)) {
       // stop all other verifications because the backend crashes if multiple verifications are run in parallel
       coordinator.logger.trace("verification can be started - all running verifications are now going to be stopped")
diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
index 2b6d7b18..7d591fe4 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
@@ -41,6 +41,8 @@ trait ManagesLeaf {
   def resetContainers(first: Boolean): Unit
   def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit
 
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction])
+
   def getInFuture[T](f: => T): Future[T]
 }
 
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
index 6683e0d3..f926a072 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
@@ -17,7 +17,7 @@ import viper.server.frontends.lsp.Lsp4jSemanticHighlight
 import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.Common
-import viper.silicon.biabduction.InferenceResult
+import viper.silicon.biabduction.ProgramEdit
 
 case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends lsp.HasRangePositions with lsp.BelongsToFile {
   override def rangePositions: Seq[lsp.RangePosition] = Seq(position)
@@ -29,7 +29,7 @@ case class CodeAction(backendClassName: Option[String],
                       kind: String,
                       diags: Seq[Diagnostic],
                       command: Option[(String, String)],
-                      edit: Option[Seq[InferenceResult]],
+                      edit: Option[Seq[ProgramEdit]],
                       diagkey: Option[lsp4j.Diagnostic],
                       fileinfo: PathInfo
                      ) extends lsp.HasRangePositions with lsp.BelongsToFile with utility.HasKey[lsp4j.Diagnostic] {
@@ -132,7 +132,6 @@ trait StandardManager extends Manager {
     cas
   }
   containers.addOne(codeActionContainer)
-
   def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] = codeActionContainer.get(diag)
   def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = add(codeActionContainer, first, vs.map(v => initCodeActionKey(v)).flatten)
 
diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
index d9f7482e..6aa80b43 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
@@ -141,6 +141,8 @@ trait ProjectManager extends ProjectAware {
     })
     grouped foreach (g => toC(g._1)(g._2))
   }
+  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit =
+    addBtf(uri => getInProject(uri).addCodeAction(first), vs)
 
   def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit =
     addBtf(uri => getInProject(uri).addCodeLens(first), vs)
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index c6e4bbde..7aca10fa 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -23,7 +23,7 @@ import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
 import org.eclipse.lsp4j
-import viper.silver.ast.utility.lsp.RangePosition
+import viper.silver.ast.utility.lsp.{CodeLens, RangePosition}
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
 import viper.silicon.interfaces._
@@ -223,11 +223,23 @@ trait VerificationManager extends ManagesLeaf {
     if (handler.isVerifying) stop()
     futureCancel.getOrElse(Future.unit).map(_ => {
       lastPhase = None
-      handler.clearWaitingOn()
-      val astJob = startConstructAst(backend, loader, mt) match {
-        case None => return Future.successful(false)
-        case Some(ast) => ast
+
+
+      val astJob = handler.astHandle match {
+        // If an AST job is already running (due file edit or LSP features), reuse it instead of cancelling and rebuilding.
+        case Some(existingAst) =>
+          coordinator.logger.info(s"Reusing existing AST job ${existingAst.id} for verification")
+          manuallyTriggered = mt
+          existingAst
+        // Otherwise, start a new AST job for verification.
+        case None =>
+          handler.clearWaitingOn()
+          startConstructAst(backend, loader, mt) match {
+            case None => return Future.successful(false)
+            case Some(ast) => ast
+          }
       }
+
       val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger))
       if (verJob.id >= 0) {
         // Execute all handles
@@ -240,6 +252,8 @@ trait VerificationManager extends ManagesLeaf {
         futureVer = coordinator.server.startStreamingVer(verJob, receiver, Some(coordinator.localLogger))
         true
       } else {
+        // Ver pool full — free the orphaned AST slot
+        coordinator.server.discardAstJobLookup(astJob)
         false
       }
     })
@@ -324,18 +338,18 @@ trait VerificationManager extends ManagesLeaf {
       if (errorType == "Verification error"){
         err match {
           case g: VerificationError =>
-            g.failureContexts.foreach { h =>
-              h match {
-                case h1: SiliconAbductionFailureContext =>
-                  h1.fix match {
-                    case Some(irs) =>
-                      if (Verifier.config.inferenceMode() == OnError) {
-                        cas = cas :+ CodeAction(backendClassName, irs.map(ir => ir.getEdit).foldLeft("")((cur: String, next: String) => if(cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
-                      }
-                    case None => ()
-                  }
-                case _ => ()
-              }
+            g.failureContexts.foreach {
+              case h1: SiliconAbductionFailureContext =>
+                h1.fix match {
+                  case Some(irs) =>
+                    cas = cas :+ CodeAction(backendClassName, irs.map(ir =>
+                      if (ir.newText.equals(""))
+                        "remove: Line " + ir.start.line + ", Col " + ir.start.column + " to Line " + ir.end.line + ", Col " + ir.end.column
+                      else
+                        "insert: " + ir.newText).foldLeft("")((cur: String, next: String) => if (cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file)
+                  case None => ()
+                }
+              case _ => ()
             }
           case _ => ()
         }
@@ -347,6 +361,6 @@ trait VerificationManager extends ManagesLeaf {
     diags.groupBy(d => d._1).foreach { case (phase, diags) =>
       this.addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2))
     }
-    this.root.addCodeAction(true)(cas)
+    this.addCodeAction(true)(cas)
   }
 }

From 69cff6f0df80324cd7150322a94d2b6d3cae7e0d Mon Sep 17 00:00:00 2001
From: Adil Sadikovic <ad-sadikovic@hotmail.com>
Date: Sun, 12 Apr 2026 17:07:54 +0200
Subject: [PATCH 06/12] Update Manager.scala

---
 src/main/scala/viper/server/frontends/lsp/file/Manager.scala | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
index f926a072..13be142e 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
@@ -15,6 +15,7 @@ import scala.collection.mutable.ArrayBuffer
 import viper.server.frontends.lsp.file.FileContent
 import viper.server.frontends.lsp.Lsp4jSemanticHighlight
 import org.eclipse.lsp4j
+
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.Common
 import viper.silicon.biabduction.ProgramEdit

From 0d704f834b26e13d1ea9d53896676ea3df70baa8 Mon Sep 17 00:00:00 2001
From: Adil Sadikovic <ad-sadikovic@hotmail.com>
Date: Sun, 12 Apr 2026 17:08:12 +0200
Subject: [PATCH 07/12] Update Manager.scala

---
 src/main/scala/viper/server/frontends/lsp/file/Manager.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
index 13be142e..84b36d87 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala
@@ -14,8 +14,8 @@ import scala.jdk.CollectionConverters._
 import scala.collection.mutable.ArrayBuffer
 import viper.server.frontends.lsp.file.FileContent
 import viper.server.frontends.lsp.Lsp4jSemanticHighlight
-import org.eclipse.lsp4j
 
+import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp
 import viper.server.frontends.lsp.Common
 import viper.silicon.biabduction.ProgramEdit

From 8b4a42c5523c50eba9c22044a94a52be0a8a094d Mon Sep 17 00:00:00 2001
From: Adil Sadikovic <ad-sadikovic@hotmail.com>
Date: Sun, 12 Apr 2026 17:10:10 +0200
Subject: [PATCH 08/12] Update DataProtocol.scala

---
 src/main/scala/viper/server/frontends/lsp/DataProtocol.scala | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index d73638e5..cd3c3850 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -81,12 +81,11 @@ case class BackendProperties(
 
 case class VerifyParams (
               uri: String,                  // file to verify
-              content: String,              // contents of file to verify
+              content: String,             // contents of file to verify
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
-              customArgs: String)     // determines whether inference should be performed on verification error
-
+              customArgs: String)            // contains the path of the file that should be verified
 
 case class ReformatParams (uri: String)
 

From d9ec3db8fa658a93dc49e07c4f3738a1b85518d3 Mon Sep 17 00:00:00 2001
From: Adil Sadikovic <ad-sadikovic@hotmail.com>
Date: Sun, 12 Apr 2026 17:16:00 +0200
Subject: [PATCH 09/12] Update Verification.scala

---
 .../viper/server/frontends/lsp/file/Verification.scala | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index 7aca10fa..e2946ca6 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -8,17 +8,16 @@ package viper.server.frontends.lsp.file
 
 import ch.qos.logback.classic.Logger
 import viper.server.frontends.lsp
-
 import scala.concurrent.Future
 import viper.server.core.ViperBackendConfig
 import viper.server.vsi.{AstJobId, VerJobId}
-
 import scala.concurrent.ExecutionContext
 import akka.actor.Props
+
 import viper.server.frontends.lsp.VerificationSuccess._
 import viper.server.frontends.lsp.VerificationState._
-import viper.silver.verifier.AbstractError
 
+import viper.silver.verifier.AbstractError
 import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
@@ -239,7 +238,6 @@ trait VerificationManager extends ManagesLeaf {
             case Some(ast) => ast
           }
       }
-
       val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger))
       if (verJob.id >= 0) {
         // Execute all handles
@@ -326,12 +324,12 @@ trait VerificationManager extends ManagesLeaf {
       }
       files.add(rp.file.toUri().toString())
 
-      val errFullId = if (err.fullId != null) s"[${err.fullId}] " else ""
+      val errFullId = if(err.fullId != null) s"[${err.fullId}] " else ""
       val backendString = if (backendClassName.isDefined) s" [${backendClassName.get}]" else ""
       coordinator.logger.debug(s"$errorType:$backendString $errFullId" +
         s"${range.getStart.getLine + 1}:${range.getStart.getCharacter + 1} $errMsgPrefixWithWhitespace${err.readableMessage}s")
 
-      val cachFlag: String = if (err.cached) " (cached)" else ""
+      val cachFlag: String = if(err.cached) " (cached)" else ""
       val message = s"$errMsgPrefixWithWhitespace${err.readableMessage}$cachFlag"
       val diagnostic = Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix)
       //If error contains inference results and inference mode is on error, create code action for inference results

From 89adcd624f7f9d364278c67cef324aad3c9469d3 Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Tue, 21 Apr 2026 02:55:41 +0200
Subject: [PATCH 10/12] Inference Mode Implemented

---
 src/main/scala/viper/server/ViperConfig.scala |  7 ------
 .../scala/viper/server/core/ViperCache.scala  | 12 ++++++----
 .../frontends/lsp/ClientCoordinator.scala     |  8 +++++++
 .../frontends/lsp/CommandProtocol.scala       |  1 +
 .../server/frontends/lsp/DataProtocol.scala   | 14 +++++++++--
 .../frontends/lsp/IdeLanguageClient.scala     |  3 +++
 .../frontends/lsp/ast/ParseAstLsp.scala       |  4 +---
 .../frontends/lsp/ast/utility/CodeLens.scala  |  2 +-
 .../frontends/lsp/file/RelayActor.scala       |  5 ++--
 .../frontends/lsp/file/Verification.scala     | 24 +++++++++++++++++--
 .../lsp/file/utility/Conversions.scala        | 18 +++++++++++---
 11 files changed, 72 insertions(+), 26 deletions(-)

diff --git a/src/main/scala/viper/server/ViperConfig.scala b/src/main/scala/viper/server/ViperConfig.scala
index 9ee10535..37a23162 100644
--- a/src/main/scala/viper/server/ViperConfig.scala
+++ b/src/main/scala/viper/server/ViperConfig.scala
@@ -46,13 +46,6 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
     }
   }
 
-  val methodInference: ScallopOption[Boolean] = opt[Boolean]("methodInference",
-    descr = "Toggle option to infer specifications for methods.",
-    default = Some(false),
-    noshort = true,
-    hidden = false
-  )
-
   val backendSpecificCache: ScallopOption[Boolean] = opt[Boolean]("backendSpecificCache",
     descr = "Use a separate cache for each backend?",
     default = Some(false),
diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala
index ad6379ee..482aec19 100644
--- a/src/main/scala/viper/server/core/ViperCache.scala
+++ b/src/main/scala/viper/server/core/ViperCache.scala
@@ -85,8 +85,11 @@ object ViperCache extends Cache {
           val content = read[ViperCacheContent](ce.content.asInstanceOf[SerializedViperCacheContent].content)
           logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName")
           // set cached flag:
-          val cachedErrors = content.errors.map(setCached)
-          cachedErrors.foreach(e => e.failureContexts = content.failureContextsMap.toMap.getOrElse(e, Seq.empty[FailureContext]))
+          val cachedErrors = content.errors.map(e => {
+            val ce = setCached(e._1)
+            ce.failureContexts = e._2
+            ce
+          })
           CacheResult(concerning_method, cachedErrors)
         } catch {
           case e: Throwable =>
@@ -306,12 +309,11 @@ object ViperCache extends Cache {
         backendName: String, file: String,
         p: Program,
         errors: List[AbstractVerificationError]): SerializedViperCacheContent = {
-    val failureContextCacheMap = errors.map(e => setCached(e) -> (e.failureContexts.filter(c => c.isInstanceOf[SiliconAbductionFailureContext])))
 
     val key: String = getKey(file = file, backendName = backendName)
 
     implicit val formats: Formats = DefaultFormats.withHints(ViperCacheHelper.errorNodeHints(p, key))
-    SerializedViperCacheContent(write(ViperCacheContent(errors, failureContextCacheMap)))
+    SerializedViperCacheContent(write(ViperCacheContent(errors.map(e => (e, e.failureContexts.filter(c => c.isInstanceOf[SiliconAbductionFailureContext]))))))
   }
 }
 
@@ -562,7 +564,7 @@ case class SerializedViperCacheContent(content: String) extends CacheContent
 /** Class containing the verification results of a viper verification run
   *
   */
-case class ViperCacheContent(errors: List[AbstractVerificationError], failureContextsMap: List[(AbstractVerificationError, Seq[FailureContext])])
+case class ViperCacheContent(errors: List[(AbstractVerificationError, Seq[FailureContext])])
 
 /** An access path holds a List of Numbers
   *
diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index b3d59ad8..831e582e 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -209,6 +209,14 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
     }
   }
 
+  def sendInferenceResults(irs: InferenceResultParams): Unit = {
+    try{
+      client.get.notifyInferenceResults(irs)
+    } catch {
+      case e: Throwable => logger.debug(s"Error while sending inference results: $e")
+    }
+  }
+
   def refreshEndings(): Future[Array[String]] = {
     client.map{_.requestVprFileEndings().asScala.map(response => {
       _vprFileEndings = Some(response.fileEndings)
diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
index e67e5a37..e5d759c3 100644
--- a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
@@ -32,6 +32,7 @@ object S2C_Commands {
   final val Log = "Log"
   final val Hint = "Hint"
   final val VerificationNotStarted = "VerificationNotStarted"
+  final val InferenceResults = "InferenceResults"
   // final val StopDebugging = "StopDebugging"
   // final val StepsAsDecorationOptions = "StepsAsDecorationOptions"
   // final val HeapGraph = "HeapGraph"
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index 32795722..215870a9 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -85,8 +85,7 @@ case class VerifyParams (
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
-              customArgs: String,           // contains the path of the file that should be verified
-              enableInference: Boolean)     // determines whether inference should be performed on verification error
+              customArgs: String)           // contains the path of the file that should be verified
 
 
 case class ReformatParams (uri: String)
@@ -180,6 +179,17 @@ case class StateChangeParams(
               stage: String = null,
               error: String = null)
 
+case class InferenceResultParams(
+              inferenceResults: Array[InferenceResult])
+
+case class InferenceResult(
+              start_line: Int,
+              start_col: Int,
+              end_line: Int,
+              end_col: Int,
+              edit: String,
+              file_uri: String)
+
 case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int)
 
 /**
diff --git a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala
index 0b614f3b..600ba568 100644
--- a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala
+++ b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala
@@ -41,4 +41,7 @@ trait IdeLanguageClient extends LanguageClient {
 
   @JsonNotification(S2C_Commands.StateChange)
   def notifyStateChanged(params: StateChangeParams): Unit
+
+  @JsonNotification(S2C_Commands.InferenceResults)
+  def notifyInferenceResults(irs: InferenceResultParams): Unit
 }
diff --git a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
index 7eeaacc8..80bb483e 100644
--- a/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala
@@ -12,9 +12,7 @@ import viper.silver.parser.PStringLiteral
 import viper.silver.plugin.standard.adt._
 
 object HasCodeLens {
-  def apply(p: PProgram, methodInference: Boolean): Seq[CodeLens] = p.deepCollect({
-    case m: PMethod if methodInference => Some(CodeLens(RangePosition(m).get, "Infer Specifications", Some("viper.verify"), Some(m.idndef.name))).toSeq
-  }).flatten
+  def apply(p: PProgram): Seq[CodeLens] = p.deepCollect(PartialFunction.empty).flatten
 }
 
 object HasDocumentSymbol {
diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala
index 3bad234e..83faf45e 100644
--- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala
@@ -18,7 +18,7 @@ case class CodeLens(
     /** The command this code lens represents. */
     command: Option[String] = None,
     /** The command this code lens represents. */
-    data: Option[Any] = None
+    args: Option[Seq[AnyRef]] = None
 ) extends HasRangePositions with BelongsToFile {
   override def rangePositions: Seq[RangePosition] = Seq(range)
   override def file = range.file
diff --git a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
index 4957ab67..f88ca68c 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
@@ -12,7 +12,7 @@ import viper.server.frontends.lsp.VerificationState._
 import viper.server.frontends.lsp.VerificationSuccess._
 import viper.silver.ast
 import viper.silver.reporter._
-import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage, VerificationError}
+import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage}
 import viper.server.frontends.lsp.file.ProgressCoordinator
 import viper.silver.parser._
 
@@ -130,8 +130,7 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends
         task.lastPhase = Some(phase)
 
         val beginnerMode = coordinator.server.config.beginnerMode()
-        val methodInference = coordinator.server.config.methodInference()
-        task.addCodeLens(true)(HasCodeLens(pProgram, methodInference))
+        task.addCodeLens(true)(HasCodeLens(pProgram))
         task.addDocumentSymbol(true)(HasDocumentSymbol(pProgram).toSeq)
         task.addHoverHint(true)(HasHoverHints(pProgram))
         task.addGotoDefinition(true)(HasGotoDefinitions(pProgram))
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index 7aca10fa..5b015805 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -21,14 +21,16 @@ import viper.silver.verifier.AbstractError
 
 import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
-import org.eclipse.lsp4j.Range
+import org.eclipse.lsp4j.{Range, WorkspaceEdit}
 import org.eclipse.lsp4j
+import viper.server.frontends.lsp.{InferenceResult, InferenceResultParams}
+import viper.server.frontends.lsp.file.utility.TranslationHelper
+import viper.silicon.Config
 import viper.silver.ast.utility.lsp.{CodeLens, RangePosition}
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
 import viper.silicon.interfaces._
 import viper.silver.verifier._
-import viper.silicon.Config.InferenceMode.OnError
 import viper.silicon.verifier.Verifier
 
 case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) {
@@ -128,6 +130,7 @@ trait VerificationManager extends ManagesLeaf {
   //other
   var lastSuccess: VerificationSuccess = NA
   var internalErrorMessage: String = ""
+  var inferenceMode: Boolean = false
 
   //state specific to one verification
   var is_aborting: Boolean = false
@@ -217,6 +220,7 @@ trait VerificationManager extends ManagesLeaf {
   def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = {
     lastBackendClassName = Some(backendClassName)
     lastCustomArgs = Some(customArgs)
+    inferenceMode = customArgs.contains("--inferenceMode=full")
     val backend = ViperBackendConfig(backendClassName, customArgs)
 
     coordinator.logger.info(s"verify $filename ($backendClassName $customArgs)")
@@ -285,6 +289,7 @@ trait VerificationManager extends ManagesLeaf {
     val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("")
     val files = HashSet[String]()
     var cas: Seq[CodeAction] = Seq.empty
+    var lsp_irs: Array[InferenceResult] = Array.empty
 
     val diags = errors.map(err => {
       coordinator.logger.info(s"Handling error ${err.toString()}")
@@ -342,6 +347,15 @@ trait VerificationManager extends ManagesLeaf {
               case h1: SiliconAbductionFailureContext =>
                 h1.fix match {
                   case Some(irs) =>
+                    irs.foreach(ir =>
+                      lsp_irs = lsp_irs :+ InferenceResult(
+                        start_line = ir.start.line,
+                        start_col = ir.start.column,
+                        end_line = ir.end.line,
+                        end_col = ir.end.column,
+                        edit = ir.newText,
+                        file_uri = this.file.file_uri)
+                    )
                     cas = cas :+ CodeAction(backendClassName, irs.map(ir =>
                       if (ir.newText.equals(""))
                         "remove: Line " + ir.start.line + ", Col " + ir.start.column + " to Line " + ir.end.line + ", Col " + ir.end.column
@@ -356,6 +370,12 @@ trait VerificationManager extends ManagesLeaf {
       }
       (phase, diagnostic)
     })
+
+    if(inferenceMode){
+      coordinator.sendInferenceResults(InferenceResultParams(inferenceResults = lsp_irs))
+      return
+    }
+
     diagnosticCount += errors.size
     errorCount += diags.count(_._2.severity == lsp4j.DiagnosticSeverity.Error)
     diags.groupBy(d => d._1).foreach { case (phase, diags) =>
diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
index c9105abb..5727316c 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
@@ -23,6 +23,18 @@ trait Translates[-T, +U, I] {
   def translate(t: Seq[T])(i: I)(implicit @annotation.unused log: Logger): Seq[U] = t.map(translate(_)(i))
 }
 
+object TranslationHelper {
+  def toWorkspaceEdit(uri: String, edits: Seq[viper.silicon.biabduction.ProgramEdit]): WorkspaceEdit = {
+    new WorkspaceEdit((Map(uri -> edits.map(edit =>
+      new lsp4j.TextEdit(
+        new lsp4j.Range(
+          Common.toPosition(edit.start),
+          Common.toPosition(edit.end)),
+        edit.newText)
+    ).asJava)).asJava)
+  }
+}
+
 case object CodeActionTranslator extends Translates[CodeAction, lsp4j.CodeAction, lsp4j.Diagnostic] {
   override def translate(cact: CodeAction)(i: lsp4j.Diagnostic): lsp4j.CodeAction = {
     val lspca = new lsp4j.CodeAction(cact.title)
@@ -30,7 +42,7 @@ case object CodeActionTranslator extends Translates[CodeAction, lsp4j.CodeAction
     lspca.setDiagnostics(Seq(cact.key).asJava)
     lspca.setEdit(
       cact.edit match {
-        case Some(e) => new WorkspaceEdit((Map(cact.fileinfo.file_uri -> e.map(edit => new lsp4j.TextEdit(new lsp4j.Range(Common.toPosition(edit.start), Common.toPosition(edit.end)), edit.newText)).asJava)).asJava)
+        case Some(e) => TranslationHelper.toWorkspaceEdit(cact.fileinfo.file_uri, e)
         case None => null
       })
     lspca.setCommand(cact.command match {
@@ -44,8 +56,8 @@ case object CodeActionTranslator extends Translates[CodeAction, lsp4j.CodeAction
 case object CodeLensTranslator extends Translates[lsp.CodeLens, lsp4j.CodeLens, Unit] {
   override def translate(lens: lsp.CodeLens)(i: Unit): lsp4j.CodeLens = {
     val range = Common.toRange(lens.range)
-    val command = new lsp4j.Command(lens.title, lens.command.getOrElse(""))
-    val data = lens.data.orNull
+    val command = new lsp4j.Command(lens.title, lens.command.getOrElse(""), lens.args.getOrElse(Seq.empty).asJava)
+    val data = lens.args.orNull
     new lsp4j.CodeLens(range, command, data)
   }
 }

From d869a66ddb4d8150fa12641462ddc13618a55e30 Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Tue, 21 Apr 2026 18:04:17 +0200
Subject: [PATCH 11/12] Silicon backend selected

---
 silicon | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/silicon b/silicon
index 59b6a35b..cfc23979 160000
--- a/silicon
+++ b/silicon
@@ -1 +1 @@
-Subproject commit 59b6a35b210f6841c218be25542d2e38e76e2a76
+Subproject commit cfc23979faad76058da633f76313633456674866

From 797cc022e60a34e76be5e90f0aadcd41a3b6e165 Mon Sep 17 00:00:00 2001
From: Adil <asadikovic@student.ethz.ch>
Date: Tue, 21 Apr 2026 18:42:59 +0200
Subject: [PATCH 12/12] Merge completed

---
 .../viper/server/frontends/lsp/file/FileManager.scala    | 2 --
 .../viper/server/frontends/lsp/file/ProjectManager.scala | 3 ---
 .../viper/server/frontends/lsp/file/Verification.scala   | 9 +++++----
 3 files changed, 5 insertions(+), 9 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
index 7e170b34..cb9427d5 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala
@@ -42,8 +42,6 @@ trait ManagesLeaf {
   def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit
   def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit
 
-  def addCodeAction(first: Boolean)(vs: Seq[CodeAction])
-
   def getInFuture[T](f: => T): Future[T]
 }
 
diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
index d1d20d73..001266b5 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala
@@ -141,9 +141,6 @@ trait ProjectManager extends ProjectAware {
     })
     grouped foreach (g => toC(g._1)(g._2))
   }
-  def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit =
-    addBtf(uri => getInProject(uri).addCodeAction(first), vs)
-
   override def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit =
     addBtf(uri => getInProject(uri).addCodeAction(first), vs)
 
diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
index b65bc96f..796077a5 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -8,26 +8,27 @@ package viper.server.frontends.lsp.file
 
 import ch.qos.logback.classic.Logger
 import viper.server.frontends.lsp
+
 import scala.concurrent.Future
 import viper.server.core.ViperBackendConfig
 import viper.server.vsi.{AstJobId, VerJobId}
+
 import scala.concurrent.ExecutionContext
 import akka.actor.Props
-
 import viper.server.frontends.lsp.VerificationSuccess._
 import viper.server.frontends.lsp.VerificationState._
-
 import viper.silver.verifier.AbstractError
+
 import scala.collection.mutable.HashSet
 import viper.silver.ast.AbstractSourcePosition
 import org.eclipse.lsp4j.Range
 import org.eclipse.lsp4j
-import viper.silver.ast.utility.lsp.{CodeLens, RangePosition}
+import viper.server.frontends.lsp.{InferenceResult, InferenceResultParams}
+import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
 import viper.silicon.interfaces._
 import viper.silver.verifier._
-import viper.silicon.verifier.Verifier
 
 case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) {
   private var waitingOn: Option[Either[AstJobId, VerJobId]] = None