From 4c5b433bb317e1cc66fd94dc67c75dede5569b99 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Fri, 6 Dec 2024 13:19:35 +0100
Subject: [PATCH 01/15] Add some debug stuff

---
 carbon                                                    | 2 +-
 silicon                                                   | 2 +-
 src/main/scala/viper/server/core/VerificationWorker.scala | 6 +++++-
 3 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/carbon b/carbon
index 2da52018..33e5d5d6 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 2da52018ead6e1f17fb1c67adc65ecdd4ff6c155
+Subproject commit 33e5d5d65f18ab8cc8d10ae4241fab2c2f0d57fc
diff --git a/silicon b/silicon
index 2257d9c0..448775ec 160000
--- a/silicon
+++ b/silicon
@@ -1 +1 @@
-Subproject commit 2257d9c029d368629ed1f831c3c959713b1d1d10
+Subproject commit 448775ec40c6413811f6c3ac1095e22bd227f7e6
diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala
index 1b6b0bfa..31db037a 100644
--- a/src/main/scala/viper/server/core/VerificationWorker.scala
+++ b/src/main/scala/viper/server/core/VerificationWorker.scala
@@ -127,6 +127,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
   /** Run the backend verification functionality */
   def execute(args: Seq[String]): Unit = {
     initialize(args)
+//    println(_ast.printAll());
 
     /**
       * the architecture is as follows:
@@ -215,8 +216,11 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
       return CachingResult(input, Seq.empty)
     }
 
+    println("Before");
+    input.methods.foreach(m => println(m.body.isDefined));
     val (transformed_prog, cached_results) = ViperCache.applyCache(backendName, programId, input)
-
+    println("After");
+    transformed_prog.methods.foreach(m => println(m.body.isDefined));
     // collect and report errors
     val all_cached_errors: collection.mutable.ListBuffer[VerificationError] = ListBuffer()
     cached_results.foreach((result: CacheResult) => {

From bac074f2de9f53a2e62392c1ae82c60629804e61 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Fri, 6 Dec 2024 13:54:22 +0100
Subject: [PATCH 02/15] more

---
 .../scala/viper/server/core/VerificationWorker.scala   |  4 ----
 src/main/scala/viper/server/core/ViperCoreServer.scala | 10 ++++++++--
 .../viper/server/frontends/lsp/ClientCoordinator.scala |  4 ++--
 .../viper/server/frontends/lsp/DataProtocol.scala      |  1 +
 .../scala/viper/server/frontends/lsp/FileManager.scala |  4 ++--
 .../scala/viper/server/frontends/lsp/Receiver.scala    |  3 ++-
 .../server/frontends/lsp/ViperServerService.scala      |  4 ++--
 7 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala
index 31db037a..027d182d 100644
--- a/src/main/scala/viper/server/core/VerificationWorker.scala
+++ b/src/main/scala/viper/server/core/VerificationWorker.scala
@@ -216,11 +216,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
       return CachingResult(input, Seq.empty)
     }
 
-    println("Before");
-    input.methods.foreach(m => println(m.body.isDefined));
     val (transformed_prog, cached_results) = ViperCache.applyCache(backendName, programId, input)
-    println("After");
-    transformed_prog.methods.foreach(m => println(m.body.isDefined));
     // collect and report errors
     val all_cached_errors: collection.mutable.ListBuffer[VerificationError] = ListBuffer()
     cached_results.foreach((result: CacheResult) => {
diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index 52dae503..c8e55d3e 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -73,7 +73,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     ast_id
   }
 
-  def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None): VerJobId = {
+  def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None, verifyTarget: Option[String] = None): VerJobId = {
     val logger = combineLoggers(localLogger)
 
     if (!isRunning) throw new IllegalStateException("Instance of VerificationServer already stopped")
@@ -86,7 +86,13 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
         val task_backend_maybe_fut: Future[Option[VerificationWorker]] =
           handle_future.map((handle: AstHandle[Option[Program]]) => {
             val program_maybe_fut: Future[Option[Program]] = handle.artifact
-            program_maybe_fut.map(_.map(new VerificationWorker(args, programId, _, logger, config)(executor))).recover({
+            program_maybe_fut.map(_.map(p => {
+              val updated = verifyTarget match {
+                case Some(t) => p.copy(methods = Seq())(p.pos, p.info, p.errT)
+                case None => p
+              }
+              new VerificationWorker(args, programId, updated, logger, config)(executor)
+            })).recover({
               case e: Throwable =>
                 logger.error(s"### An exception has occurred while constructing Viper AST: $e")
                 throw e
diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index 5e9c3fbf..9ef85cb2 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -139,9 +139,9 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   }
 
   /** returns true if verification was started */
-  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean): Boolean = {
+  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean, verifyTarget: Option[String]): Boolean = {
     Option(_files.get(uri))
-      .exists(fm => fm.startVerification(backendClassName, customArgs, manuallyTriggered))
+      .exists(fm => fm.startVerification(backendClassName, customArgs, manuallyTriggered, verifyTarget))
   }
 
   /** flushes verification cache, optionally only for a particular file */
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index be00e4f9..b443530f 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -84,6 +84,7 @@ case class VerifyParams (
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
+              verifyTarget: Option[String],       // A specfic target that should be verified, instead of the whole file.
               customArgs: String)            // contains the path of the file that should be verified
 
 case class SettingsError (errorType: SettingsErrorType, msg: String)
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
index 598e2338..98d5c2d3 100644
--- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -104,7 +104,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
     s"$backendClassName $customArgs"
   }
 
-  def startVerification(backendClassName: String, customArgs: String, manuallyTriggered: Boolean): Boolean = {
+  def startVerification(backendClassName: String, customArgs: String, manuallyTriggered: Boolean, verifyTarget: Option[String]): Boolean = {
     prepareVerification()
     this.manuallyTriggered = manuallyTriggered
 
@@ -115,7 +115,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
 
     val command = getVerificationCommand(backendClassName, customArgs)
     coordinator.logger.debug(s"verification command: $command")
-    val handle = coordinator.server.verifyWithCommand(command, Some(coordinator.localLogger))
+    val handle = coordinator.server.verifyWithCommand(command, Some(coordinator.localLogger), verifyTarget)
     jid = handle.id
     if (jid >= 0) {
       coordinator.server.startStreaming(handle, RelayActor.props(this, backendClassName), Some(coordinator.localLogger))
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 4501cd12..08ed0f68 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -177,7 +177,8 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
       coordinator.stopAllRunningVerifications().map(_ => {
         coordinator.logger.info("start or restart verification")
 
-        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered)
+        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, data.verifyTarget)
+//        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, None)
         if (verificationStarted) {
           coordinator.logger.info("Verification Started")
         } else {
diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
index 6b179eca..bae45743 100644
--- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
@@ -23,7 +23,7 @@ import scala.concurrent.duration._
 class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext)
   extends ViperCoreServer(config)(executor) with DefaultVerificationServerStart {
 
-  def verifyWithCommand(command: String, localLogger: Option[Logger] = None): VerJobId = {
+  def verifyWithCommand(command: String, localLogger: Option[Logger] = None, verifyTarget: Option[String]): VerJobId = {
     val logger = combineLoggers(localLogger)
     logger.debug("Requesting ViperServer to start new job...")
 
@@ -47,7 +47,7 @@ class ViperServerService(config: ViperConfig)(override implicit val executor: Ve
         return VerJobId(-1)
     }
 
-    val ver_id = verifyWithAstJob(file, ast_id, backend, localLogger)
+    val ver_id = verifyWithAstJob(file, ast_id, backend, localLogger, verifyTarget)
     if (ver_id.id >= 0) {
       logger.info(s"Verification process #${ver_id.id} has successfully started.")
     } else {

From 2de38dce833788b436cf11897fd4534c3317b269 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Fri, 6 Dec 2024 16:04:43 +0100
Subject: [PATCH 03/15] Finish

---
 src/main/scala/viper/server/core/ViperCoreServer.scala   | 9 ++++++++-
 src/main/scala/viper/server/frontends/lsp/Receiver.scala | 2 +-
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index c8e55d3e..d5a2326e 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -88,7 +88,14 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
             val program_maybe_fut: Future[Option[Program]] = handle.artifact
             program_maybe_fut.map(_.map(p => {
               val updated = verifyTarget match {
-                case Some(t) => p.copy(methods = Seq())(p.pos, p.info, p.errT)
+                // Make all methods abstract except for the selected method.
+                case Some(t) => p.copy(methods = p.methods.map(m => {
+                  if (m.name == t) {
+                    m
+                  } else {
+                    m.copy(body = None)(m.pos, m.info, m.errT)
+                  }
+                }))(p.pos, p.info, p.errT)
                 case None => p
               }
               new VerificationWorker(args, programId, updated, logger, config)(executor)
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 08ed0f68..64bef8eb 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -177,7 +177,7 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
       coordinator.stopAllRunningVerifications().map(_ => {
         coordinator.logger.info("start or restart verification")
 
-        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, data.verifyTarget)
+        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, Some("test2"))
 //        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, None)
         if (verificationStarted) {
           coordinator.logger.info("Verification Started")

From 4923bc18ee43f561d500c92eedf3504afa69b9c8 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Sat, 7 Dec 2024 14:46:52 +0100
Subject: [PATCH 04/15] Add GetDefinitions

---
 .../server/frontends/lsp/ClientCoordinator.scala |  5 ++++-
 .../server/frontends/lsp/CommandProtocol.scala   |  1 +
 .../server/frontends/lsp/DataProtocol.scala      |  4 ++++
 .../viper/server/frontends/lsp/FileManager.scala |  4 +++-
 .../viper/server/frontends/lsp/Receiver.scala    | 16 +++++++++++-----
 5 files changed, 23 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index 9ef85cb2..7fdf815e 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -80,7 +80,10 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
 
   def getSymbolsForFile(uri: String): Array[DocumentSymbol]= {
     Option(_files.get(uri))
-      .map(fm => fm.symbolInformation.toArray)
+      .map(fm => {
+        println("getting symbols for " + uri + ", fm " + fm.hashCode());
+        fm.symbolInformation.toArray
+      })
       .getOrElse(Array.empty)
   }
 
diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
index e0a2e674..64f96b0c 100644
--- a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
@@ -20,6 +20,7 @@ object C2S_Commands {
   // final val ShowHeap = "ShowHeap"
   // final val GetExecutionTrace = "GetExecutionTrace"
   final val RemoveDiagnostics = "RemoveDiagnostics"
+  final val GetDefinitions = "GetDefinitions"
   final val GetViperFileEndings = "GetViperFileEndings"
   final val FlushCache = "FlushCache"
   final val GetIdentifier = "GetIdentifier"
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index b443530f..cef357e6 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -179,6 +179,10 @@ case class StopVerificationResponse(success: Boolean)
 
 case class GetLanguageServerUrlResponse(url: String)
 
+case class GetDefinitionsRequest(uri: String)
+
+case class GetDefinitionsResponse(definitions: Array[Definition])
+
 case class RemoveDiagnosticsRequest(uri: String)
 
 case class RemoveDiagnosticsResponse(success: Boolean)
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
index 98d5c2d3..920f6965 100644
--- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -27,6 +27,7 @@ import scala.concurrent.Future
 
 class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit executor: VerificationExecutionContext) {
   // File information
+  println("creating new file manager for " + file_uri);
   var uri: URI = URI.create(file_uri)
   var path: Path = Paths.get(uri)
   var filename: String = path.getFileName.toString
@@ -157,7 +158,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
         coordinator.logger.debug(s"ignoring message because we are aborting: $m")
 
       case ProgramOutlineReport(members) =>
-        symbolInformation = ArrayBuffer()
+//        symbolInformation = ArrayBuffer()
         members.foreach(m => {
           val member_start = m.pos.asInstanceOf[SourcePosition].start
           val member_end = m.pos.asInstanceOf[SourcePosition].end.getOrElse(member_start)
@@ -175,6 +176,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
           }
           // for now, we use `range` as range & selectionRange. The latter one is supposed to be only a sub-range
           // that should be selected when the user selects the symbol.
+          println("appending symbol for " + file_uri + ", fm " + task.hashCode());
           val info = new DocumentSymbol(m.name, kind, range, range)
           symbolInformation.append(info)
         })
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 64bef8eb..5e86b9b1 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -37,11 +37,13 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("initialized")
   def onInitialized(@unused params: InitializedParams): Unit = {
+    println("initialized");
     coordinator.logger.info("initialized")
   }
 
   @JsonNotification("textDocument/didOpen")
   def onDidOpenDocument(params: DidOpenTextDocumentParams): Unit = {
+    println("opened file");
     val uri: String = params.getTextDocument.getUri
     coordinator.logger.info(s"On opening document $uri")
     try {
@@ -61,6 +63,7 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("textDocument/didChange")
   def onDidChangeDocument(params: DidChangeTextDocumentParams): Unit = {
+    println("on change document!");
     coordinator.logger.info("On changing document")
     coordinator.resetFile(params.getTextDocument.getUri)
   }
@@ -73,6 +76,7 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("textDocument/didSave")
   def onDidSaveDocument(params: DidSaveTextDocumentParams): Unit = {
+    println("on save!");
     coordinator.logger.info("On saving document")
     coordinator.resetFile(params.getTextDocument.getUri)
   }
@@ -162,16 +166,18 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
     CompletableFuture.completedFuture(RemoveDiagnosticsResponse(true))
   }
 
-  @JsonRequest(C2S_Commands.GetLanguageServerUrl)
-  def onGetServerUrl(): CompletionStage[GetLanguageServerUrlResponse] = {
-    coordinator.logger.debug("On getting server URL")
-    CompletableFuture.completedFuture(GetLanguageServerUrlResponse(serverUrl))
+  @JsonRequest(C2S_Commands.GetDefinitions)
+  def onGetDefinitions(request: GetDefinitionsRequest): CompletionStage[GetDefinitionsResponse] = {
+    coordinator.logger.debug("On getting definitions")
+    CompletableFuture.completedFuture(GetDefinitionsResponse(coordinator.getDefinitionsForFile(request.uri).toArray))
   }
 
   @JsonNotification(C2S_Commands.Verify)
   def onVerify(data: VerifyParams): Unit = {
-    coordinator.logger.debug("On verifying")
+    coordinator.logger.debug("On verifying");
+    println("Symbols: " + coordinator.getSymbolsForFile(data.uri).length);
     if (coordinator.canVerificationBeStarted(data.uri, 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")
       coordinator.stopAllRunningVerifications().map(_ => {

From 382fc0c7db95525306921e1d294d679cfad461a3 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Sun, 8 Dec 2024 10:56:01 +0100
Subject: [PATCH 05/15] Add functions to the filter

---
 .../viper/server/core/ViperCoreServer.scala   | 26 +++++++++++++------
 .../server/frontends/lsp/FileManager.scala    |  2 --
 .../viper/server/frontends/lsp/Receiver.scala |  1 -
 3 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index d5a2326e..01d0dc1c 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -88,14 +88,24 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
             val program_maybe_fut: Future[Option[Program]] = handle.artifact
             program_maybe_fut.map(_.map(p => {
               val updated = verifyTarget match {
-                // Make all methods abstract except for the selected method.
-                case Some(t) => p.copy(methods = p.methods.map(m => {
-                  if (m.name == t) {
-                    m
-                  } else {
-                    m.copy(body = None)(m.pos, m.info, m.errT)
-                  }
-                }))(p.pos, p.info, p.errT)
+                // Make all methods and functions abstract except for the selected method.
+                case Some(t) => {
+                  val methods = p.methods.map(m => {
+                    if (m.name == t) {
+                      m
+                    } else {
+                      m.copy(body = None)(m.pos, m.info, m.errT)
+                    }
+                  });
+                  val functions = p.functions.map(m => {
+                    if (m.name == t) {
+                      m
+                    } else {
+                      m.copy(body = None)(m.pos, m.info, m.errT)
+                    }
+                  })
+                  p.copy(methods = methods, functions = functions)(p.pos, p.info, p.errT)
+                }
                 case None => p
               }
               new VerificationWorker(args, programId, updated, logger, config)(executor)
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
index 920f6965..ea7611ef 100644
--- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -158,7 +158,6 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
         coordinator.logger.debug(s"ignoring message because we are aborting: $m")
 
       case ProgramOutlineReport(members) =>
-//        symbolInformation = ArrayBuffer()
         members.foreach(m => {
           val member_start = m.pos.asInstanceOf[SourcePosition].start
           val member_end = m.pos.asInstanceOf[SourcePosition].end.getOrElse(member_start)
@@ -176,7 +175,6 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
           }
           // for now, we use `range` as range & selectionRange. The latter one is supposed to be only a sub-range
           // that should be selected when the user selects the symbol.
-          println("appending symbol for " + file_uri + ", fm " + task.hashCode());
           val info = new DocumentSymbol(m.name, kind, range, range)
           symbolInformation.append(info)
         })
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 5e86b9b1..dec565a2 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -175,7 +175,6 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
   @JsonNotification(C2S_Commands.Verify)
   def onVerify(data: VerifyParams): Unit = {
     coordinator.logger.debug("On verifying");
-    println("Symbols: " + coordinator.getSymbolsForFile(data.uri).length);
     if (coordinator.canVerificationBeStarted(data.uri, data.manuallyTriggered)) {
 
       // stop all other verifications because the backend crashes if multiple verifications are run in parallel

From 662671f10e2402e18baf05e558fa610f7c87e9dd Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Mon, 9 Dec 2024 19:45:10 +0100
Subject: [PATCH 06/15] don't take option string for verify target

---
 .../scala/viper/server/frontends/lsp/DataProtocol.scala    | 2 +-
 .../scala/viper/server/frontends/lsp/FileManager.scala     | 1 -
 src/main/scala/viper/server/frontends/lsp/Receiver.scala   | 7 +++----
 3 files changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index cef357e6..dbb12082 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -84,7 +84,7 @@ case class VerifyParams (
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
-              verifyTarget: Option[String],       // A specfic target that should be verified, instead of the whole file.
+              verifyTarget: String,       // A specfic target that should be verified, instead of the whole file.
               customArgs: String)            // contains the path of the file that should be verified
 
 case class SettingsError (errorType: SettingsErrorType, msg: String)
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
index ea7611ef..cddc0273 100644
--- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -27,7 +27,6 @@ import scala.concurrent.Future
 
 class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit executor: VerificationExecutionContext) {
   // File information
-  println("creating new file manager for " + file_uri);
   var uri: URI = URI.create(file_uri)
   var path: Path = Paths.get(uri)
   var filename: String = path.getFileName.toString
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index dec565a2..ccbef029 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -43,7 +43,6 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("textDocument/didOpen")
   def onDidOpenDocument(params: DidOpenTextDocumentParams): Unit = {
-    println("opened file");
     val uri: String = params.getTextDocument.getUri
     coordinator.logger.info(s"On opening document $uri")
     try {
@@ -76,7 +75,6 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("textDocument/didSave")
   def onDidSaveDocument(params: DidSaveTextDocumentParams): Unit = {
-    println("on save!");
     coordinator.logger.info("On saving document")
     coordinator.resetFile(params.getTextDocument.getUri)
   }
@@ -182,8 +180,9 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
       coordinator.stopAllRunningVerifications().map(_ => {
         coordinator.logger.info("start or restart verification")
 
-        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, Some("test2"))
-//        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, None)
+        val verifyTarget = if(data.verifyTarget == null || data.verifyTarget.isEmpty) None else Some(data.verifyTarget)
+
+        val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, verifyTarget)
         if (verificationStarted) {
           coordinator.logger.info("Verification Started")
         } else {

From 3e33d804c3c46b9bf5f8ec63b86ad8102f4d4a6c Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Fri, 13 Dec 2024 13:00:51 +0100
Subject: [PATCH 07/15] Form the transitive closure when verifiying a specific
 method/function

---
 carbon                                        |  2 +-
 .../viper/server/core/ViperCoreServer.scala   | 36 +++++++++++--------
 .../viper/server/frontends/lsp/Receiver.scala |  1 -
 3 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/carbon b/carbon
index 33e5d5d6..a46ac124 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 33e5d5d65f18ab8cc8d10ae4241fab2c2f0d57fc
+Subproject commit a46ac124fd74d3f9de281f9c20ca9c46ac04433b
diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index 01d0dc1c..26984bd7 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -12,9 +12,10 @@ import akka.util.Timeout
 import ch.qos.logback.classic.Logger
 import viper.server.ViperConfig
 import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer}
-import viper.silver.ast.Program
+import viper.silver.ast.{Method, Node, Program, Function}
 import viper.silver.logger.ViperLogger
 
+import scala.collection.immutable.HashSet
 import scala.concurrent.duration._
 import scala.concurrent.Future
 import scala.language.postfixOps
@@ -87,24 +88,31 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
           handle_future.map((handle: AstHandle[Option[Program]]) => {
             val program_maybe_fut: Future[Option[Program]] = handle.artifact
             program_maybe_fut.map(_.map(p => {
-              val updated = verifyTarget match {
-                // Make all methods and functions abstract except for the selected method.
-                case Some(t) => {
-                  val methods = p.methods.map(m => {
-                    if (m.name == t) {
-                      m
-                    } else {
-                      m.copy(body = None)(m.pos, m.info, m.errT)
-                    }
-                  });
-                  val functions = p.functions.map(m => {
-                    if (m.name == t) {
+              val updated = verifyTarget.flatMap(t => {
+                val m: Option[Node] = p.findMethodOptionally(t).orElse(p.findFunctionOptionally(t))
+                if (m.isEmpty) {
+                  logger.warn(s"Tried to verify ${t}, but not method or function with that name exists. Falling back to verifying the whole file instead.")
+                }
+                // TODO: Send some kind of error instead?
+                m
+              }) match {
+                // Make all other methods abstract and remove unused parts of the program.
+                case Some(root) => {
+                  val deps = HashSet() ++ (root match {
+                    case m: Method => p.getMethodDependenciesWithMethods(p, m)
+                    case f: Function => p.getFunctionDependencies(p, f)
+                  })
+                  val functions = p.functions.filter(deps.contains(_))
+                  val predicates = p.predicates.filter(deps.contains(_))
+                  // For methods, we additionally make them abstract if they are not the target method
+                  val methods = p.methods.filter(deps.contains(_)).map(m => {
+                    if (m == root) {
                       m
                     } else {
                       m.copy(body = None)(m.pos, m.info, m.errT)
                     }
                   })
-                  p.copy(methods = methods, functions = functions)(p.pos, p.info, p.errT)
+                  p.copy(methods = methods, functions = functions, predicates = predicates)(p.pos, p.info, p.errT)
                 }
                 case None => p
               }
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index ccbef029..e9048c94 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -62,7 +62,6 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("textDocument/didChange")
   def onDidChangeDocument(params: DidChangeTextDocumentParams): Unit = {
-    println("on change document!");
     coordinator.logger.info("On changing document")
     coordinator.resetFile(params.getTextDocument.getUri)
   }

From bf70825668ff43c99f05a3e1b24b6e081c1af923 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Fri, 13 Dec 2024 13:15:26 +0100
Subject: [PATCH 08/15] Throw runtime exception for now

---
 src/main/scala/viper/server/core/ViperCoreServer.scala | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index 26984bd7..556b59a5 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -91,7 +91,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
               val updated = verifyTarget.flatMap(t => {
                 val m: Option[Node] = p.findMethodOptionally(t).orElse(p.findFunctionOptionally(t))
                 if (m.isEmpty) {
-                  logger.warn(s"Tried to verify ${t}, but not method or function with that name exists. Falling back to verifying the whole file instead.")
+                  throw new RuntimeException("Tried to verify ${t}, but not method or function with that name exists.")
                 }
                 // TODO: Send some kind of error instead?
                 m

From 744a89fe79f7feb915bc36e7ae76beadba71a193 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Mon, 20 Jan 2025 20:23:58 +0100
Subject: [PATCH 09/15] Add verification of a specific target

---
 carbon                                        |  2 +-
 .../server/core/VerificationWorker.scala      | 15 +++++++
 .../viper/server/core/ViperCoreServer.scala   | 40 +++++++++++--------
 .../frontends/lsp/ClientCoordinator.scala     |  3 +-
 .../server/frontends/lsp/DataProtocol.scala   |  6 ++-
 .../server/frontends/lsp/FileManager.scala    | 20 ++++++++--
 .../viper/server/frontends/lsp/Receiver.scala |  3 +-
 .../frontends/lsp/ViperServerService.scala    |  3 +-
 8 files changed, 68 insertions(+), 24 deletions(-)

diff --git a/carbon b/carbon
index a46ac124..a5b12fe5 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit a46ac124fd74d3f9de281f9c20ca9c46ac04433b
+Subproject commit a5b12fe56746404fe7f11bc1b5dbcfb50d6eae14
diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala
index 027d182d..c9acc721 100644
--- a/src/main/scala/viper/server/core/VerificationWorker.scala
+++ b/src/main/scala/viper/server/core/VerificationWorker.scala
@@ -32,6 +32,9 @@ case class ViperEnvelope(m: Message) extends Envelope
 class VerificationWorker(private val command: List[String],
                          private val programId: String,
                          private val program: Program,
+                         // Does the verification process target the whole file,
+                         // or just a specific function/method at a specific location?
+                         private val target: Option[SourcePosition],
                          override val logger: Logger,
                          private val config: ViperConfig)
                         (override val executor: VerificationExecutionContext)
@@ -106,6 +109,18 @@ class VerificationWorker(private val command: List[String],
     backend.mapEntityVerificationResult(entity, result)
   }
 
+  override def registerTaskEnd(success: Boolean): Unit = {
+    // We need to enqueue the message here instead of doing it in the constructor
+    // of the verification worker, because at that point the task hasn't been created yet,
+    // and thus the message cant be sent.
+    target match {
+      case Some(t) => enqueueMessage(TargetSelectionReport(t))
+      case _ =>
+    }
+
+    super.registerTaskEnd(success);
+  }
+
   override def call(): Unit = run()
 }
 
diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index 556b59a5..0dc426c5 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -12,7 +12,7 @@ import akka.util.Timeout
 import ch.qos.logback.classic.Logger
 import viper.server.ViperConfig
 import viper.server.vsi.{AstHandle, AstJobId, VerJobId, VerificationServer}
-import viper.silver.ast.{Method, Node, Program, Function}
+import viper.silver.ast.{Function, HasLineColumn, Method, Node, Program, SourcePosition}
 import viper.silver.logger.ViperLogger
 
 import scala.collection.immutable.HashSet
@@ -74,7 +74,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     ast_id
   }
 
-  def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None, verifyTarget: Option[String] = None): VerJobId = {
+  def verifyWithAstJob(programId: String, ast_id: AstJobId, backend_config: ViperBackendConfig, localLogger: Option[Logger] = None, verifyTarget: Option[HasLineColumn] = None): VerJobId = {
     val logger = combineLoggers(localLogger)
 
     if (!isRunning) throw new IllegalStateException("Instance of VerificationServer already stopped")
@@ -88,17 +88,21 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
           handle_future.map((handle: AstHandle[Option[Program]]) => {
             val program_maybe_fut: Future[Option[Program]] = handle.artifact
             program_maybe_fut.map(_.map(p => {
-              val updated = verifyTarget.flatMap(t => {
-                val m: Option[Node] = p.findMethodOptionally(t).orElse(p.findFunctionOptionally(t))
-                if (m.isEmpty) {
-                  throw new RuntimeException("Tried to verify ${t}, but not method or function with that name exists.")
-                }
-                // TODO: Send some kind of error instead?
-                m
-              }) match {
+              val target: Option[(Node, SourcePosition)] = verifyTarget.flatMap(pos => {
+                (p.methods ++ p.functions).collectFirst(m =>  m.pos match {
+                  case p: SourcePosition  if p.start <= pos && p.end.getOrElse(p.start)  >= pos => (m, p)
+                })
+              });
+
+              if (!verifyTarget.isEmpty && target.isEmpty) {
+                logger.warn(s"Tried to verify target at position ${verifyTarget.get}, " +
+                  s"but no method or function exists at that position.")
+              }
+
+              val (updated_program, position) = target match {
                 // Make all other methods abstract and remove unused parts of the program.
                 case Some(root) => {
-                  val deps = HashSet() ++ (root match {
+                  val deps = HashSet() ++ (root._1 match {
                     case m: Method => p.getMethodDependenciesWithMethods(p, m)
                     case f: Function => p.getFunctionDependencies(p, f)
                   })
@@ -106,17 +110,21 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
                   val predicates = p.predicates.filter(deps.contains(_))
                   // For methods, we additionally make them abstract if they are not the target method
                   val methods = p.methods.filter(deps.contains(_)).map(m => {
-                    if (m == root) {
+                    if (m == root._1) {
                       m
                     } else {
                       m.copy(body = None)(m.pos, m.info, m.errT)
                     }
                   })
-                  p.copy(methods = methods, functions = functions, predicates = predicates)(p.pos, p.info, p.errT)
+                  (p.copy(methods = methods, functions = functions, predicates = predicates)(p.pos, p.info, p.errT), Some(root._2))
                 }
-                case None => p
+
+                case None => (p, None)
               }
-              new VerificationWorker(args, programId, updated, logger, config)(executor)
+
+              val worker = new VerificationWorker(args, programId, updated_program, position, logger, config)(executor)
+
+              worker
             })).recover({
               case e: Throwable =>
                 logger.error(s"### An exception has occurred while constructing Viper AST: $e")
@@ -142,7 +150,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
     val logger = combineLoggers(localLogger)
 
     val args: List[String] = backend_config.toList
-    val task_backend = new VerificationWorker(args, programId, program, logger, config)(executor)
+    val task_backend = new VerificationWorker(args, programId, program, None, logger, config)(executor)
     val ver_id = initializeVerificationProcess(Future.successful(Some(task_backend)), None)
 
     if (ver_id.id >= 0) {
diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index 7fdf815e..bdd09f74 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -10,6 +10,7 @@ import ch.qos.logback.classic.Logger
 import org.eclipse.lsp4j.DocumentSymbol
 import viper.server.core.VerificationExecutionContext
 import viper.server.frontends.lsp.VerificationState.Ready
+import viper.silver.ast.HasLineColumn
 
 import java.util.concurrent.{ConcurrentHashMap, ConcurrentMap}
 import scala.collection.mutable.ArrayBuffer
@@ -142,7 +143,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
   }
 
   /** returns true if verification was started */
-  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean, verifyTarget: Option[String]): Boolean = {
+  def startVerification(backendClassName: String, customArgs: String, uri: String, manuallyTriggered: Boolean, verifyTarget: Option[HasLineColumn] = None): Boolean = {
     Option(_files.get(uri))
       .exists(fm => fm.startVerification(backendClassName, customArgs, manuallyTriggered, verifyTarget))
   }
diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
index dbb12082..c46680e4 100644
--- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala
@@ -84,7 +84,8 @@ case class VerifyParams (
               manuallyTriggered: Boolean,   // was the verification triggered manually
               workspace: String,            // the path to the open workspace folder
               backend: String,
-              verifyTarget: String,       // A specfic target that should be verified, instead of the whole file.
+              verifyTarget: Position,       // A specific method/function at a position that should be verified,
+                                            // instead of the whole file.
               customArgs: String)            // contains the path of the file that should be verified
 
 case class SettingsError (errorType: SettingsErrorType, msg: String)
@@ -155,6 +156,9 @@ case class StateChangeParams(
               success: Int = NA.id,
               verificationCompleted: Double = -1,
               manuallyTriggered: Double = -1,
+              // The range of the source code that is currently being verified, if for example
+              // a specific method/function is verified instead of the whole file.
+              currentTarget: Range = null,
               filename: String = null,
               backendName: String = null,
               time: Double = -1, /** [sec] */
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
index cddc0273..28213af8 100644
--- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -37,6 +37,9 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
   var is_aborting: Boolean = false
   var is_verifying: Boolean = false
   var global_failure: Boolean = false
+  // The range of the function/method we are currently verifying, if we are verifying a specific
+  // target instead of the whole file.
+  var currentTarget: Option[SourcePosition] = None
   var state: VerificationState = Stopped
   var manuallyTriggered: Boolean = _
 
@@ -67,6 +70,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
   def prepareVerification(): Unit = {
     is_verifying = true
     is_aborting = false
+    currentTarget = None
     state = Stopped
     if (partialData.nonEmpty) {
       coordinator.logger.debug(s"Some unparsed output has been detected: $partialData")
@@ -104,7 +108,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
     s"$backendClassName $customArgs"
   }
 
-  def startVerification(backendClassName: String, customArgs: String, manuallyTriggered: Boolean, verifyTarget: Option[String]): Boolean = {
+  def startVerification(backendClassName: String, customArgs: String, manuallyTriggered: Boolean, verifyTarget: Option[HasLineColumn] = None): Boolean = {
     prepareVerification()
     this.manuallyTriggered = manuallyTriggered
 
@@ -219,6 +223,9 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
       case WarningsDuringVerification(warnings) =>
         markErrorsAsReported(warnings)
         processErrors(backendClassName, warnings)
+      case TargetSelectionReport(ts) => {
+        currentTarget = Some(ts)
+      }
       case EntitySuccessMessage(_, concerning, _, _) =>
         if (progress == null) {
           coordinator.logger.debug("The backend must send a VerificationStart message before the ...Verified message.")
@@ -341,6 +348,13 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
       var success = NA
       val mt = if (this.manuallyTriggered) 1 else 0
 
+      val target = currentTarget.map(p => {
+        val start = p.start
+        val end = p.end.getOrElse(p.start)
+
+        new Range(new Position(start.line - 1, start.column - 1), new Position(end.line - 1, end.column - 1))
+      }).getOrElse(null)
+
       val isVerifyingStage = true
 
       // do we need to start a followUp Stage?
@@ -356,7 +370,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
         coordinator.sendStateChangeNotification(params, Some(this))
 
         // notify client about outcome of verification
-        params = StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+        params = StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt, currentTarget=target,
           filename = filename, time = timeMs.toDouble / 1000, verificationCompleted = 1, uri = file_uri,
           error = internalErrorMessage, diagnostics = diagnostics.toArray)
         coordinator.sendStateChangeNotification(params, Some(this))
@@ -366,7 +380,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
         }
       } else {
         success = if (is_aborting) Aborted else Success
-        params = StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+        params = StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt, currentTarget=target,
           filename = filename, time = timeMs.toDouble / 1000, verificationCompleted = 0, uri = file_uri,
           error = internalErrorMessage, diagnostics = diagnostics.toArray)
         coordinator.sendStateChangeNotification(params, Some(this))
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index e9048c94..76af1a69 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -12,6 +12,7 @@ import org.eclipse.lsp4j.services.{LanguageClient, LanguageClientAware}
 import org.eclipse.lsp4j.{DidChangeConfigurationParams, DidChangeTextDocumentParams, DidChangeWatchedFilesParams, DidCloseTextDocumentParams, DidOpenTextDocumentParams, DidSaveTextDocumentParams, InitializeParams, InitializeResult, InitializedParams, ServerCapabilities, TextDocumentSyncKind}
 import viper.server.ViperConfig
 import viper.server.core.VerificationExecutionContext
+import viper.silver.ast.{LineColumnPosition, SourcePosition}
 import viper.viperserver.BuildInfo
 
 import scala.annotation.unused
@@ -179,7 +180,7 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
       coordinator.stopAllRunningVerifications().map(_ => {
         coordinator.logger.info("start or restart verification")
 
-        val verifyTarget = if(data.verifyTarget == null || data.verifyTarget.isEmpty) None else Some(data.verifyTarget)
+        val verifyTarget = if(data.verifyTarget == null) None else Some(LineColumnPosition(data.verifyTarget.getLine + 1, data.verifyTarget.getCharacter + 1))
 
         val verificationStarted = coordinator.startVerification(data.backend, data.customArgs, data.uri, data.manuallyTriggered, verifyTarget)
         if (verificationStarted) {
diff --git a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
index bae45743..54082ea0 100644
--- a/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ViperServerService.scala
@@ -16,6 +16,7 @@ import viper.server.core.{VerificationExecutionContext, ViperBackendConfig, Vipe
 import viper.server.utility.Helpers.{getArgListFromArgString, validateViperFile}
 import viper.server.vsi.VerificationProtocol.{StopAstConstruction, StopVerification}
 import viper.server.vsi.{AstJobId, DefaultVerificationServerStart, VerHandle, VerJobId}
+import viper.silver.ast.HasLineColumn
 
 import scala.concurrent.Future
 import scala.concurrent.duration._
@@ -23,7 +24,7 @@ import scala.concurrent.duration._
 class ViperServerService(config: ViperConfig)(override implicit val executor: VerificationExecutionContext)
   extends ViperCoreServer(config)(executor) with DefaultVerificationServerStart {
 
-  def verifyWithCommand(command: String, localLogger: Option[Logger] = None, verifyTarget: Option[String]): VerJobId = {
+  def verifyWithCommand(command: String, localLogger: Option[Logger] = None, verifyTarget: Option[HasLineColumn] = None): VerJobId = {
     val logger = combineLoggers(localLogger)
     logger.debug("Requesting ViperServer to start new job...")
 

From 4f48f8ec9e8f68bbeada7c6ef0dd8fcc008de4ab Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Mon, 20 Jan 2025 20:40:37 +0100
Subject: [PATCH 10/15] Remove some unnecessary changes

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

diff --git a/carbon b/carbon
index a5b12fe5..6f77d2d7 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit a5b12fe56746404fe7f11bc1b5dbcfb50d6eae14
+Subproject commit 6f77d2d745c82246b8f9714631193d687d29ba22

From 96c5b9809d266c7dc0eb80ec310d1fa0b6a3dfb6 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Mon, 20 Jan 2025 20:41:23 +0100
Subject: [PATCH 11/15] Remove more

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

diff --git a/carbon b/carbon
index 6f77d2d7..854510c9 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 6f77d2d745c82246b8f9714631193d687d29ba22
+Subproject commit 854510c9a4e66bfbe0f19bfa04eac3973ab439e1

From 4212ede0004c7247ccd19b59f926e9e35b16b6e4 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Mon, 20 Jan 2025 21:23:42 +0100
Subject: [PATCH 12/15] update deps

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

diff --git a/carbon b/carbon
index 854510c9..b50d7a6d 160000
--- a/carbon
+++ b/carbon
@@ -1 +1 @@
-Subproject commit 854510c9a4e66bfbe0f19bfa04eac3973ab439e1
+Subproject commit b50d7a6d90dc7d6e3263f1454f49f55e0a23d5a5

From 032d64c51b1177b6ac2821adf9a91b584a6e489f Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Mon, 20 Jan 2025 21:53:16 +0100
Subject: [PATCH 13/15] revert some unnecessary changes

---
 .../scala/viper/server/core/VerificationWorker.scala     | 2 +-
 src/main/scala/viper/server/core/ViperCoreServer.scala   | 3 ++-
 .../viper/server/frontends/lsp/ClientCoordinator.scala   | 5 +----
 .../viper/server/frontends/lsp/CommandProtocol.scala     | 1 -
 .../scala/viper/server/frontends/lsp/FileManager.scala   | 1 +
 src/main/scala/viper/server/frontends/lsp/Receiver.scala | 9 ++++-----
 6 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala
index c9acc721..235f2b91 100644
--- a/src/main/scala/viper/server/core/VerificationWorker.scala
+++ b/src/main/scala/viper/server/core/VerificationWorker.scala
@@ -142,7 +142,6 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
   /** Run the backend verification functionality */
   def execute(args: Seq[String]): Unit = {
     initialize(args)
-//    println(_ast.printAll());
 
     /**
       * the architecture is as follows:
@@ -232,6 +231,7 @@ class ViperBackend(val backendName: String, private val _frontend: SilFrontend,
     }
 
     val (transformed_prog, cached_results) = ViperCache.applyCache(backendName, programId, input)
+
     // collect and report errors
     val all_cached_errors: collection.mutable.ListBuffer[VerificationError] = ListBuffer()
     cached_results.foreach((result: CacheResult) => {
diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index 0dc426c5..e51f0c65 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -100,7 +100,8 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
               }
 
               val (updated_program, position) = target match {
-                // Make all other methods abstract and remove unused parts of the program.
+                // Remove unused functions, predicates and methods
+                // and make not-targeted methods abstract
                 case Some(root) => {
                   val deps = HashSet() ++ (root._1 match {
                     case m: Method => p.getMethodDependenciesWithMethods(p, m)
diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
index bdd09f74..728771a4 100644
--- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
+++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala
@@ -81,10 +81,7 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif
 
   def getSymbolsForFile(uri: String): Array[DocumentSymbol]= {
     Option(_files.get(uri))
-      .map(fm => {
-        println("getting symbols for " + uri + ", fm " + fm.hashCode());
-        fm.symbolInformation.toArray
-      })
+      .map(fm => fm.symbolInformation.toArray)
       .getOrElse(Array.empty)
   }
 
diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
index 64f96b0c..e0a2e674 100644
--- a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
+++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala
@@ -20,7 +20,6 @@ object C2S_Commands {
   // final val ShowHeap = "ShowHeap"
   // final val GetExecutionTrace = "GetExecutionTrace"
   final val RemoveDiagnostics = "RemoveDiagnostics"
-  final val GetDefinitions = "GetDefinitions"
   final val GetViperFileEndings = "GetViperFileEndings"
   final val FlushCache = "FlushCache"
   final val GetIdentifier = "GetIdentifier"
diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
index 28213af8..c441aadf 100644
--- a/src/main/scala/viper/server/frontends/lsp/FileManager.scala
+++ b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -161,6 +161,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
         coordinator.logger.debug(s"ignoring message because we are aborting: $m")
 
       case ProgramOutlineReport(members) =>
+        symbolInformation = ArrayBuffer()
         members.foreach(m => {
           val member_start = m.pos.asInstanceOf[SourcePosition].start
           val member_end = m.pos.asInstanceOf[SourcePosition].end.getOrElse(member_start)
diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
index 76af1a69..a0a7c254 100644
--- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala
+++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala
@@ -38,7 +38,6 @@ abstract class StandardReceiver(server: ViperServerService)(implicit executor: V
 
   @JsonNotification("initialized")
   def onInitialized(@unused params: InitializedParams): Unit = {
-    println("initialized");
     coordinator.logger.info("initialized")
   }
 
@@ -164,10 +163,10 @@ class CustomReceiver(config: ViperConfig, server: ViperServerService, serverUrl:
     CompletableFuture.completedFuture(RemoveDiagnosticsResponse(true))
   }
 
-  @JsonRequest(C2S_Commands.GetDefinitions)
-  def onGetDefinitions(request: GetDefinitionsRequest): CompletionStage[GetDefinitionsResponse] = {
-    coordinator.logger.debug("On getting definitions")
-    CompletableFuture.completedFuture(GetDefinitionsResponse(coordinator.getDefinitionsForFile(request.uri).toArray))
+  @JsonRequest(C2S_Commands.GetLanguageServerUrl)
+  def onGetServerUrl(): CompletionStage[GetLanguageServerUrlResponse] = {
+    coordinator.logger.debug("On getting server URL")
+    CompletableFuture.completedFuture(GetLanguageServerUrlResponse(serverUrl))
   }
 
   @JsonNotification(C2S_Commands.Verify)

From 49ed35b122c183849ff02e228ee31b9aaaf9ccf2 Mon Sep 17 00:00:00 2001
From: Laurenz Stampfl <laurenz.stampfl+github@gmail.com>
Date: Wed, 12 Feb 2025 09:34:30 +0100
Subject: [PATCH 14/15] Small adjustments

---
 src/main/scala/viper/server/core/VerificationWorker.scala | 3 ++-
 src/main/scala/viper/server/core/ViperCoreServer.scala    | 4 +---
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/server/core/VerificationWorker.scala b/src/main/scala/viper/server/core/VerificationWorker.scala
index 235f2b91..a8a9ee77 100644
--- a/src/main/scala/viper/server/core/VerificationWorker.scala
+++ b/src/main/scala/viper/server/core/VerificationWorker.scala
@@ -110,7 +110,8 @@ class VerificationWorker(private val command: List[String],
   }
 
   override def registerTaskEnd(success: Boolean): Unit = {
-    // We need to enqueue the message here instead of doing it in the constructor
+    // We need to enqueue the message for choosing a specific verification target
+    // in the source code here instead of doing it in the constructor
     // of the verification worker, because at that point the task hasn't been created yet,
     // and thus the message cant be sent.
     target match {
diff --git a/src/main/scala/viper/server/core/ViperCoreServer.scala b/src/main/scala/viper/server/core/ViperCoreServer.scala
index e51f0c65..8fb40522 100644
--- a/src/main/scala/viper/server/core/ViperCoreServer.scala
+++ b/src/main/scala/viper/server/core/ViperCoreServer.scala
@@ -123,9 +123,7 @@ abstract class ViperCoreServer(val config: ViperConfig)(implicit val executor: V
                 case None => (p, None)
               }
 
-              val worker = new VerificationWorker(args, programId, updated_program, position, logger, config)(executor)
-
-              worker
+              new VerificationWorker(args, programId, updated_program, position, logger, config)(executor)
             })).recover({
               case e: Throwable =>
                 logger.error(s"### An exception has occurred while constructing Viper AST: $e")

From 6ffc939cc731362ef9d72808010ad118cd39be5b Mon Sep 17 00:00:00 2001
From: Nicolas Klose <nicolas.klose@inf.ethz.ch>
Date: Tue, 24 Jun 2025 17:19:53 +0200
Subject: [PATCH 15/15] merge fixes

---
 .../server/frontends/lsp/file/RelayActor.scala     | 14 ++++++++++++--
 .../server/frontends/lsp/file/Verification.scala   | 10 ++++++++--
 2 files changed, 20 insertions(+), 4 deletions(-)

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 86fcb4d5..4852bc8b 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala
@@ -7,6 +7,7 @@
 package viper.server.frontends.lsp.file
 
 import akka.actor.{Actor, PoisonPill, Props, Status}
+import org.eclipse.lsp4j.{Diagnostic, DiagnosticSeverity, DocumentSymbol, Position, PublishDiagnosticsParams, Range, SymbolKind}
 import viper.server.frontends.lsp
 import viper.server.frontends.lsp.VerificationState._
 import viper.server.frontends.lsp.VerificationSuccess._
@@ -45,6 +46,13 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
       var success = NA
       val mt = if (this.manuallyTriggered) 1 else 0
 
+      val target = currentTarget.map(p => {
+        val start = p.start
+        val end = p.end.getOrElse(p.start)
+
+        new Range(new Position(start.line - 1, start.column - 1), new Position(end.line - 1, end.column - 1))
+      }).getOrElse(null)
+
       val isVerifyingStage = true
 
       // do we need to start a followUp Stage?
@@ -55,7 +63,7 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
         coordinator.sendStateChangeNotification(params, Some(this))
 
         // notify client about outcome of verification
-        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt, currentTarget=target,
           filename = filename, time = timeMs.toDouble / 1000, verificationCompleted = 1, uri = file_uri,
           error = "")
         coordinator.sendStateChangeNotification(params, Some(this))
@@ -65,7 +73,7 @@ trait MessageHandler extends ProjectManager with VerificationManager with Quanti
         }
       } else {
         success = if (is_aborting) Aborted else Success
-        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt,
+        params = lsp.StateChangeParams(Ready.id, success = success.id, manuallyTriggered = mt, currentTarget=target,
           filename = filename, time = timeMs.toDouble / 1000, verificationCompleted = 0, uri = file_uri,
           error = "")
         coordinator.sendStateChangeNotification(params, Some(this))
@@ -197,6 +205,8 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends
     case WarningsDuringVerification(warnings) =>
       markErrorsAsReported(warnings)
       task.processErrors(backendClassName, warnings)
+    case TargetSelectionReport(ts) =>
+        currentTarget = Some(ts)
     // the completion handler is not yet invoked (but as part of Status.Success)
     case QuantifierChosenTriggersMessage(qexp, triggers, oldTriggers) =>
       coordinator.logger.trace(s"[receive@${task.filename}/${backendClassName.isDefined}] QuantifierChosenTriggersMessage")
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 3d6240d1..0c4b5d49 100644
--- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
+++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala
@@ -25,6 +25,7 @@ import org.eclipse.lsp4j
 import viper.silver.ast.utility.lsp.RangePosition
 import viper.silver.ast.HasLineColumn
 import viper.silver.ast.LineColumnPosition
+import viper.silver.ast.SourcePosition
 
 case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) {
   private var waitingOn: Option[Either[AstJobId, VerJobId]] = None
@@ -131,6 +132,10 @@ trait VerificationManager extends ManagesLeaf {
   var manuallyTriggered: Boolean = _
   var neverParsed: Boolean = true
 
+  // The range of the function/method we are currently verifying, if we are verifying a specific
+  // target instead of the whole file.
+  var currentTarget: Option[SourcePosition] = None
+
   //verification results
   var jid: Int = -1
   var timeMs: Long = 0
@@ -147,6 +152,7 @@ trait VerificationManager extends ManagesLeaf {
 
     is_verifying = true
     is_aborting = false
+    currentTarget = None
     state = Stopped
     neverParsed = false
     timeMs = 0
@@ -201,7 +207,7 @@ trait VerificationManager extends ManagesLeaf {
   }
 
   /** Do full parsing, type checking and verification */
-  def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = {
+  def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean, verifyTarget: Option[HasLineColumn] = None): Future[Boolean] = {
     val command = getVerificationCommand(backendClassName, customArgs)
     val backend = ViperBackendConfig(command);
 
@@ -214,7 +220,7 @@ trait VerificationManager extends ManagesLeaf {
         case None => return Future.successful(false)
         case Some(ast) => ast
       }
-      val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger))
+      val verJob = coordinator.server.verifyAst(astJob, file.toString(), backend, Some(coordinator.localLogger), verifyTarget)
       if (verJob.id >= 0) {
         // Execute all handles
         this.resetContainers(false)