From d32a83648f36a3561001f62278760ac96f5f59f0 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 15 Dec 2025 17:10:02 +0100
Subject: [PATCH 01/27] WIP: pass dependency results to Gobra

---
 src/main/scala/viper/silver/ast/Ast.scala            |  2 ++
 .../silver/ast/utility/rewriter/Rewritable.scala     |  3 ++-
 .../AbstractDependencyGraphInterpreter.scala         |  5 +++++
 .../AbstractReadOnlyDependencyGraph.scala            |  5 +++++
 .../viper/silver/verifier/VerificationError.scala    | 12 ++++++++++++
 5 files changed, 26 insertions(+), 1 deletion(-)
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 304de1bcf..62f8ed73e 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -364,6 +364,8 @@ trait Info {
     case _: T => NoInfo
     case info => info
   }
+
+  def getSourceString: String = ""
 }
 
 /** A default `Info` that is empty. */
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
index 434c2ccf4..b1e450328 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
@@ -7,7 +7,7 @@
 package viper.silver.ast.utility.rewriter
 
 import viper.silver.parser.PNode
-import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position}
+import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, DomainMember, ErrorTrafo, FuncApp, Info, Node, Position}
 
 import scala.reflect.runtime.{universe => reflection}
 
@@ -112,6 +112,7 @@ trait Rewritable extends Product {
       val arguments = this match {
         case fa: FuncApp => this.children ++ Seq(pos, info, fa.typ, trafo)
         case df: DomainFuncApp => this.children ++ Seq(pos, info, df.typ, df.domainName, trafo)
+        case dm: DomainMember => this.children ++ Seq(pos, info, dm.domainName, trafo)
         case _ => this.children ++ Seq(pos, info, trafo)
       }
 
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala b/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala
new file mode 100644
index 000000000..fe906fa8f
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala
@@ -0,0 +1,5 @@
+package viper.silver.dependencyAnalysis
+
+abstract class AbstractDependencyGraphInterpreter {
+
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala b/src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala
new file mode 100644
index 000000000..2d256f377
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala
@@ -0,0 +1,5 @@
+package viper.silver.dependencyAnalysis
+
+trait AbstractReadOnlyDependencyGraph {}
+
+trait AbstractDependencyAnalysisNode {}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 4ee3f6d45..74ccf05c3 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -9,6 +9,7 @@ package viper.silver.verifier
 import fastparse.Parsed
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Rewritable
+import viper.silver.dependencyAnalysis.AbstractDependencyGraphInterpreter
 
 
 /**********************************************************************************
@@ -349,6 +350,17 @@ object errors {
   def ErrorWrapperWithExampleTransformer(pve: PartialVerificationError, transformer: CounterexampleTransformer) : PartialVerificationError =
     PartialVerificationError((reason: ErrorReason) => ErrorWrapperWithExampleTransformer(pve.f(reason).asInstanceOf[AbstractVerificationError], transformer))
 
+  case class DependencyAnalysisFakeError(dependencyGraphInterpreter: AbstractDependencyGraphInterpreter) extends AbstractVerificationError {
+    override protected def text: String = "Dependency Analysis results available."
+    override def withReason(reason: ErrorReason): AbstractVerificationError = this
+    override def reason: ErrorReason = DummyReason
+    override def id: String = "dependencyAnalysis.result"
+    override def offendingNode: ErrorNode = DummyNode
+    override def withNode(offendingNode: ErrorNode): ErrorMessage = this
+
+    override def transformedError(): AbstractVerificationError = this
+  }
+
   case class ExhaleFailed(offendingNode: Exhale, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
     val id = "exhale.failed"
     val text = "Exhale might fail."

From 4f07e8eec282a2759f225ab0254e6ce347c5402d Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Wed, 17 Dec 2025 10:00:42 +0100
Subject: [PATCH 02/27] fix source info string

---
 src/main/scala/viper/silver/ast/Ast.scala | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 62f8ed73e..304fc2db6 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -428,6 +428,8 @@ abstract class FailureExpectedInfo extends Info {
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
   override val isCached = head.isCached || tail.isCached
+
+  override def getSourceString: String = head.getSourceString ++ tail.getSourceString
 }
 
 /** Build a `ConsInfo` instance out of two `Info`s, unless the latter is `NoInfo` (which can be dropped) */

From d76e56217a1e624f562696029651a0d137fc7ffb Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Thu, 18 Dec 2025 11:39:03 +0100
Subject: [PATCH 03/27] modifications for Gobra dependency analysis

---
 src/main/scala/viper/silver/ast/Ast.scala | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 304fc2db6..9eaa77d09 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -364,8 +364,6 @@ trait Info {
     case _: T => NoInfo
     case info => info
   }
-
-  def getSourceString: String = ""
 }
 
 /** A default `Info` that is empty. */
@@ -424,12 +422,16 @@ abstract class FailureExpectedInfo extends Info {
   override val isCached = false
 }
 
+case class DependencyAnalysisInfo(info: String, pos: AbstractSourcePosition) extends Info {
+  override val comment = Nil
+  override val isCached = false
+}
+
+
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
   override val isCached = head.isCached || tail.isCached
-
-  override def getSourceString: String = head.getSourceString ++ tail.getSourceString
 }
 
 /** Build a `ConsInfo` instance out of two `Info`s, unless the latter is `NoInfo` (which can be dropped) */

From d6c8aea6997560cc96101c2a09b2ce50018c6e1a Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 19 Dec 2025 18:21:17 +0100
Subject: [PATCH 04/27] (WIP) add support for decreases clause

---
 .../transformation/DecreasesCheck.scala           | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala
index 48c959f53..88bbda1e3 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/DecreasesCheck.scala
@@ -65,7 +65,8 @@ trait DecreasesCheck extends ProgramManager with ErrorReporter {
    * @param tupleCondition     for which tuple decreasing should be checked (default: true)
    * @param errTrafo           for termination related assertions
    * @param reasonTrafoFactory for termination related assertion reasons
-   * @return termination check as a Assert Stmt (if decreasing and bounded are defined, otherwise EmptyStmt)
+   * @return termination check as a
+   *         Stmt (if decreasing and bounded are defined, otherwise EmptyStmt)
    */
   protected def createTupleCheck(tupleCondition: Option[Exp], biggerTuple: Seq[Exp], smallerTuple: Seq[Exp],
                                  errTrafo: ErrTrafo, reasonTrafoFactory: ReasonTrafoFactory): Stmt = {
@@ -87,11 +88,11 @@ trait DecreasesCheck extends ProgramManager with ErrorReporter {
     val decreasesSimpleReasonTrafo = reasonTrafoFactory.generateTupleSimpleFalse()
 
     val tupleImplies = tupleCondition match {
-      case Some(c) => Implies(c, lexCheck)(errT = decreasesSimpleReasonTrafo)
+      case Some(c) => Implies(c, lexCheck)(lexCheck.pos, lexCheck.info, decreasesSimpleReasonTrafo)
       case None => lexCheck
     }
 
-    val tupleAssert = Assert(tupleImplies)(errT = errTrafo)
+    val tupleAssert = Assert(tupleImplies)(lexCheck.pos, lexCheck.info, errTrafo)
 
     tupleAssert
   }
@@ -158,13 +159,13 @@ trait DecreasesCheck extends ProgramManager with ErrorReporter {
               argTypeVarsDecr.last -> bigger.typ
             ))(errT = boundReTrafo)
 
-          val andPart = And(dec, bound)(errT = simpleReTrafo)
+          val andPart = And(dec, bound)(smaller.pos, smaller.info,simpleReTrafo)
 
-          val eq = EqCmp(smaller, bigger)(errT = decreasesReTrafo)
+          val eq = EqCmp(smaller, bigger)(smaller.pos, smaller.info, decreasesReTrafo)
 
           val next = createExp(bTuple.tail, sTuple.tail)
-          val nextPart = And(eq, next)(errT = simpleReTrafo)
-          Or(andPart, nextPart)(errT = simpleReTrafo)
+          val nextPart = And(eq, next)(eq.pos, eq.info, simpleReTrafo)
+          Or(andPart, nextPart)(smaller.pos, smaller.info, simpleReTrafo)
         }
       }
     }

From a3335d831dd01fc18fef4c0aa21045772722b6bb Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 9 Jan 2026 16:51:47 +0100
Subject: [PATCH 05/27] cleanup of how passing dependency results to Gobra

---
 .../AbstractDependencyAnalysisResult.scala           |  8 ++++++++
 .../viper/silver/verifier/VerificationError.scala    | 12 ------------
 src/main/scala/viper/silver/verifier/Verifier.scala  |  3 +++
 3 files changed, 11 insertions(+), 12 deletions(-)
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala

diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala b/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala
new file mode 100644
index 000000000..0d53c72af
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala
@@ -0,0 +1,8 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast.Program
+
+abstract class AbstractDependencyAnalysisResult(programName: String, program: Program, dependencyGraphInterpreters: Iterable[AbstractDependencyGraphInterpreter]) {
+
+  def getFullDependencyGraphInterpreter: AbstractDependencyGraphInterpreter
+}
diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala
index 74ccf05c3..4ee3f6d45 100644
--- a/src/main/scala/viper/silver/verifier/VerificationError.scala
+++ b/src/main/scala/viper/silver/verifier/VerificationError.scala
@@ -9,7 +9,6 @@ package viper.silver.verifier
 import fastparse.Parsed
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Rewritable
-import viper.silver.dependencyAnalysis.AbstractDependencyGraphInterpreter
 
 
 /**********************************************************************************
@@ -350,17 +349,6 @@ object errors {
   def ErrorWrapperWithExampleTransformer(pve: PartialVerificationError, transformer: CounterexampleTransformer) : PartialVerificationError =
     PartialVerificationError((reason: ErrorReason) => ErrorWrapperWithExampleTransformer(pve.f(reason).asInstanceOf[AbstractVerificationError], transformer))
 
-  case class DependencyAnalysisFakeError(dependencyGraphInterpreter: AbstractDependencyGraphInterpreter) extends AbstractVerificationError {
-    override protected def text: String = "Dependency Analysis results available."
-    override def withReason(reason: ErrorReason): AbstractVerificationError = this
-    override def reason: ErrorReason = DummyReason
-    override def id: String = "dependencyAnalysis.result"
-    override def offendingNode: ErrorNode = DummyNode
-    override def withNode(offendingNode: ErrorNode): ErrorMessage = this
-
-    override def transformedError(): AbstractVerificationError = this
-  }
-
   case class ExhaleFailed(offendingNode: Exhale, reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
     val id = "exhale.failed"
     val text = "Exhale might fail."
diff --git a/src/main/scala/viper/silver/verifier/Verifier.scala b/src/main/scala/viper/silver/verifier/Verifier.scala
index ba8af5c26..7eaef6430 100644
--- a/src/main/scala/viper/silver/verifier/Verifier.scala
+++ b/src/main/scala/viper/silver/verifier/Verifier.scala
@@ -8,6 +8,7 @@ package viper.silver.verifier
 
 import viper.silver.ast.Program
 import viper.silver.components.LifetimeComponent
+import viper.silver.dependencyAnalysis.AbstractDependencyAnalysisResult
 import viper.silver.reporter.{NoopReporter, Reporter}
 
 /** An abstract class for verifiers of Viper programs.
@@ -94,6 +95,8 @@ trait Verifier extends LifetimeComponent {
   def stop(): Unit
 
   def reporter: Reporter
+
+  def getDependencyAnalysisResult: Option[AbstractDependencyAnalysisResult] = None
 }
 
 /**

From ec397f9b76572960ef00f24d1c8fc5ce2572e0f3 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Tue, 13 Jan 2026 13:31:05 +0100
Subject: [PATCH 06/27] add dependency analysis info to else branch conditions

---
 .../scala/viper/silver/cfg/silver/CfgGenerator.scala     | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
index b7ca5648b..644ae02eb 100644
--- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
+++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
@@ -363,8 +363,13 @@ object CfgGenerator {
             current = None
           case ConditionalJumpStmt(cond, thnTarget, elsTarget) =>
             current.foreach { currentIndex =>
-              val neg = Not(cond)(cond.pos, cond.info, cond.errT)
-              addTmpEdge(TmpConditionalEdge(cond, currentIndex, resolve(thnTarget)))
+              val negInfo = cond.pos match {
+                case position: AbstractSourcePosition if cond.info.getUniqueInfo[DependencyAnalysisInfo].isEmpty =>
+                  MakeInfoPair(cond.info, DependencyAnalysisInfo(cond.toString, position))
+                case _ => cond.info
+              }
+              val neg = Not(cond)(cond.pos, negInfo, cond.errT)
+              addTmpEdge(TmpConditionalEdge(cond.withMeta(cond.pos, negInfo, cond.errT), currentIndex, resolve(thnTarget)))
               addTmpEdge(TmpConditionalEdge(neg, currentIndex, resolve(elsTarget)))
             }
             current = None

From 0f3f92702b5a468215ec25978c449311b7d3f8f1 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Wed, 14 Jan 2026 11:28:16 +0100
Subject: [PATCH 07/27] add dependency types

---
 src/main/scala/viper/silver/ast/Ast.scala                 | 6 ------
 src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala | 4 ++--
 2 files changed, 2 insertions(+), 8 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 9eaa77d09..304de1bcf 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -422,12 +422,6 @@ abstract class FailureExpectedInfo extends Info {
   override val isCached = false
 }
 
-case class DependencyAnalysisInfo(info: String, pos: AbstractSourcePosition) extends Info {
-  override val comment = Nil
-  override val isCached = false
-}
-
-
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
index 644ae02eb..36b17791c 100644
--- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
+++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
@@ -364,8 +364,8 @@ object CfgGenerator {
           case ConditionalJumpStmt(cond, thnTarget, elsTarget) =>
             current.foreach { currentIndex =>
               val negInfo = cond.pos match {
-                case position: AbstractSourcePosition if cond.info.getUniqueInfo[DependencyAnalysisInfo].isEmpty =>
-                  MakeInfoPair(cond.info, DependencyAnalysisInfo(cond.toString, position))
+//                case position: AbstractSourcePosition if cond.info.getUniqueInfo[DependencyAnalysisInfo].isEmpty => TODO ake
+//                  MakeInfoPair(cond.info, DependencyAnalysisInfo(cond.toString, position))
                 case _ => cond.info
               }
               val neg = Not(cond)(cond.pos, negInfo, cond.errT)

From f0f273c6c92a00ec96be35ee9b224d16bebe2ac2 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 9 Feb 2026 15:01:28 +0100
Subject: [PATCH 08/27] infeasible paths: optimizations

---
 .../viper/silver/ast/utility/Statements.scala | 31 +++++++++++++++++++
 1 file changed, 31 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/Statements.scala b/src/main/scala/viper/silver/ast/utility/Statements.scala
index 4cd741e40..633afcfca 100644
--- a/src/main/scala/viper/silver/ast/utility/Statements.scala
+++ b/src/main/scala/viper/silver/ast/utility/Statements.scala
@@ -87,4 +87,35 @@ object Statements {
 
     writtenTo.distinct
   }
+
+  def hasProofObligations(s: Stmt, p: Program): Boolean = {
+    def goE(exp: Exp): Boolean = !Expressions.isKnownWellDefined(exp, Some(p))
+
+    def goEs(exps: Seq[Exp]): Boolean = exps exists goE
+
+    s match {
+      case _: FieldAssign | _: Exhale | _: Assert | _: Fold | _: Unfold | _: Package | _: Apply => true
+      case NewStmt(lhs, _) => goE(lhs)
+      case LocalVarAssign(lhs, rhs) => goE(lhs) || goE(rhs)
+      case MethodCall(methodName, args, targets) => p.findMethod(methodName).pres.nonEmpty || goEs(args) || goEs(targets)
+      case Inhale(exp) => goE(exp)
+      case Assume(exp) => goE(exp)
+      case Seqn(ss, _) => ss exists (hasProofObligations(_, p))
+      case If(cond, thn, els) => goE(cond) || hasProofObligations(thn, p) || hasProofObligations(els, p)
+      case While(cond, invs, body) => invs.nonEmpty || goE(cond) || hasProofObligations(body, p)
+      case Label(_, invs) => invs.nonEmpty
+      case _: Goto | _: LocalVarDeclStmt => false
+      case _: Quasihavoc | _: Quasihavocall => true
+      case _: ExtensionStmt => true // TODO ake
+    }
+  }
+
+  def introducesSmtAssumptions(s: Stmt): Boolean = s match {
+      case Seqn(ss, _) => ss exists introducesSmtAssumptions
+      case Label(_, invs) => invs.nonEmpty
+      case _: Exhale | _: Assert | _: Goto | _: LocalVarDeclStmt | _: Quasihavoc | _: Quasihavocall => false
+      case _: ExtensionStmt => true // TODO ake
+      case _ => true
+    }
+
 }

From e68f9d533fdb38ccd52f9e796413a486869c8872 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 30 Mar 2026 17:35:28 +0200
Subject: [PATCH 09/27] refactor dependency type

---
 src/main/scala/viper/silver/ast/Ast.scala     |  24 ++++
 .../AnalysisSourceInfo.scala                  | 118 ++++++++++++++++++
 .../dependencyAnalysis/DependencyType.scala   |  86 +++++++++++++
 .../FrontendDependencyAnalysisInfo.scala      |  50 ++++++++
 .../viper/silver/parser/Translator.scala      |  29 +++--
 5 files changed, 297 insertions(+), 10 deletions(-)
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 304de1bcf..164739169 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -10,8 +10,11 @@ import scala.collection.mutable
 import scala.reflect.ClassTag
 import pretty.FastPrettyPrinter
 import utility._
+import viper.silver.ast
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
+import viper.silver.dependencyAnalysis.{AssumptionType, DependencyType}
+import viper.silver.dependencyAnalysis.DependencyType.{ExplicitAssertion, ExplicitAssumption, MethodCall, Rewrite, SourceCode}
 import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
@@ -422,6 +425,27 @@ abstract class FailureExpectedInfo extends Info {
   override val isCached = false
 }
 
+object DependencyTypeInfo {
+  def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = {
+    val depType = stmt match {
+      case _: ast.MethodCall => MethodCall
+      case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
+      case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
+      case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
+      case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
+      case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
+      case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
+    }
+    DependencyTypeInfo(depType)
+  }
+}
+
+case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
+
+  override def comment: Seq[String] = Nil
+  override def isCached: Boolean = false
+}
+
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
new file mode 100644
index 000000000..3c2ee2f22
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
@@ -0,0 +1,118 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast
+import viper.silver.ast._
+
+object AnalysisSourceInfo {
+  def extractPositionString(p: Position): String = {
+    p match {
+      case NoPosition => "???"
+      case filePos: AbstractSourcePosition => filePos.file.getFileName.toString + " @ line " + filePos.line
+      case filePos: FilePosition => filePos.file.getFileName.toString + " @ line " + filePos.line
+      case lineColumn: HasLineColumn => "line " + lineColumn.line.toString
+      case VirtualPosition(identifier) => "label " + identifier
+    }
+  }
+
+  def createAnalysisSourceInfo(exp: ast.Exp): AnalysisSourceInfo = {
+    val depInfo = exp.info.getUniqueInfo[FrontendDependencyAnalysisInfo]
+    if(depInfo.isDefined) depInfo.get.getAnalysisSourceInfo
+    else ExpAnalysisSourceInfo(exp, exp.pos)
+  }
+
+  def createAnalysisSourceInfo(stmt: ast.Stmt): AnalysisSourceInfo = {
+    val depInfo = stmt.info.getUniqueInfo[FrontendDependencyAnalysisInfo]
+    if(depInfo.isDefined) depInfo.get.getAnalysisSourceInfo
+    else StmtAnalysisSourceInfo(stmt, stmt.pos)
+  }
+
+  def createAnalysisSourceInfo(description: String, pos: Position): AnalysisSourceInfo = StringAnalysisSourceInfo(description, pos)
+
+}
+
+trait AnalysisSourceInfo extends ast.Info {
+  override def toString: String = getPositionString
+
+  def getDescription: String
+
+  def getLineNumber: Option[Int] = getPosition match {
+    case column: HasLineColumn => Some(column.line)
+    case _ => None
+  }
+
+  def getPositionString: String = {
+    AnalysisSourceInfo.extractPositionString(getPosition)
+  }
+
+  def getPosition: Position
+
+  /**
+   * @return the analysis source info used for lifting low-level graphs to higher-level graphs
+   *         and presenting dependency results to the user
+   */
+  def getTopLevelSource: AnalysisSourceInfo = this
+
+  /**
+   * @return the analysis source info used for adding transitive edges within a source exp/stmt
+   */
+  def getSourceForTransitiveEdges: AnalysisSourceInfo = getTopLevelSource
+
+  /**
+   * @return the analysis source info used for joining graphs
+   */
+  def getFineGrainedSource: AnalysisSourceInfo = this
+
+  def isAnalysisEnabled: Boolean = true
+
+
+  override def comment: Seq[String] = Nil
+  override def isCached: Boolean = false
+}
+
+case class NoAnalysisSourceInfo() extends AnalysisSourceInfo {
+  override def getPosition: Position = NoPosition
+
+  override def getDescription: String = ""
+
+  override def equals(obj: Any): Boolean = false
+}
+
+case class ExpAnalysisSourceInfo(source: ast.Exp, pos: Position) extends AnalysisSourceInfo {
+
+  override def toString: String = getDescription + " (" + super.toString + ")"
+
+  override def getPosition: Position = pos
+
+  override def isAnalysisEnabled: Boolean = true // DependencyAnalyzer.extractEnableAnalysisFromInfo(source.info).getOrElse(true)
+
+  override def getDescription: String = source.toString.replaceAll("\n", "\t")
+}
+
+case class StmtAnalysisSourceInfo(source: ast.Stmt, pos: Position) extends AnalysisSourceInfo {
+
+  override def toString: String = getDescription + " (" + super.toString + ")"
+  override def getPosition: Position = pos
+
+  override def isAnalysisEnabled: Boolean = true // DependencyAnalyzer.extractEnableAnalysisFromInfo(source.info).getOrElse(true)
+
+  override def getDescription: String = source.toString().replaceAll("\n", "\t")
+}
+
+case class StringAnalysisSourceInfo(description: String, position: Position) extends AnalysisSourceInfo {
+  override def toString: String = getDescription + " (" + getPositionString + ")"
+  override def getPosition: Position = position
+
+  override def getDescription: String = description.replaceAll("\n", "\t")
+}
+
+case class CompositeAnalysisSourceInfo(coarseGrainedSource: AnalysisSourceInfo, fineGrainedSource: AnalysisSourceInfo) extends AnalysisSourceInfo {
+  override def toString: String = getTopLevelSource.toString
+  override def getPosition: Position = coarseGrainedSource.getPosition
+
+  override def getTopLevelSource: AnalysisSourceInfo = coarseGrainedSource.getTopLevelSource
+  override def getFineGrainedSource: AnalysisSourceInfo = fineGrainedSource.getFineGrainedSource
+
+  override def isAnalysisEnabled: Boolean = coarseGrainedSource.isAnalysisEnabled && fineGrainedSource.isAnalysisEnabled
+
+  override def getDescription: String = coarseGrainedSource.getDescription
+}
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
new file mode 100644
index 000000000..695db98e4
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -0,0 +1,86 @@
+package viper.silver.dependencyAnalysis
+
+object AssumptionType extends Enumeration {
+  type AssumptionType = Value
+  val Explicit, LoopInvariant, PathCondition, Rewrite, SourceCode, DomainAxiom, Implicit, Internal, Trigger, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, MethodCall, FunctionBody, Precondition, Ghost, Annotation, CustomInternal, Unknown = Value
+
+  def fromString(s: String): Option[Value] = values.find(_.toString == s)
+
+  def explicitAssumptionTypes: Set[AssumptionType] = Set(Explicit, ExplicitPostcondition)
+  def postconditionTypes: Set[AssumptionType] = Set(ImplicitPostcondition, ExplicitPostcondition, ImportedPostcondition)
+  def preconditionTypes: Set[AssumptionType] = Set(Precondition)
+  def explicitAssertionTypes: Set[AssumptionType] = Set(Explicit, ImplicitPostcondition, ExplicitPostcondition)
+  def internalTypes: Set[AssumptionType] = Set(Internal, Trigger, CustomInternal) // will always be hidden from user
+  def joinConditionTypes: Set[AssumptionType] = preconditionTypes ++ postconditionTypes ++ Set(FunctionBody, MethodCall)
+  def importedTypes: Set[AssumptionType] = Set(ImportedPostcondition)
+  def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation)
+  def sourceCodeTypes: Set[AssumptionType] = AssumptionType.values.diff(explicitAssumptionTypes ++ explicitAssertionTypes ++ verificationAnnotationTypes ++ internalTypes)
+
+  def getMaxPriorityAssumptionType(types: Set[AssumptionType]): Option[AssumptionType] = {
+    val priorityList = List(ExplicitPostcondition, Explicit) ++ internalTypes.toList ++ verificationAnnotationTypes.toList ++ sourceCodeTypes.toList ++ values.toList
+    priorityList.find(t => types.contains(t))
+  }
+
+  def getPostcondType(isAbstractFunction: Boolean, dependencyType: Option[DependencyType]=None, isImported: Boolean=false): AssumptionType = {
+    if(isImported) return ImportedPostcondition
+
+    dependencyType.flatMap(_.assertionType match {
+      case AssumptionType.Explicit | AssumptionType.ExplicitPostcondition => Some(AssumptionType.ExplicitPostcondition)
+      case AssumptionType.ImportedPostcondition => Some(AssumptionType.ImportedPostcondition)
+      case AssumptionType.ImplicitPostcondition  => Some(AssumptionType.ImplicitPostcondition)
+      case AssumptionType.Internal => Some(AssumptionType.Internal)
+      case AssumptionType.CustomInternal => Some(AssumptionType.CustomInternal)
+      case AssumptionType.Annotation | AssumptionType.Ghost => None
+      case _ => None
+    }).getOrElse(
+      if(isAbstractFunction) AssumptionType.ExplicitPostcondition else AssumptionType.ImplicitPostcondition
+    )
+  }
+}
+
+import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType
+
+object DependencyType {
+
+  val Implicit: DependencyType = DependencyType(AssumptionType.Implicit, AssumptionType.Implicit)
+  val SourceCode: DependencyType = DependencyType(AssumptionType.SourceCode, AssumptionType.SourceCode)
+  val Explicit: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Explicit)
+  val ExplicitAssertion: DependencyType = DependencyType(AssumptionType.Ghost, AssumptionType.Explicit)
+  val ExplicitAssumption: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Implicit)
+  val PathCondition: DependencyType = DependencyType(AssumptionType.PathCondition, AssumptionType.Implicit)
+  val Invariant: DependencyType = DependencyType(AssumptionType.LoopInvariant, AssumptionType.LoopInvariant)
+  val Rewrite: DependencyType = DependencyType(AssumptionType.Rewrite, AssumptionType.Rewrite)
+  val Internal: DependencyType = DependencyType(AssumptionType.Internal, AssumptionType.Internal)
+  val Trigger: DependencyType = DependencyType(AssumptionType.Trigger, AssumptionType.Trigger)
+  val MethodCall: DependencyType = DependencyType(AssumptionType.MethodCall, AssumptionType.MethodCall)
+  val Ghost: DependencyType = DependencyType.make(AssumptionType.Ghost)
+  val Annotation: DependencyType = DependencyType.make(AssumptionType.Annotation)
+
+  def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
+
+//  def get(stmt: ast.Stmt): DependencyType = {
+//    val annotatedDependencyType = DependencyAnalyzer.extractDependencyTypeFromInfo(stmt.info)
+//    if(annotatedDependencyType.isDefined) return annotatedDependencyType.get
+//
+//    stmt match {
+//      case _: ast.MethodCall => MethodCall
+//      case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
+//      case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
+//      case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
+//      case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
+//      case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
+//      case _ => DependencyType.make(Unknown) /* TODO: should not happen */
+//    }
+//  }
+//
+//  def get(exp: ast.Exp, dependencyType: DependencyType): DependencyType = DependencyAnalyzer.extractDependencyTypeFromInfo(exp.info).getOrElse(dependencyType)
+
+  def getMaxPriorityType(types: Set[DependencyType]): Option[DependencyType] = {
+    val assumptionType = AssumptionType.getMaxPriorityAssumptionType(types.map(_.assumptionType))
+    val assertionType = AssumptionType.getMaxPriorityAssumptionType(types.map(_.assertionType))
+    if(assumptionType.isDefined && assertionType.isDefined) Some(DependencyType(assumptionType.get, assertionType.get)) else None
+  }
+
+}
+
+case class DependencyType(assumptionType: AssumptionType, assertionType: AssumptionType)
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala
new file mode 100644
index 000000000..b2993426d
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala
@@ -0,0 +1,50 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast.{Info, Position}
+import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType
+
+abstract class FrontendDependencyAnalysisInfo extends Info {
+  override val comment = Nil
+  override val isCached = false
+
+  val info: String
+  val pos: Position
+  val dependencyType: Option[DependencyType]=None
+
+  def getAnalysisSourceInfo: AnalysisSourceInfo
+}
+
+case class SimpleFrontendDependencyAnalysisInfo(sourceInfo: AnalysisSourceInfo, _dependencyType: DependencyType) extends FrontendDependencyAnalysisInfo {
+
+  override val info: String = sourceInfo.toString
+  override val pos: Position = sourceInfo.getPosition
+  override val dependencyType: Option[DependencyType] = Some(_dependencyType)
+
+  override def getAnalysisSourceInfo: AnalysisSourceInfo = sourceInfo
+}
+
+/*
+ Viper statements / expressions with a DependencyAnalysisJoinNodeInfo will produce an assertion and assumption node with the given source info and dependency type,
+ and with isJoinNode set to true.
+ The idea is that these nodes can be used to join graphs without the need for an explicit method call.
+ We use this, for example, for Gobra interfaces and implementation proofs.
+ */
+case class DependencyAnalysisJoinNodeInfo(sourceInfo: AnalysisSourceInfo, _dependencyType: DependencyType) extends FrontendDependencyAnalysisInfo {
+//  def getAssertionNode: GeneralAssertionNode =
+//    SimpleAssertionNode(True, sourceInfo, AssumptionType.CustomInternal, isClosed=false, isJoinNode=true)
+//
+//  def getAssertionNode(outerSourceInfo: AnalysisSourceInfo): GeneralAssertionNode =
+//    SimpleAssertionNode(True, CompositeAnalysisSourceInfo(outerSourceInfo, sourceInfo), AssumptionType.CustomInternal,  isClosed=false, isJoinNode=true)
+//
+//  def getAssertionNode(outerSourceInfo: AnalysisSourceInfo, assumptionType: AssumptionType): GeneralAssertionNode =
+//    SimpleAssertionNode(True, CompositeAnalysisSourceInfo(outerSourceInfo, sourceInfo), assumptionType,  isClosed=false, isJoinNode=true)
+//
+//  def getAssumptionNode(outerSourceInfo: AnalysisSourceInfo): GeneralAssumptionNode =
+//    SimpleAssumptionNode(True, None, CompositeAnalysisSourceInfo(outerSourceInfo, sourceInfo), AssumptionType.CustomInternal, isClosed=false, isJoinNode=true)
+
+  override val info: String = sourceInfo.toString
+  override val pos: Position = sourceInfo.getPosition
+  override val dependencyType: Option[DependencyType] = Some(_dependencyType)
+
+  override def getAnalysisSourceInfo: AnalysisSourceInfo = sourceInfo
+}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index a09b825bd..20c24997a 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -9,6 +9,7 @@ package viper.silver.parser
 import viper.silver.FastMessaging
 import viper.silver.ast.utility._
 import viper.silver.ast.{SourcePosition, _}
+import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
 import viper.silver.plugin.standard.adt.{Adt, AdtType}
 
 import scala.collection.mutable
@@ -82,7 +83,9 @@ case class Translator(program: PProgram) {
 
       val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn])
 
-      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT)
+      val postconditionType = if(body.isDefined) DependencyType.make(AssumptionType.ImplicitPostcondition) else DependencyType.make(AssumptionType.ExplicitPostcondition)
+
+      val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e, Some(DependencyType.make(AssumptionType.Precondition)))), posts = posts.toSeq map (p => exp(p.e, Some(postconditionType))), body = newBody)(m.pos, m.info, m.errT)
 
       members(m.name) = finalMethod
 
@@ -108,7 +111,8 @@ case class Translator(program: PProgram) {
   private def translate(f: PFunction): Function = f match {
     case PFunction(_, _, idndef, _, _, _, pres, posts, body) =>
       val f = findFunction(idndef)
-      val ff = f.copy( pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = body map (_.e.inner) map exp)(f.pos, f.info, f.errT)
+      val postconditionType = if(body.isDefined) DependencyType.make(AssumptionType.ImplicitPostcondition) else DependencyType.make(AssumptionType.ExplicitPostcondition)
+      val ff = f.copy( pres = pres.toSeq map (p => exp(p.e, Some(DependencyType.make(AssumptionType.Precondition)))), posts = posts.toSeq map (p => exp(p.e, Some(postconditionType))), body = body map (_.e.inner) map (exp(_, Some(DependencyType.make(AssumptionType.FunctionBody)))))(f.pos, f.info, f.errT)
       members(f.name) = ff
       ff
   }
@@ -176,7 +180,7 @@ case class Translator(program: PProgram) {
     val (s, annotations) = extractAnnotationFromStmt(pStmt)
     val sourcePNodeInfo = SourcePNodeInfo(pStmt)
     val info = if (annotations.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotations))
-    s match {
+    val resS = s match {
       case PAssign(targets, _, PCall(method, args, _)) if members(method.name).isInstanceOf[Method] =>
         methodCallAssign(s, targets.toSeq, ts => MethodCall(findMethod(method), args.inner.toSeq map exp, ts)(pos, info))
       case PAssign(targets, _, _) if targets.length != 1 =>
@@ -215,9 +219,9 @@ case class Translator(program: PProgram) {
       case PApplyWand(_, e) =>
         Apply(exp(e).asInstanceOf[MagicWand])(pos, info)
       case PInhale(_, e) =>
-        Inhale(exp(e))(pos, info)
+        Inhale(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PAssume(_, e) =>
-        Assume(exp(e))(pos, info)
+        Assume(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PExhale(_, e) =>
         Exhale(exp(e))(pos, info)
       case PAssert(_, e) =>
@@ -227,13 +231,13 @@ case class Translator(program: PProgram) {
       case PGoto(_, label) =>
         Goto(label.name)(pos, info)
       case PIf(_, cond, thn, els) =>
-        If(exp(cond.inner), stmt(thn).asInstanceOf[Seqn], els map (stmt(_) match {
+        If(exp(cond.inner, Some(DependencyType.PathCondition)), stmt(thn).asInstanceOf[Seqn], els map (stmt(_) match {
           case s: Seqn => s
           case s => Seqn(Seq(s), Nil)(s.pos, s.info)
         }) getOrElse Statements.EmptyStmt)(pos, info)
       case PElse(_, els) => stmt(els)
       case PWhile(_, cond, invs, body) =>
-        While(exp(cond.inner), invs.toSeq map (inv => exp(inv.e)), stmt(body).asInstanceOf[Seqn])(pos, info)
+        While(exp(cond.inner, Some(DependencyType.PathCondition)), invs.toSeq map (inv => exp(inv.e, Some(DependencyType.Invariant))), stmt(body).asInstanceOf[Seqn])(pos, info)
       case PQuasihavoc(_, lhs, e) =>
         val (newLhs, newE) = havocStmtHelper(lhs, e)
         Quasihavoc(newLhs, newE)(pos, info)
@@ -245,6 +249,7 @@ case class Translator(program: PProgram) {
       case _: PDefine | _: PSkip =>
         sys.error(s"Found unexpected intermediate statement $s (${s.getClass.getName}})")
     }
+    resS.withMeta(resS.pos, MakeInfoPair(MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(resS), DependencyTypeInfo.getDependencyTypeInfo(resS)), resS.info), resS.errT)
   }
 
   /**
@@ -342,17 +347,20 @@ case class Translator(program: PProgram) {
     }
   }
 
+  def exp(parseExp: PExp): Exp = exp(parseExp, None)
+
   /** Takes a `PExp` and turns it into an `Exp`. */
-  def exp(parseExp: PExp): Exp = {
+  def exp(parseExp: PExp, dependencyType: Option[DependencyType]): Exp = {
     val pos = parseExp
     val (pexp, annotationMap) = extractAnnotation(parseExp)
     val sourcePNodeInfo = SourcePNodeInfo(parseExp)
-    val info = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
+    val info0 = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
+    val info = if(dependencyType.isDefined) ConsInfo(info0, DependencyTypeInfo(dependencyType.get)) else info0
     expInternal(pexp, pos, info)
   }
 
   protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
-    pexp match {
+    val expr = pexp match {
       case PIdnUseExp(piu) =>
         piu.decl match {
           case Some(_: PTypedVarDecl) => LocalVar(piu.name, ttyp(pexp.typ))(pos, info)
@@ -634,6 +642,7 @@ case class Translator(program: PProgram) {
 
       case t: PExtender => t.translateExp(this)
     }
+    expr.withMeta((expr.pos, MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(expr), expr.info), expr.errT))
   }
 
   implicit def liftPos(node: Where): SourcePosition = Translator.liftWhere(node)

From 5bca3ee1a0fb2ae52869390a7b7e445351ef48f3 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 30 Mar 2026 20:16:54 +0200
Subject: [PATCH 10/27] refactoring

---
 .../ast/utility/ImpureAssumeRewriter.scala    |  2 +-
 .../AnalysisSourceInfo.scala                  | 26 -------------
 .../dependencyAnalysis/DependencyType.scala   |  1 +
 .../viper/silver/parser/Translator.scala      | 39 ++++++++++++-------
 4 files changed, 26 insertions(+), 42 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
index e3587c590..ff39a8834 100644
--- a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
+++ b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
@@ -227,7 +227,7 @@ object ImpureAssumeRewriter {
     }).execute(p)
 
     val pAssume: Program = ViperStrategy.Slim({
-      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos))
+      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos, a.info, a.errT))
     }).execute(pInvs)
 
     if (funcs.isEmpty && domains.isEmpty) {
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
index 3c2ee2f22..dac6858e4 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
@@ -46,21 +46,6 @@ trait AnalysisSourceInfo extends ast.Info {
 
   def getPosition: Position
 
-  /**
-   * @return the analysis source info used for lifting low-level graphs to higher-level graphs
-   *         and presenting dependency results to the user
-   */
-  def getTopLevelSource: AnalysisSourceInfo = this
-
-  /**
-   * @return the analysis source info used for adding transitive edges within a source exp/stmt
-   */
-  def getSourceForTransitiveEdges: AnalysisSourceInfo = getTopLevelSource
-
-  /**
-   * @return the analysis source info used for joining graphs
-   */
-  def getFineGrainedSource: AnalysisSourceInfo = this
 
   def isAnalysisEnabled: Boolean = true
 
@@ -105,14 +90,3 @@ case class StringAnalysisSourceInfo(description: String, position: Position) ext
   override def getDescription: String = description.replaceAll("\n", "\t")
 }
 
-case class CompositeAnalysisSourceInfo(coarseGrainedSource: AnalysisSourceInfo, fineGrainedSource: AnalysisSourceInfo) extends AnalysisSourceInfo {
-  override def toString: String = getTopLevelSource.toString
-  override def getPosition: Position = coarseGrainedSource.getPosition
-
-  override def getTopLevelSource: AnalysisSourceInfo = coarseGrainedSource.getTopLevelSource
-  override def getFineGrainedSource: AnalysisSourceInfo = fineGrainedSource.getFineGrainedSource
-
-  override def isAnalysisEnabled: Boolean = coarseGrainedSource.isAnalysisEnabled && fineGrainedSource.isAnalysisEnabled
-
-  override def getDescription: String = coarseGrainedSource.getDescription
-}
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index 695db98e4..21b3aaaac 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -55,6 +55,7 @@ object DependencyType {
   val MethodCall: DependencyType = DependencyType(AssumptionType.MethodCall, AssumptionType.MethodCall)
   val Ghost: DependencyType = DependencyType.make(AssumptionType.Ghost)
   val Annotation: DependencyType = DependencyType.make(AssumptionType.Annotation)
+  val Axiom: DependencyType = DependencyType.make(AssumptionType.DomainAxiom)
 
   def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 20c24997a..7fb6cf303 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -101,11 +101,20 @@ case class Translator(program: PProgram) {
       dd
   }
 
-  private def translate(a: PAxiom): DomainAxiom = a match {
-    case pa@PAxiom(anns, _, Some(name), e) =>
-      NamedDomainAxiom(name.name, exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
-    case pa@PAxiom(anns, _, None, e) =>
-      AnonymousDomainAxiom(exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+  private def translate(a: PAxiom): DomainAxiom = {
+    def attachInfo(axiom: DomainAxiom) = {
+      val info = ConsInfo(axiom.info, ConsInfo(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), DependencyTypeInfo(DependencyType.Axiom)))
+      axiom.withMeta(axiom.pos, info, axiom.errT)
+    }
+
+    a match {
+      case pa@PAxiom(anns, _, Some(name), e) =>
+        val axiom = NamedDomainAxiom(name.name, exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        attachInfo(axiom)
+      case pa@PAxiom(anns, _, None, e) =>
+        val axiom = AnonymousDomainAxiom(exp(e.e.inner, Some(DependencyType.make(AssumptionType.DomainAxiom))))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        attachInfo(axiom)
+    }
   }
 
   private def translate(f: PFunction): Function = f match {
@@ -210,22 +219,22 @@ case class Translator(program: PProgram) {
         }.flatten
         Seqn(seqn filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos, info)
       case PFold(_, e) =>
-        Fold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info)
+        Fold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info)
       case PUnfold(_, e) =>
-        Unfold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info)
+        Unfold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info)
       case PPackageWand(_, e, proofScript) =>
-        val wand = exp(e).asInstanceOf[MagicWand]
+        val wand = exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand]
         Package(wand, proofScript map (stmt(_).asInstanceOf[Seqn]) getOrElse Statements.EmptyStmt)(pos, info)
       case PApplyWand(_, e) =>
-        Apply(exp(e).asInstanceOf[MagicWand])(pos, info)
+        Apply(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand])(pos, info)
       case PInhale(_, e) =>
         Inhale(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PAssume(_, e) =>
         Assume(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PExhale(_, e) =>
-        Exhale(exp(e))(pos, info)
+        Exhale(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info)
       case PAssert(_, e) =>
-        Assert(exp(e))(pos, info)
+        Assert(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info)
       case PLabel(_, name, invs) =>
         Label(name.name, invs.toSeq map (_.e) map exp)(pos, info)
       case PGoto(_, label) =>
@@ -355,11 +364,11 @@ case class Translator(program: PProgram) {
     val (pexp, annotationMap) = extractAnnotation(parseExp)
     val sourcePNodeInfo = SourcePNodeInfo(parseExp)
     val info0 = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
-    val info = if(dependencyType.isDefined) ConsInfo(info0, DependencyTypeInfo(dependencyType.get)) else info0
-    expInternal(pexp, pos, info)
+    val info = if(dependencyType.isDefined) MakeInfoPair(info0, DependencyTypeInfo(dependencyType.get)) else info0
+    expInternal(pexp, pos, info, dependencyType)
   }
 
-  protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
+  protected def expInternal(pexp: PExp, pos: PExp, info: Info, dependencyType: Option[DependencyType]): Exp = {
     val expr = pexp match {
       case PIdnUseExp(piu) =>
         piu.decl match {
@@ -369,7 +378,7 @@ case class Translator(program: PProgram) {
           case _ => sys.error("should not occur in type-checked program")
         }
       case pbe @ PBinExp(left, op, right) =>
-        val (l, r) = (exp(left), exp(right))
+        val (l, r) = (exp(left, dependencyType), exp(right, dependencyType))
         op.rs match {
           case PSymOp.Plus =>
             r.typ match {

From 5bfadfbd4fff1563ed7a43b5cae74a39c9bdd6ef Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 30 Mar 2026 20:16:54 +0200
Subject: [PATCH 11/27] refactoring

---
 .../ast/utility/ImpureAssumeRewriter.scala    |  2 +-
 .../AnalysisSourceInfo.scala                  | 26 ------------
 .../dependencyAnalysis/DependencyType.scala   |  1 +
 .../viper/silver/parser/Translator.scala      | 41 +++++++++++--------
 4 files changed, 27 insertions(+), 43 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
index e3587c590..ff39a8834 100644
--- a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
+++ b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
@@ -227,7 +227,7 @@ object ImpureAssumeRewriter {
     }).execute(p)
 
     val pAssume: Program = ViperStrategy.Slim({
-      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos))
+      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos, a.info, a.errT))
     }).execute(pInvs)
 
     if (funcs.isEmpty && domains.isEmpty) {
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
index 3c2ee2f22..dac6858e4 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
@@ -46,21 +46,6 @@ trait AnalysisSourceInfo extends ast.Info {
 
   def getPosition: Position
 
-  /**
-   * @return the analysis source info used for lifting low-level graphs to higher-level graphs
-   *         and presenting dependency results to the user
-   */
-  def getTopLevelSource: AnalysisSourceInfo = this
-
-  /**
-   * @return the analysis source info used for adding transitive edges within a source exp/stmt
-   */
-  def getSourceForTransitiveEdges: AnalysisSourceInfo = getTopLevelSource
-
-  /**
-   * @return the analysis source info used for joining graphs
-   */
-  def getFineGrainedSource: AnalysisSourceInfo = this
 
   def isAnalysisEnabled: Boolean = true
 
@@ -105,14 +90,3 @@ case class StringAnalysisSourceInfo(description: String, position: Position) ext
   override def getDescription: String = description.replaceAll("\n", "\t")
 }
 
-case class CompositeAnalysisSourceInfo(coarseGrainedSource: AnalysisSourceInfo, fineGrainedSource: AnalysisSourceInfo) extends AnalysisSourceInfo {
-  override def toString: String = getTopLevelSource.toString
-  override def getPosition: Position = coarseGrainedSource.getPosition
-
-  override def getTopLevelSource: AnalysisSourceInfo = coarseGrainedSource.getTopLevelSource
-  override def getFineGrainedSource: AnalysisSourceInfo = fineGrainedSource.getFineGrainedSource
-
-  override def isAnalysisEnabled: Boolean = coarseGrainedSource.isAnalysisEnabled && fineGrainedSource.isAnalysisEnabled
-
-  override def getDescription: String = coarseGrainedSource.getDescription
-}
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index 695db98e4..21b3aaaac 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -55,6 +55,7 @@ object DependencyType {
   val MethodCall: DependencyType = DependencyType(AssumptionType.MethodCall, AssumptionType.MethodCall)
   val Ghost: DependencyType = DependencyType.make(AssumptionType.Ghost)
   val Annotation: DependencyType = DependencyType.make(AssumptionType.Annotation)
+  val Axiom: DependencyType = DependencyType.make(AssumptionType.DomainAxiom)
 
   def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 20c24997a..d9daa7976 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -101,11 +101,20 @@ case class Translator(program: PProgram) {
       dd
   }
 
-  private def translate(a: PAxiom): DomainAxiom = a match {
-    case pa@PAxiom(anns, _, Some(name), e) =>
-      NamedDomainAxiom(name.name, exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
-    case pa@PAxiom(anns, _, None, e) =>
-      AnonymousDomainAxiom(exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+  private def translate(a: PAxiom): DomainAxiom = {
+    def attachInfo(axiom: DomainAxiom) = {
+      val info = ConsInfo(axiom.info, ConsInfo(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), DependencyTypeInfo(DependencyType.Axiom)))
+      axiom.withMeta(axiom.pos, info, axiom.errT)
+    }
+
+    a match {
+      case pa@PAxiom(anns, _, Some(name), e) =>
+        val axiom = NamedDomainAxiom(name.name, exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        attachInfo(axiom)
+      case pa@PAxiom(anns, _, None, e) =>
+        val axiom = AnonymousDomainAxiom(exp(e.e.inner, Some(DependencyType.make(AssumptionType.DomainAxiom))))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        attachInfo(axiom)
+    }
   }
 
   private def translate(f: PFunction): Function = f match {
@@ -120,7 +129,7 @@ case class Translator(program: PProgram) {
   private def translate(p: PPredicate): Predicate = p match {
     case PPredicate(_, _, idndef, _, body) =>
       val p = findPredicate(idndef)
-      val pp = p.copy(body = body map (_.e.inner) map exp)(p.pos, p.info, p.errT)
+      val pp = p.copy(body = body map (_.e.inner) map (exp(_, Some(DependencyType.Rewrite))))(p.pos, p.info, p.errT)
       members(p.name) = pp
       pp
   }
@@ -210,22 +219,22 @@ case class Translator(program: PProgram) {
         }.flatten
         Seqn(seqn filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos, info)
       case PFold(_, e) =>
-        Fold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info)
+        Fold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info)
       case PUnfold(_, e) =>
-        Unfold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info)
+        Unfold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info)
       case PPackageWand(_, e, proofScript) =>
-        val wand = exp(e).asInstanceOf[MagicWand]
+        val wand = exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand]
         Package(wand, proofScript map (stmt(_).asInstanceOf[Seqn]) getOrElse Statements.EmptyStmt)(pos, info)
       case PApplyWand(_, e) =>
-        Apply(exp(e).asInstanceOf[MagicWand])(pos, info)
+        Apply(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand])(pos, info)
       case PInhale(_, e) =>
         Inhale(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PAssume(_, e) =>
         Assume(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PExhale(_, e) =>
-        Exhale(exp(e))(pos, info)
+        Exhale(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info)
       case PAssert(_, e) =>
-        Assert(exp(e))(pos, info)
+        Assert(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info)
       case PLabel(_, name, invs) =>
         Label(name.name, invs.toSeq map (_.e) map exp)(pos, info)
       case PGoto(_, label) =>
@@ -355,11 +364,11 @@ case class Translator(program: PProgram) {
     val (pexp, annotationMap) = extractAnnotation(parseExp)
     val sourcePNodeInfo = SourcePNodeInfo(parseExp)
     val info0 = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
-    val info = if(dependencyType.isDefined) ConsInfo(info0, DependencyTypeInfo(dependencyType.get)) else info0
-    expInternal(pexp, pos, info)
+    val info = if(dependencyType.isDefined) MakeInfoPair(info0, DependencyTypeInfo(dependencyType.get)) else info0
+    expInternal(pexp, pos, info, dependencyType)
   }
 
-  protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
+  protected def expInternal(pexp: PExp, pos: PExp, info: Info, dependencyType: Option[DependencyType]): Exp = {
     val expr = pexp match {
       case PIdnUseExp(piu) =>
         piu.decl match {
@@ -369,7 +378,7 @@ case class Translator(program: PProgram) {
           case _ => sys.error("should not occur in type-checked program")
         }
       case pbe @ PBinExp(left, op, right) =>
-        val (l, r) = (exp(left), exp(right))
+        val (l, r) = (exp(left, dependencyType), exp(right, dependencyType))
         op.rs match {
           case PSymOp.Plus =>
             r.typ match {

From ff2c3356ffbcf9f157d1dbf6fc439da50c2d6d0c Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Tue, 31 Mar 2026 13:45:14 +0200
Subject: [PATCH 12/27] fix analysis source info

---
 .../ast/utility/QuantifiedPermissions.scala   |  5 +-
 .../viper/silver/parser/Translator.scala      | 91 ++++++++++---------
 2 files changed, 51 insertions(+), 45 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 5d99d4e62..176b43a97 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -9,6 +9,7 @@ package viper.silver.ast.utility
 import scala.collection.mutable
 import scala.language.postfixOps
 import viper.silver.ast._
+import viper.silver.dependencyAnalysis.AnalysisSourceInfo
 
 /** Utility methods for quantified predicate permissions. */
 object QuantifiedPermissions {
@@ -164,7 +165,7 @@ object QuantifiedPermissions {
   def desugarSourceQuantifiedPermissionSyntax(source: Forall): Seq[Forall] = {
 
 
-    source match {
+    val res = source match {
       case SourceQuantifiedPermissionAssertion(_, Implies(cond, rhs)) if (!rhs.isPure) =>
         /* Source forall denotes a quantified permission assertion that potentially
          * needs to be desugared
@@ -272,5 +273,7 @@ object QuantifiedPermissions {
          */
         Seq(source)
     }
+
+    res.map(e => e.withMeta(e.pos, MakeInfoPair(AnalysisSourceInfo.createAnalysisSourceInfo(e), e.info), e.errT))
   }
 }
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index d9daa7976..924a9ca32 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -369,6 +369,9 @@ case class Translator(program: PProgram) {
   }
 
   protected def expInternal(pexp: PExp, pos: PExp, info: Info, dependencyType: Option[DependencyType]): Exp = {
+
+    def goExp(parseExp: PExp) = exp(parseExp, dependencyType)
+
     val expr = pexp match {
       case PIdnUseExp(piu) =>
         piu.decl match {
@@ -378,7 +381,7 @@ case class Translator(program: PProgram) {
           case _ => sys.error("should not occur in type-checked program")
         }
       case pbe @ PBinExp(left, op, right) =>
-        val (l, r) = (exp(left, dependencyType), exp(right, dependencyType))
+        val (l, r) = (goExp(left), goExp(right))
         op.rs match {
           case PSymOp.Plus =>
             r.typ match {
@@ -471,7 +474,7 @@ case class Translator(program: PProgram) {
           case _ => sys.error(s"unexpected operator $op")
         }
       case PUnExp(op, pe) =>
-        val e = exp(pe)
+        val e = goExp(pe)
         op.rs match {
           case PSymOp.Neg =>
             e.typ match {
@@ -482,7 +485,7 @@ case class Translator(program: PProgram) {
           case PSymOp.Not => Not(e)(pos, info)
         }
       case PInhaleExhaleExp(_, in, _, ex, _) =>
-        InhaleExhaleExp(exp(in), exp(ex))(pos, info)
+        InhaleExhaleExp(goExp(in), goExp(ex))(pos, info)
       case PIntLit(i) =>
         IntLit(i)(pos, info)
       case p@PResultLit(_) =>
@@ -494,13 +497,13 @@ case class Translator(program: PProgram) {
       case PNullLit(_) =>
         NullLit()(pos, info)
       case PFieldAccess(rcv, _, idn) =>
-        FieldAccess(exp(rcv), findField(idn))(pos, info)
-      case PMagicWandExp(left, _, right) => MagicWand(exp(left), exp(right))(pos, info)
+        FieldAccess(goExp(rcv), findField(idn))(pos, info)
+      case PMagicWandExp(left, _, right) => MagicWand(goExp(left), goExp(right))(pos, info)
       case pfa@PCall(func, args, _) =>
         members(func.name) match {
-          case f: Function => FuncApp(f, args.inner.toSeq map exp)(pos, info)
+          case f: Function => FuncApp(f, args.inner.toSeq map goExp)(pos, info)
           case f @ DomainFunc(_, _, _, _, _) =>
-            val actualArgs = args.inner.toSeq map exp
+            val actualArgs = args.inner.toSeq map goExp
             /* TODO: Not used - problem?*/
             type TypeSubstitution = Map[TypeVar, Type]
             val so : Option[TypeSubstitution] = pfa.domainSubstitution match{
@@ -520,33 +523,33 @@ case class Translator(program: PProgram) {
               case _ => sys.error("type unification error - should report and not crash")
             }
           case _: Predicate =>
-            val inner = PredicateAccess(args.inner.toSeq map exp, findPredicate(func).name) (pos, info)
+            val inner = PredicateAccess(args.inner.toSeq map goExp, findPredicate(func).name) (pos, info)
             PredicateAccessPredicate(inner, None) (pos, info)
           case _ => sys.error("unexpected reference to non-function")
         }
       case PNewExp(_, _) => sys.error("unexpected `new` expression")
       case PUnfolding(_, loc, _, e) =>
-        Unfolding(exp(loc).asInstanceOf[PredicateAccessPredicate], exp(e))(pos, info)
+        Unfolding(goExp(loc).asInstanceOf[PredicateAccessPredicate], goExp(e))(pos, info)
       case PApplying(_, wand, _, e) =>
-        Applying(exp(wand).asInstanceOf[MagicWand], exp(e))(pos, info)
+        Applying(goExp(wand).asInstanceOf[MagicWand], goExp(e))(pos, info)
       case PAsserting(_, a, _, e) =>
-        Asserting(exp(a), exp(e))(pos, info)
+        Asserting(goExp(a), goExp(e))(pos, info)
       case pl@PLet(_, _, _, exp1, _, PLetNestedScope(body)) =>
-        Let(liftLogicalDecl(pl.decl), exp(exp1.inner), exp(body))(pos, info)
+        Let(liftLogicalDecl(pl.decl), goExp(exp1.inner), goExp(body))(pos, info)
       case _: PLetNestedScope =>
         sys.error("unexpected node PLetNestedScope, should only occur as a direct child of PLet nodes")
       case PExists(_, vars, _, triggers, e) =>
-        val ts = triggers map (t => Trigger((t.exp.inner.toSeq map exp) map (e => e match {
+        val ts = triggers map (t => Trigger((t.exp.inner.toSeq map goExp) map (e => e match {
           case PredicateAccessPredicate(inner, _) => inner
           case _ => e
         }))(t))
-        Exists(vars.toSeq map liftLogicalDecl, ts, exp(e))(pos, info)
+        Exists(vars.toSeq map liftLogicalDecl, ts, goExp(e))(pos, info)
       case PForall(_, vars, _, triggers, e) =>
-        val ts = triggers map (t => Trigger((t.exp.inner.toSeq map exp) map (e => e match {
+        val ts = triggers map (t => Trigger((t.exp.inner.toSeq map goExp) map (e => e match {
           case PredicateAccessPredicate(inner, _) => inner
           case _ => e
         }))(t))
-        val fa = Forall(vars.toSeq map liftLogicalDecl, ts, exp(e))(pos, info)
+        val fa = Forall(vars.toSeq map liftLogicalDecl, ts, goExp(e))(pos, info)
         if (fa.isPure) {
           fa
         } else {
@@ -556,21 +559,21 @@ case class Translator(program: PProgram) {
         }
       case fp@PForPerm(_, vars, _, _, e) =>
         val varList = vars.toSeq map liftLogicalDecl
-        exp(fp.accessRes) match {
-          case PredicateAccessPredicate(inner, _) => ForPerm(varList, inner, exp(e))(pos, info)
-          case f : FieldAccess => ForPerm(varList, f, exp(e))(pos, info)
-          case p : PredicateAccess => ForPerm(varList, p, exp(e))(pos, info)
-          case w : MagicWand => ForPerm(varList, w, exp(e))(pos, info)
+        goExp(fp.accessRes) match {
+          case PredicateAccessPredicate(inner, _) => ForPerm(varList, inner, goExp(e))(pos, info)
+          case f : FieldAccess => ForPerm(varList, f, goExp(e))(pos, info)
+          case p : PredicateAccess => ForPerm(varList, p, goExp(e))(pos, info)
+          case w : MagicWand => ForPerm(varList, w, goExp(e))(pos, info)
           case other =>
             sys.error(s"Internal Error: Unexpectedly found $other in forperm")
         }
       case POldExp(_, lbl, e) =>
-        val ee = exp(e.inner)
+        val ee = goExp(e.inner)
         lbl.map(l => LabelledOld(ee, l.inner.fold(_.rs.keyword, _.name))(pos, info)).getOrElse(Old(ee)(pos, info))
       case PCondExp(cond, _, thn, _, els) =>
-        CondExp(exp(cond), exp(thn), exp(els))(pos, info)
+        CondExp(goExp(cond), goExp(thn), goExp(els))(pos, info)
       case PCurPerm(_, res) =>
-        exp(res.inner) match {
+        goExp(res.inner) match {
           case PredicateAccessPredicate(inner, _) => CurrentPerm(inner)(pos, info)
           case x: FieldAccess => CurrentPerm(x)(pos, info)
           case x: PredicateAccess => CurrentPerm(x)(pos, info)
@@ -586,8 +589,8 @@ case class Translator(program: PProgram) {
       case PEpsilon(_) =>
         EpsilonPerm()(pos, info)
       case acc: PAccPred =>
-        val p = acc.permExp.map(exp)
-        exp(acc.loc) match {
+        val p = acc.permExp.map(goExp)
+        goExp(acc.loc) match {
           case loc@FieldAccess(_, _) =>
             FieldAccessPredicate(loc, p)(pos, info)
           case loc@PredicateAccess(_, _) =>
@@ -599,55 +602,55 @@ case class Translator(program: PProgram) {
       case _: PEmptySeq =>
         EmptySeq(ttyp(pexp.typ.asInstanceOf[PSeqType].elementType.inner))(pos, info)
       case PExplicitSeq(_, elems) =>
-        ExplicitSeq(elems.inner.toSeq map exp)(pos, info)
+        ExplicitSeq(elems.inner.toSeq map goExp)(pos, info)
       case PRangeSeq(_, low, _, high, _) =>
-        RangeSeq(exp(low), exp(high))(pos, info)
+        RangeSeq(goExp(low), goExp(high))(pos, info)
 
       case PLookup(base, _, index, _) => base.typ match {
-        case _: PSeqType => SeqIndex(exp(base), exp(index))(pos, info)
-        case _: PMapType => MapLookup(exp(base), exp(index))(pos, info)
+        case _: PSeqType => SeqIndex(goExp(base), goExp(index))(pos, info)
+        case _: PMapType => MapLookup(goExp(base), goExp(index))(pos, info)
         case t => sys.error(s"unexpected type $t")
       }
 
       case PSeqSlice(seq, _, s, _, e, _) =>
-        val es = exp(seq)
-        val ss = e.map(exp).map(SeqTake(es, _)(pos, info)).getOrElse(es)
-        s.map(exp).map(SeqDrop(ss, _)(pos, info)).getOrElse(ss)
+        val es = goExp(seq)
+        val ss = e.map(goExp).map(SeqTake(es, _)(pos, info)).getOrElse(es)
+        s.map(goExp).map(SeqDrop(ss, _)(pos, info)).getOrElse(ss)
 
       case PUpdate(base, _, key, _, value, _) => base.typ match {
-        case _: PSeqType => SeqUpdate(exp(base), exp(key), exp(value))(pos, info)
-        case _: PMapType => MapUpdate(exp(base), exp(key), exp(value))(pos, info)
+        case _: PSeqType => SeqUpdate(goExp(base), goExp(key), goExp(value))(pos, info)
+        case _: PMapType => MapUpdate(goExp(base), goExp(key), goExp(value))(pos, info)
         case t => sys.error(s"unexpected type $t")
       }
 
       case PSize(_, base, _) => base.typ match {
-        case _: PSeqType => SeqLength(exp(base))(pos, info)
-        case _: PMapType => MapCardinality(exp(base))(pos, info)
-        case _: PSetType | _: PMultisetType => AnySetCardinality(exp(base))(pos, info)
+        case _: PSeqType => SeqLength(goExp(base))(pos, info)
+        case _: PMapType => MapCardinality(goExp(base))(pos, info)
+        case _: PSetType | _: PMultisetType => AnySetCardinality(goExp(base))(pos, info)
         case t => sys.error(s"unexpected type $t")
       }
 
       case _: PEmptySet =>
         EmptySet(ttyp(pexp.typ.asInstanceOf[PSetType].elementType.inner))(pos, info)
       case PExplicitSet(_, elems) =>
-        ExplicitSet(elems.inner.toSeq map exp)(pos, info)
+        ExplicitSet(elems.inner.toSeq map goExp)(pos, info)
       case _: PEmptyMultiset =>
         EmptyMultiset(ttyp(pexp.typ.asInstanceOf[PMultisetType].elementType.inner))(pos, info)
       case PExplicitMultiset(_, elems) =>
-        ExplicitMultiset(elems.inner.toSeq map exp)(pos, info)
+        ExplicitMultiset(elems.inner.toSeq map goExp)(pos, info)
 
       case _: PEmptyMap => EmptyMap(
         ttyp(pexp.typ.asInstanceOf[PMapType].keyType),
         ttyp(pexp.typ.asInstanceOf[PMapType].valueType)
       )(pos, info)
       case PExplicitMap(_, elems) =>
-        ExplicitMap(elems.inner.toSeq map exp)(pos, info)
+        ExplicitMap(elems.inner.toSeq map goExp)(pos, info)
       case PMaplet(key, _, value) =>
-        Maplet(exp(key), exp(value))(pos, info)
+        Maplet(goExp(key), goExp(value))(pos, info)
       case PMapDomain(_, base) =>
-        MapDomain(exp(base.inner))(pos, info)
+        MapDomain(goExp(base.inner))(pos, info)
       case PMapRange(_, base) =>
-        MapRange(exp(base.inner))(pos, info)
+        MapRange(goExp(base.inner))(pos, info)
 
       case t: PExtender => t.translateExp(this)
     }

From e8b60a5e7c874da234caaebe016aaa750f5d3a12 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Tue, 31 Mar 2026 14:57:06 +0200
Subject: [PATCH 13/27] fix axioms

---
 src/main/scala/viper/silver/ast/Ast.scala     | 48 ++++++++++++++++++-
 .../viper/silver/parser/Translator.scala      |  4 +-
 2 files changed, 49 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 164739169..ca008c0ca 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -11,9 +11,11 @@ import scala.reflect.ClassTag
 import pretty.FastPrettyPrinter
 import utility._
 import viper.silver.ast
+import viper.silver.ast.EdgeType.EdgeType
+import viper.silver.ast.JoinType.JoinType
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
-import viper.silver.dependencyAnalysis.{AssumptionType, DependencyType}
+import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
 import viper.silver.dependencyAnalysis.DependencyType.{ExplicitAssertion, ExplicitAssumption, MethodCall, Rewrite, SourceCode}
 import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
@@ -446,6 +448,50 @@ case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
   override def isCached: Boolean = false
 }
 
+object JoinType extends Enumeration {
+  type JoinType = Value
+  val Source, Sink = Value
+}
+
+object EdgeType extends Enumeration {
+  type EdgeType = Value
+  val Up, Down = Value
+}
+
+
+trait DependencyAnalysisJoinInfo extends ast.Info {
+  override def comment: Seq[String] = Nil
+  override def isCached: Boolean = false
+
+  def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = {
+    (this, dependencyAnalysisJoinInfo) match {
+      case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) =>
+        sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1)
+    }
+  }
+}
+
+case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+
+trait DependencyAnalysisMergeInfo extends ast.Info {
+
+  def isMerge: Boolean
+
+  override def comment: Seq[String] = Nil
+  override def isCached: Boolean = false
+}
+
+case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo {
+  override def isMerge: Boolean = false
+}
+
+case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+  override def isMerge: Boolean = true
+}
+
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 924a9ca32..3a1ce76e4 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -9,7 +9,7 @@ package viper.silver.parser
 import viper.silver.FastMessaging
 import viper.silver.ast.utility._
 import viper.silver.ast.{SourcePosition, _}
-import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
+import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyAnalysisJoinNodeInfo, DependencyType}
 import viper.silver.plugin.standard.adt.{Adt, AdtType}
 
 import scala.collection.mutable
@@ -103,7 +103,7 @@ case class Translator(program: PProgram) {
 
   private def translate(a: PAxiom): DomainAxiom = {
     def attachInfo(axiom: DomainAxiom) = {
-      val info = ConsInfo(axiom.info, ConsInfo(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), DependencyTypeInfo(DependencyType.Axiom)))
+      val info = ConsInfo(axiom.info, ConsInfo(ConsInfo(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), DependencyTypeInfo(DependencyType.Axiom)), SimpleDependencyAnalysisJoin(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), JoinType.Source, EdgeType.Down)))
       axiom.withMeta(axiom.pos, info, axiom.errT)
     }
 

From 6fee57cb9fa06cc510cc87272b87618db30fe6f4 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 30 Mar 2026 20:16:54 +0200
Subject: [PATCH 14/27] refactoring

---
 .../ast/utility/ImpureAssumeRewriter.scala    |  2 +-
 .../silver/cfg/silver/CfgGenerator.scala      |  2 -
 .../AnalysisSourceInfo.scala                  | 26 -------------
 .../dependencyAnalysis/DependencyType.scala   |  1 +
 .../viper/silver/parser/Translator.scala      | 39 ++++++++++++-------
 5 files changed, 26 insertions(+), 44 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
index e3587c590..ff39a8834 100644
--- a/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
+++ b/src/main/scala/viper/silver/ast/utility/ImpureAssumeRewriter.scala
@@ -227,7 +227,7 @@ object ImpureAssumeRewriter {
     }).execute(p)
 
     val pAssume: Program = ViperStrategy.Slim({
-      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos))
+      case a: Assume => rewriteInhale(Inhale(rewrite(a.exp, pInvs))(a.pos, a.info, a.errT))
     }).execute(pInvs)
 
     if (funcs.isEmpty && domains.isEmpty) {
diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
index 36b17791c..727284162 100644
--- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
+++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
@@ -364,8 +364,6 @@ object CfgGenerator {
           case ConditionalJumpStmt(cond, thnTarget, elsTarget) =>
             current.foreach { currentIndex =>
               val negInfo = cond.pos match {
-//                case position: AbstractSourcePosition if cond.info.getUniqueInfo[DependencyAnalysisInfo].isEmpty => TODO ake
-//                  MakeInfoPair(cond.info, DependencyAnalysisInfo(cond.toString, position))
                 case _ => cond.info
               }
               val neg = Not(cond)(cond.pos, negInfo, cond.errT)
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
index 3c2ee2f22..dac6858e4 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
@@ -46,21 +46,6 @@ trait AnalysisSourceInfo extends ast.Info {
 
   def getPosition: Position
 
-  /**
-   * @return the analysis source info used for lifting low-level graphs to higher-level graphs
-   *         and presenting dependency results to the user
-   */
-  def getTopLevelSource: AnalysisSourceInfo = this
-
-  /**
-   * @return the analysis source info used for adding transitive edges within a source exp/stmt
-   */
-  def getSourceForTransitiveEdges: AnalysisSourceInfo = getTopLevelSource
-
-  /**
-   * @return the analysis source info used for joining graphs
-   */
-  def getFineGrainedSource: AnalysisSourceInfo = this
 
   def isAnalysisEnabled: Boolean = true
 
@@ -105,14 +90,3 @@ case class StringAnalysisSourceInfo(description: String, position: Position) ext
   override def getDescription: String = description.replaceAll("\n", "\t")
 }
 
-case class CompositeAnalysisSourceInfo(coarseGrainedSource: AnalysisSourceInfo, fineGrainedSource: AnalysisSourceInfo) extends AnalysisSourceInfo {
-  override def toString: String = getTopLevelSource.toString
-  override def getPosition: Position = coarseGrainedSource.getPosition
-
-  override def getTopLevelSource: AnalysisSourceInfo = coarseGrainedSource.getTopLevelSource
-  override def getFineGrainedSource: AnalysisSourceInfo = fineGrainedSource.getFineGrainedSource
-
-  override def isAnalysisEnabled: Boolean = coarseGrainedSource.isAnalysisEnabled && fineGrainedSource.isAnalysisEnabled
-
-  override def getDescription: String = coarseGrainedSource.getDescription
-}
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index 695db98e4..21b3aaaac 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -55,6 +55,7 @@ object DependencyType {
   val MethodCall: DependencyType = DependencyType(AssumptionType.MethodCall, AssumptionType.MethodCall)
   val Ghost: DependencyType = DependencyType.make(AssumptionType.Ghost)
   val Annotation: DependencyType = DependencyType.make(AssumptionType.Annotation)
+  val Axiom: DependencyType = DependencyType.make(AssumptionType.DomainAxiom)
 
   def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
 
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 20c24997a..7fb6cf303 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -101,11 +101,20 @@ case class Translator(program: PProgram) {
       dd
   }
 
-  private def translate(a: PAxiom): DomainAxiom = a match {
-    case pa@PAxiom(anns, _, Some(name), e) =>
-      NamedDomainAxiom(name.name, exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
-    case pa@PAxiom(anns, _, None, e) =>
-      AnonymousDomainAxiom(exp(e.e.inner))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+  private def translate(a: PAxiom): DomainAxiom = {
+    def attachInfo(axiom: DomainAxiom) = {
+      val info = ConsInfo(axiom.info, ConsInfo(AnalysisSourceInfo.createAnalysisSourceInfo(axiom.exp), DependencyTypeInfo(DependencyType.Axiom)))
+      axiom.withMeta(axiom.pos, info, axiom.errT)
+    }
+
+    a match {
+      case pa@PAxiom(anns, _, Some(name), e) =>
+        val axiom = NamedDomainAxiom(name.name, exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        attachInfo(axiom)
+      case pa@PAxiom(anns, _, None, e) =>
+        val axiom = AnonymousDomainAxiom(exp(e.e.inner, Some(DependencyType.make(AssumptionType.DomainAxiom))))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        attachInfo(axiom)
+    }
   }
 
   private def translate(f: PFunction): Function = f match {
@@ -210,22 +219,22 @@ case class Translator(program: PProgram) {
         }.flatten
         Seqn(seqn filterNot (_.isInstanceOf[PSkip]) map stmt, locals)(pos, info)
       case PFold(_, e) =>
-        Fold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info)
+        Fold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info)
       case PUnfold(_, e) =>
-        Unfold(exp(e).asInstanceOf[PredicateAccessPredicate])(pos, info)
+        Unfold(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[PredicateAccessPredicate])(pos, info)
       case PPackageWand(_, e, proofScript) =>
-        val wand = exp(e).asInstanceOf[MagicWand]
+        val wand = exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand]
         Package(wand, proofScript map (stmt(_).asInstanceOf[Seqn]) getOrElse Statements.EmptyStmt)(pos, info)
       case PApplyWand(_, e) =>
-        Apply(exp(e).asInstanceOf[MagicWand])(pos, info)
+        Apply(exp(e, Some(DependencyType.Rewrite)).asInstanceOf[MagicWand])(pos, info)
       case PInhale(_, e) =>
         Inhale(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PAssume(_, e) =>
         Assume(exp(e, Some(DependencyType.ExplicitAssumption)))(pos, info)
       case PExhale(_, e) =>
-        Exhale(exp(e))(pos, info)
+        Exhale(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info)
       case PAssert(_, e) =>
-        Assert(exp(e))(pos, info)
+        Assert(exp(e, Some(DependencyType.ExplicitAssertion)))(pos, info)
       case PLabel(_, name, invs) =>
         Label(name.name, invs.toSeq map (_.e) map exp)(pos, info)
       case PGoto(_, label) =>
@@ -355,11 +364,11 @@ case class Translator(program: PProgram) {
     val (pexp, annotationMap) = extractAnnotation(parseExp)
     val sourcePNodeInfo = SourcePNodeInfo(parseExp)
     val info0 = if (annotationMap.isEmpty) sourcePNodeInfo else ConsInfo(sourcePNodeInfo, AnnotationInfo(annotationMap))
-    val info = if(dependencyType.isDefined) ConsInfo(info0, DependencyTypeInfo(dependencyType.get)) else info0
-    expInternal(pexp, pos, info)
+    val info = if(dependencyType.isDefined) MakeInfoPair(info0, DependencyTypeInfo(dependencyType.get)) else info0
+    expInternal(pexp, pos, info, dependencyType)
   }
 
-  protected def expInternal(pexp: PExp, pos: PExp, info: Info): Exp = {
+  protected def expInternal(pexp: PExp, pos: PExp, info: Info, dependencyType: Option[DependencyType]): Exp = {
     val expr = pexp match {
       case PIdnUseExp(piu) =>
         piu.decl match {
@@ -369,7 +378,7 @@ case class Translator(program: PProgram) {
           case _ => sys.error("should not occur in type-checked program")
         }
       case pbe @ PBinExp(left, op, right) =>
-        val (l, r) = (exp(left), exp(right))
+        val (l, r) = (exp(left, dependencyType), exp(right, dependencyType))
         op.rs match {
           case PSymOp.Plus =>
             r.typ match {

From 68cd5f289228c0a8255d9f9ede68e3a09f0f0b86 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Thu, 9 Apr 2026 10:54:42 +0200
Subject: [PATCH 15/27] make method calls more precise by separating it from
 argument evaluation

---
 src/main/scala/viper/silver/ast/Ast.scala | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index ca008c0ca..4db093dd0 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -6,21 +6,22 @@
 
 package viper.silver.ast
 
-import scala.collection.mutable
-import scala.reflect.ClassTag
-import pretty.FastPrettyPrinter
-import utility._
 import viper.silver.ast
 import viper.silver.ast.EdgeType.EdgeType
 import viper.silver.ast.JoinType.JoinType
+import viper.silver.ast.pretty.FastPrettyPrinter
+import viper.silver.ast.utility._
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
-import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
 import viper.silver.dependencyAnalysis.DependencyType.{ExplicitAssertion, ExplicitAssumption, MethodCall, Rewrite, SourceCode}
+import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
 import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
 
+import scala.collection.mutable
+import scala.reflect.ClassTag
+
 /*
 
 This is the Viper abstract syntax description.
@@ -492,6 +493,17 @@ case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends
   override def isMerge: Boolean = true
 }
 
+object SimpleDependencyAnalysisMerge {
+	def attachExpMergeInfo(exps: Seq[ast.Exp]): Seq[ast.Exp] = {
+		exps.map(attachExpMergeInfo)
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp): ast.Exp = {
+		val mergeInfo = SimpleDependencyAnalysisMerge(AnalysisSourceInfo.createAnalysisSourceInfo(exp))
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
+}
+
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment

From f1ef6668997b902d59fc46bba8aec12e59fc5e1a Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Thu, 9 Apr 2026 11:50:22 +0200
Subject: [PATCH 16/27] make function calls more precise by separating it from
 argument evaluation

---
 src/main/scala/viper/silver/ast/Ast.scala | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 4db093dd0..004796d71 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -502,6 +502,11 @@ object SimpleDependencyAnalysisMerge {
 		val mergeInfo = SimpleDependencyAnalysisMerge(AnalysisSourceInfo.createAnalysisSourceInfo(exp))
 		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
 	}
+
+	def attachExpMergeInfo(exp: ast.Exp, source: AnalysisSourceInfo): ast.Exp = {
+		val mergeInfo = SimpleDependencyAnalysisMerge(source)
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
 }
 
 /** An `Info` instance for composing multiple `Info`s together */

From f90274bf856cd3e89f77b6de84f3e325bcf79523 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Thu, 9 Apr 2026 15:57:16 +0200
Subject: [PATCH 17/27] refactor interpreter and user tool

---
 .../scala/viper/silver/dependencyAnalysis/DependencyType.scala  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index 21b3aaaac..e60d88773 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -45,7 +45,7 @@ object DependencyType {
   val Implicit: DependencyType = DependencyType(AssumptionType.Implicit, AssumptionType.Implicit)
   val SourceCode: DependencyType = DependencyType(AssumptionType.SourceCode, AssumptionType.SourceCode)
   val Explicit: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Explicit)
-  val ExplicitAssertion: DependencyType = DependencyType(AssumptionType.Ghost, AssumptionType.Explicit)
+  val ExplicitAssertion: DependencyType = DependencyType(AssumptionType.Internal, AssumptionType.Explicit)
   val ExplicitAssumption: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Implicit)
   val PathCondition: DependencyType = DependencyType(AssumptionType.PathCondition, AssumptionType.Implicit)
   val Invariant: DependencyType = DependencyType(AssumptionType.LoopInvariant, AssumptionType.LoopInvariant)

From 75f02f321e60619b49892720493d83d1ac1ca28a Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 10 Apr 2026 14:08:52 +0200
Subject: [PATCH 18/27] fix for method and function calls

---
 src/main/scala/viper/silver/ast/Ast.scala     | 23 ++++++++++++-------
 .../dependencyAnalysis/DependencyType.scala   |  2 +-
 2 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 004796d71..09436d458 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -493,18 +493,25 @@ case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends
   override def isMerge: Boolean = true
 }
 
-object SimpleDependencyAnalysisMerge {
-	def attachExpMergeInfo(exps: Seq[ast.Exp]): Seq[ast.Exp] = {
-		exps.map(attachExpMergeInfo)
+case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+object DependencyAnalysisMergeInfo {
+	def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = {
+		exps.map(attachExpMergeInfo(_, sourceInfo2))
 	}
 
-	def attachExpMergeInfo(exp: ast.Exp): ast.Exp = {
-		val mergeInfo = SimpleDependencyAnalysisMerge(AnalysisSourceInfo.createAnalysisSourceInfo(exp))
-		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp)
+		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
 	}
 
-	def attachExpMergeInfo(exp: ast.Exp, source: AnalysisSourceInfo): ast.Exp = {
-		val mergeInfo = SimpleDependencyAnalysisMerge(source)
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val mergeInfo = if(sourceInfo2.isDefined)
+			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)
+		else
+			SimpleDependencyAnalysisMerge(sourceInfo1)
 		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
 	}
 }
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index e60d88773..b98a8dc97 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -13,7 +13,7 @@ object AssumptionType extends Enumeration {
   def internalTypes: Set[AssumptionType] = Set(Internal, Trigger, CustomInternal) // will always be hidden from user
   def joinConditionTypes: Set[AssumptionType] = preconditionTypes ++ postconditionTypes ++ Set(FunctionBody, MethodCall)
   def importedTypes: Set[AssumptionType] = Set(ImportedPostcondition)
-  def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation)
+  def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody /* TODO ake: review */, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation)
   def sourceCodeTypes: Set[AssumptionType] = AssumptionType.values.diff(explicitAssumptionTypes ++ explicitAssertionTypes ++ verificationAnnotationTypes ++ internalTypes)
 
   def getMaxPriorityAssumptionType(types: Set[AssumptionType]): Option[AssumptionType] = {

From f63ebf53b4114d5c8b9672a4424f2be9cbb114b7 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 10 Apr 2026 17:02:18 +0200
Subject: [PATCH 19/27] add documentation and cleanup unused code

---
 src/main/scala/viper/silver/ast/Ast.scala     | 10 +++++--
 .../AbstractReadOnlyDependencyGraph.scala     |  5 ----
 .../dependencyAnalysis/DependencyType.scala   | 30 -------------------
 3 files changed, 8 insertions(+), 37 deletions(-)
 delete mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 09436d458..11b80048e 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -459,7 +459,10 @@ object EdgeType extends Enumeration {
   val Up, Down = Value
 }
 
-
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of
+ * individual verification components. Nodes with matching join information are connected by an interprocedural edge.
+ */
 trait DependencyAnalysisJoinInfo extends ast.Info {
   override def comment: Seq[String] = Nil
   override def isCached: Boolean = false
@@ -476,7 +479,10 @@ case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeTyp
 
 case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
 
-
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural
+ * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge.
+ */
 trait DependencyAnalysisMergeInfo extends ast.Info {
 
   def isMerge: Boolean
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala b/src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala
deleted file mode 100644
index 2d256f377..000000000
--- a/src/main/scala/viper/silver/dependencyAnalysis/AbstractReadOnlyDependencyGraph.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package viper.silver.dependencyAnalysis
-
-trait AbstractReadOnlyDependencyGraph {}
-
-trait AbstractDependencyAnalysisNode {}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index b98a8dc97..481357cdd 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -11,15 +11,10 @@ object AssumptionType extends Enumeration {
   def preconditionTypes: Set[AssumptionType] = Set(Precondition)
   def explicitAssertionTypes: Set[AssumptionType] = Set(Explicit, ImplicitPostcondition, ExplicitPostcondition)
   def internalTypes: Set[AssumptionType] = Set(Internal, Trigger, CustomInternal) // will always be hidden from user
-  def joinConditionTypes: Set[AssumptionType] = preconditionTypes ++ postconditionTypes ++ Set(FunctionBody, MethodCall)
   def importedTypes: Set[AssumptionType] = Set(ImportedPostcondition)
   def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody /* TODO ake: review */, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation)
   def sourceCodeTypes: Set[AssumptionType] = AssumptionType.values.diff(explicitAssumptionTypes ++ explicitAssertionTypes ++ verificationAnnotationTypes ++ internalTypes)
 
-  def getMaxPriorityAssumptionType(types: Set[AssumptionType]): Option[AssumptionType] = {
-    val priorityList = List(ExplicitPostcondition, Explicit) ++ internalTypes.toList ++ verificationAnnotationTypes.toList ++ sourceCodeTypes.toList ++ values.toList
-    priorityList.find(t => types.contains(t))
-  }
 
   def getPostcondType(isAbstractFunction: Boolean, dependencyType: Option[DependencyType]=None, isImported: Boolean=false): AssumptionType = {
     if(isImported) return ImportedPostcondition
@@ -41,7 +36,6 @@ object AssumptionType extends Enumeration {
 import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType
 
 object DependencyType {
-
   val Implicit: DependencyType = DependencyType(AssumptionType.Implicit, AssumptionType.Implicit)
   val SourceCode: DependencyType = DependencyType(AssumptionType.SourceCode, AssumptionType.SourceCode)
   val Explicit: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Explicit)
@@ -58,30 +52,6 @@ object DependencyType {
   val Axiom: DependencyType = DependencyType.make(AssumptionType.DomainAxiom)
 
   def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
-
-//  def get(stmt: ast.Stmt): DependencyType = {
-//    val annotatedDependencyType = DependencyAnalyzer.extractDependencyTypeFromInfo(stmt.info)
-//    if(annotatedDependencyType.isDefined) return annotatedDependencyType.get
-//
-//    stmt match {
-//      case _: ast.MethodCall => MethodCall
-//      case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
-//      case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
-//      case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
-//      case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
-//      case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
-//      case _ => DependencyType.make(Unknown) /* TODO: should not happen */
-//    }
-//  }
-//
-//  def get(exp: ast.Exp, dependencyType: DependencyType): DependencyType = DependencyAnalyzer.extractDependencyTypeFromInfo(exp.info).getOrElse(dependencyType)
-
-  def getMaxPriorityType(types: Set[DependencyType]): Option[DependencyType] = {
-    val assumptionType = AssumptionType.getMaxPriorityAssumptionType(types.map(_.assumptionType))
-    val assertionType = AssumptionType.getMaxPriorityAssumptionType(types.map(_.assertionType))
-    if(assumptionType.isDefined && assertionType.isDefined) Some(DependencyType(assumptionType.get, assertionType.get)) else None
-  }
-
 }
 
 case class DependencyType(assumptionType: AssumptionType, assertionType: AssumptionType)
\ No newline at end of file

From b2584ff4d43bcb62639d585e9377a275d7068c54 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 10 Apr 2026 18:22:53 +0200
Subject: [PATCH 20/27] adapt Gobra DA implementation to new design

---
 .../AnalysisSourceInfo.scala                   | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
index dac6858e4..f009ac9bf 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
@@ -14,17 +14,13 @@ object AnalysisSourceInfo {
     }
   }
 
-  def createAnalysisSourceInfo(exp: ast.Exp): AnalysisSourceInfo = {
-    val depInfo = exp.info.getUniqueInfo[FrontendDependencyAnalysisInfo]
-    if(depInfo.isDefined) depInfo.get.getAnalysisSourceInfo
-    else ExpAnalysisSourceInfo(exp, exp.pos)
-  }
-
-  def createAnalysisSourceInfo(stmt: ast.Stmt): AnalysisSourceInfo = {
-    val depInfo = stmt.info.getUniqueInfo[FrontendDependencyAnalysisInfo]
-    if(depInfo.isDefined) depInfo.get.getAnalysisSourceInfo
-    else StmtAnalysisSourceInfo(stmt, stmt.pos)
-  }
+	def createAnalysisSourceInfo(node: ast.Node): AnalysisSourceInfo = {
+		node match {
+			case stmt: ast.Stmt => StmtAnalysisSourceInfo(stmt, stmt.pos)
+			case exp: ast.Exp => ExpAnalysisSourceInfo(exp, exp.pos)
+			case _ => createAnalysisSourceInfo("Unknown", NoPosition)
+		}
+	}
 
   def createAnalysisSourceInfo(description: String, pos: Position): AnalysisSourceInfo = StringAnalysisSourceInfo(description, pos)
 

From 711854a175d258de2ed1ccfa689c41469ce24c89 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 10 Apr 2026 21:35:52 +0200
Subject: [PATCH 21/27] adapt solution for Gobra interfaces

---
 src/main/scala/viper/silver/ast/Ast.scala     |  99 ----------------
 .../DependencyAnalysisInfo.scala              | 110 ++++++++++++++++++
 .../viper/silver/parser/Translator.scala      |   2 +-
 3 files changed, 111 insertions(+), 100 deletions(-)
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 11b80048e..df179325a 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -6,15 +6,10 @@
 
 package viper.silver.ast
 
-import viper.silver.ast
-import viper.silver.ast.EdgeType.EdgeType
-import viper.silver.ast.JoinType.JoinType
 import viper.silver.ast.pretty.FastPrettyPrinter
 import viper.silver.ast.utility._
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
-import viper.silver.dependencyAnalysis.DependencyType.{ExplicitAssertion, ExplicitAssumption, MethodCall, Rewrite, SourceCode}
-import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
 import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
@@ -428,100 +423,6 @@ abstract class FailureExpectedInfo extends Info {
   override val isCached = false
 }
 
-object DependencyTypeInfo {
-  def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = {
-    val depType = stmt match {
-      case _: ast.MethodCall => MethodCall
-      case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
-      case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
-      case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
-      case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
-      case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
-      case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
-    }
-    DependencyTypeInfo(depType)
-  }
-}
-
-case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
-
-  override def comment: Seq[String] = Nil
-  override def isCached: Boolean = false
-}
-
-object JoinType extends Enumeration {
-  type JoinType = Value
-  val Source, Sink = Value
-}
-
-object EdgeType extends Enumeration {
-  type EdgeType = Value
-  val Up, Down = Value
-}
-
-/**
- * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of
- * individual verification components. Nodes with matching join information are connected by an interprocedural edge.
- */
-trait DependencyAnalysisJoinInfo extends ast.Info {
-  override def comment: Seq[String] = Nil
-  override def isCached: Boolean = false
-
-  def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = {
-    (this, dependencyAnalysisJoinInfo) match {
-      case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) =>
-        sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1)
-    }
-  }
-}
-
-case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
-
-case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
-
-/**
- * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural
- * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge.
- */
-trait DependencyAnalysisMergeInfo extends ast.Info {
-
-  def isMerge: Boolean
-
-  override def comment: Seq[String] = Nil
-  override def isCached: Boolean = false
-}
-
-case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo {
-  override def isMerge: Boolean = false
-}
-
-case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
-  override def isMerge: Boolean = true
-}
-
-case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
-	override def isMerge: Boolean = true
-}
-
-object DependencyAnalysisMergeInfo {
-	def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = {
-		exps.map(attachExpMergeInfo(_, sourceInfo2))
-	}
-
-	def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
-		val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp)
-		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
-	}
-
-	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
-		val mergeInfo = if(sourceInfo2.isDefined)
-			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)
-		else
-			SimpleDependencyAnalysisMerge(sourceInfo1)
-		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
-	}
-}
-
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
new file mode 100644
index 000000000..f78401093
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
@@ -0,0 +1,110 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast
+import viper.silver.dependencyAnalysis.DependencyType._
+import viper.silver.dependencyAnalysis.EdgeType.EdgeType
+import viper.silver.dependencyAnalysis.JoinType.JoinType
+
+object DependencyTypeInfo {
+	def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = {
+		val depType = stmt match {
+			case _: ast.MethodCall => MethodCall
+			case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
+			case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
+			case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
+			case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
+			case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
+			case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
+		}
+		DependencyTypeInfo(depType)
+	}
+}
+
+case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+object JoinType extends Enumeration {
+	type JoinType = Value
+	val Source, Sink = Value
+}
+
+object EdgeType extends Enumeration {
+	type EdgeType = Value
+	val Up, Down = Value
+}
+
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of
+ * individual verification components. Nodes with matching join information are connected by an interprocedural edge.
+ */
+trait DependencyAnalysisJoinInfo extends ast.Info {
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+
+	def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = {
+		(this, dependencyAnalysisJoinInfo) match {
+			case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) =>
+				sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1)
+		}
+	}
+}
+
+case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural
+ * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge.
+ */
+trait DependencyAnalysisMergeInfo extends ast.Info {
+
+	def isMerge: Boolean
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = false
+}
+
+case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+object DependencyAnalysisMergeInfo {
+	def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = {
+		exps.map(attachExpMergeInfo(_, sourceInfo2))
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp)
+		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val mergeInfo = if(sourceInfo2.isDefined)
+			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)
+		else
+			SimpleDependencyAnalysisMerge(sourceInfo1)
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
+}
+
+trait AdditionalDependencyNodeInfo extends ast.Info {
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+case class AdditionalAssertionNode() extends AdditionalDependencyNodeInfo
+
+case class AdditionalAssumptionNode() extends AdditionalDependencyNodeInfo
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 3a1ce76e4..be4a698f1 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -9,7 +9,7 @@ package viper.silver.parser
 import viper.silver.FastMessaging
 import viper.silver.ast.utility._
 import viper.silver.ast.{SourcePosition, _}
-import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyAnalysisJoinNodeInfo, DependencyType}
+import viper.silver.dependencyAnalysis._
 import viper.silver.plugin.standard.adt.{Adt, AdtType}
 
 import scala.collection.mutable

From dca53b2ab1521010531fa8a597de0ba0ad4245d3 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Fri, 10 Apr 2026 21:35:52 +0200
Subject: [PATCH 22/27] adapt solution for Gobra interfaces

---
 src/main/scala/viper/silver/ast/Ast.scala     |  99 ----------------
 .../DependencyAnalysisInfo.scala              | 110 ++++++++++++++++++
 .../FrontendDependencyAnalysisInfo.scala      |  50 --------
 .../viper/silver/parser/Translator.scala      |   2 +-
 4 files changed, 111 insertions(+), 150 deletions(-)
 create mode 100644 src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
 delete mode 100644 src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala

diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala
index 11b80048e..df179325a 100644
--- a/src/main/scala/viper/silver/ast/Ast.scala
+++ b/src/main/scala/viper/silver/ast/Ast.scala
@@ -6,15 +6,10 @@
 
 package viper.silver.ast
 
-import viper.silver.ast
-import viper.silver.ast.EdgeType.EdgeType
-import viper.silver.ast.JoinType.JoinType
 import viper.silver.ast.pretty.FastPrettyPrinter
 import viper.silver.ast.utility._
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder, Traverse}
-import viper.silver.dependencyAnalysis.DependencyType.{ExplicitAssertion, ExplicitAssumption, MethodCall, Rewrite, SourceCode}
-import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyType}
 import viper.silver.parser.PNode
 import viper.silver.verifier.errors.ErrorNode
 import viper.silver.verifier.{AbstractVerificationError, ConsistencyError, ErrorReason}
@@ -428,100 +423,6 @@ abstract class FailureExpectedInfo extends Info {
   override val isCached = false
 }
 
-object DependencyTypeInfo {
-  def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = {
-    val depType = stmt match {
-      case _: ast.MethodCall => MethodCall
-      case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
-      case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
-      case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
-      case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
-      case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
-      case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
-    }
-    DependencyTypeInfo(depType)
-  }
-}
-
-case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
-
-  override def comment: Seq[String] = Nil
-  override def isCached: Boolean = false
-}
-
-object JoinType extends Enumeration {
-  type JoinType = Value
-  val Source, Sink = Value
-}
-
-object EdgeType extends Enumeration {
-  type EdgeType = Value
-  val Up, Down = Value
-}
-
-/**
- * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of
- * individual verification components. Nodes with matching join information are connected by an interprocedural edge.
- */
-trait DependencyAnalysisJoinInfo extends ast.Info {
-  override def comment: Seq[String] = Nil
-  override def isCached: Boolean = false
-
-  def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = {
-    (this, dependencyAnalysisJoinInfo) match {
-      case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) =>
-        sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1)
-    }
-  }
-}
-
-case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
-
-case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
-
-/**
- * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural
- * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge.
- */
-trait DependencyAnalysisMergeInfo extends ast.Info {
-
-  def isMerge: Boolean
-
-  override def comment: Seq[String] = Nil
-  override def isCached: Boolean = false
-}
-
-case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo {
-  override def isMerge: Boolean = false
-}
-
-case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
-  override def isMerge: Boolean = true
-}
-
-case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
-	override def isMerge: Boolean = true
-}
-
-object DependencyAnalysisMergeInfo {
-	def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = {
-		exps.map(attachExpMergeInfo(_, sourceInfo2))
-	}
-
-	def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
-		val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp)
-		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
-	}
-
-	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
-		val mergeInfo = if(sourceInfo2.isDefined)
-			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)
-		else
-			SimpleDependencyAnalysisMerge(sourceInfo1)
-		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
-	}
-}
-
 /** An `Info` instance for composing multiple `Info`s together */
 case class ConsInfo(head: Info, tail: Info) extends Info {
   override val comment = head.comment ++ tail.comment
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
new file mode 100644
index 000000000..f78401093
--- /dev/null
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
@@ -0,0 +1,110 @@
+package viper.silver.dependencyAnalysis
+
+import viper.silver.ast
+import viper.silver.dependencyAnalysis.DependencyType._
+import viper.silver.dependencyAnalysis.EdgeType.EdgeType
+import viper.silver.dependencyAnalysis.JoinType.JoinType
+
+object DependencyTypeInfo {
+	def getDependencyTypeInfo(stmt: ast.Stmt): DependencyTypeInfo = {
+		val depType = stmt match {
+			case _: ast.MethodCall => MethodCall
+			case  _: ast.NewStmt | _: ast.AbstractAssign => SourceCode
+			case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
+			case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
+			case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
+			case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
+			case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
+		}
+		DependencyTypeInfo(depType)
+	}
+}
+
+case class DependencyTypeInfo(dependencyType: DependencyType) extends ast.Info {
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+object JoinType extends Enumeration {
+	type JoinType = Value
+	val Source, Sink = Value
+}
+
+object EdgeType extends Enumeration {
+	type EdgeType = Value
+	val Up, Down = Value
+}
+
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to join dependency graphs of
+ * individual verification components. Nodes with matching join information are connected by an interprocedural edge.
+ */
+trait DependencyAnalysisJoinInfo extends ast.Info {
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+
+	def matches(dependencyAnalysisJoinInfo: DependencyAnalysisJoinInfo) = {
+		(this, dependencyAnalysisJoinInfo) match {
+			case (SimpleDependencyAnalysisJoin(sourceInfo, joinType, edgeType), SimpleDependencyAnalysisJoin(sourceInfo1, joinType1, edgeType1)) =>
+				sourceInfo.equals(sourceInfo1) && edgeType.equals(edgeType1)
+		}
+	}
+}
+
+case class EvalStackDependencyAnalysisJoin(joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+case class SimpleDependencyAnalysisJoin(sourceInfo: AnalysisSourceInfo, joinType: JoinType, edgeType: EdgeType) extends DependencyAnalysisJoinInfo
+
+/**
+ * Represent the piece of information to be stored in dependency nodes in order to finalize the intraprocedural
+ * dependency graph. Nodes with matching merge information are connected by an intraprocedural edge.
+ */
+trait DependencyAnalysisMergeInfo extends ast.Info {
+
+	def isMerge: Boolean
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+case class NoDependencyAnalysisMerge() extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = false
+}
+
+case class SimpleDependencyAnalysisMerge(sourceInfo: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+case class CompositeDependencyAnalysisMergeInfo(sourceInfo1: AnalysisSourceInfo, sourceInfo2: AnalysisSourceInfo) extends DependencyAnalysisMergeInfo {
+	override def isMerge: Boolean = true
+}
+
+object DependencyAnalysisMergeInfo {
+	def attachExpMergeInfo(exps: Seq[ast.Exp], sourceInfo2: Option[AnalysisSourceInfo]): Seq[ast.Exp] = {
+		exps.map(attachExpMergeInfo(_, sourceInfo2))
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val expSourceInfo = AnalysisSourceInfo.createAnalysisSourceInfo(exp)
+		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
+	}
+
+	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
+		val mergeInfo = if(sourceInfo2.isDefined)
+			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)
+		else
+			SimpleDependencyAnalysisMerge(sourceInfo1)
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
+}
+
+trait AdditionalDependencyNodeInfo extends ast.Info {
+
+	override def comment: Seq[String] = Nil
+	override def isCached: Boolean = false
+}
+
+case class AdditionalAssertionNode() extends AdditionalDependencyNodeInfo
+
+case class AdditionalAssumptionNode() extends AdditionalDependencyNodeInfo
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala
deleted file mode 100644
index b2993426d..000000000
--- a/src/main/scala/viper/silver/dependencyAnalysis/FrontendDependencyAnalysisInfo.scala
+++ /dev/null
@@ -1,50 +0,0 @@
-package viper.silver.dependencyAnalysis
-
-import viper.silver.ast.{Info, Position}
-import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType
-
-abstract class FrontendDependencyAnalysisInfo extends Info {
-  override val comment = Nil
-  override val isCached = false
-
-  val info: String
-  val pos: Position
-  val dependencyType: Option[DependencyType]=None
-
-  def getAnalysisSourceInfo: AnalysisSourceInfo
-}
-
-case class SimpleFrontendDependencyAnalysisInfo(sourceInfo: AnalysisSourceInfo, _dependencyType: DependencyType) extends FrontendDependencyAnalysisInfo {
-
-  override val info: String = sourceInfo.toString
-  override val pos: Position = sourceInfo.getPosition
-  override val dependencyType: Option[DependencyType] = Some(_dependencyType)
-
-  override def getAnalysisSourceInfo: AnalysisSourceInfo = sourceInfo
-}
-
-/*
- Viper statements / expressions with a DependencyAnalysisJoinNodeInfo will produce an assertion and assumption node with the given source info and dependency type,
- and with isJoinNode set to true.
- The idea is that these nodes can be used to join graphs without the need for an explicit method call.
- We use this, for example, for Gobra interfaces and implementation proofs.
- */
-case class DependencyAnalysisJoinNodeInfo(sourceInfo: AnalysisSourceInfo, _dependencyType: DependencyType) extends FrontendDependencyAnalysisInfo {
-//  def getAssertionNode: GeneralAssertionNode =
-//    SimpleAssertionNode(True, sourceInfo, AssumptionType.CustomInternal, isClosed=false, isJoinNode=true)
-//
-//  def getAssertionNode(outerSourceInfo: AnalysisSourceInfo): GeneralAssertionNode =
-//    SimpleAssertionNode(True, CompositeAnalysisSourceInfo(outerSourceInfo, sourceInfo), AssumptionType.CustomInternal,  isClosed=false, isJoinNode=true)
-//
-//  def getAssertionNode(outerSourceInfo: AnalysisSourceInfo, assumptionType: AssumptionType): GeneralAssertionNode =
-//    SimpleAssertionNode(True, CompositeAnalysisSourceInfo(outerSourceInfo, sourceInfo), assumptionType,  isClosed=false, isJoinNode=true)
-//
-//  def getAssumptionNode(outerSourceInfo: AnalysisSourceInfo): GeneralAssumptionNode =
-//    SimpleAssumptionNode(True, None, CompositeAnalysisSourceInfo(outerSourceInfo, sourceInfo), AssumptionType.CustomInternal, isClosed=false, isJoinNode=true)
-
-  override val info: String = sourceInfo.toString
-  override val pos: Position = sourceInfo.getPosition
-  override val dependencyType: Option[DependencyType] = Some(_dependencyType)
-
-  override def getAnalysisSourceInfo: AnalysisSourceInfo = sourceInfo
-}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index 3a1ce76e4..be4a698f1 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -9,7 +9,7 @@ package viper.silver.parser
 import viper.silver.FastMessaging
 import viper.silver.ast.utility._
 import viper.silver.ast.{SourcePosition, _}
-import viper.silver.dependencyAnalysis.{AnalysisSourceInfo, AssumptionType, DependencyAnalysisJoinNodeInfo, DependencyType}
+import viper.silver.dependencyAnalysis._
 import viper.silver.plugin.standard.adt.{Adt, AdtType}
 
 import scala.collection.mutable

From acb3d686e93cac74863f40640d43e16f17784a7e Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Sun, 12 Apr 2026 17:14:53 +0200
Subject: [PATCH 23/27] fixes

---
 .../silver/dependencyAnalysis/DependencyAnalysisInfo.scala    | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
index f78401093..3b4cea5c3 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
@@ -90,6 +90,10 @@ object DependencyAnalysisMergeInfo {
 		attachExpMergeInfo(exp, expSourceInfo, sourceInfo2)
 	}
 
+	def attachExpMergeInfo(exp: ast.Exp, mergeInfo: DependencyAnalysisMergeInfo): ast.Exp = {
+		exp.withMeta((exp.pos, ast.MakeInfoPair(mergeInfo, exp.info), exp.errT))
+	}
+
 	def attachExpMergeInfo(exp: ast.Exp, sourceInfo1: AnalysisSourceInfo, sourceInfo2: Option[AnalysisSourceInfo]): ast.Exp = {
 		val mergeInfo = if(sourceInfo2.isDefined)
 			CompositeDependencyAnalysisMergeInfo(sourceInfo1, sourceInfo2.get)

From 13725ae1cf6301623fb78ffaefae337e9efa8767 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 20 Apr 2026 10:29:23 +0200
Subject: [PATCH 24/27] fix withMeta for BackendFuncApp

---
 .../scala/viper/silver/ast/utility/rewriter/Rewritable.scala | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
index b1e450328..296f08cb0 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
@@ -6,8 +6,8 @@
 
 package viper.silver.ast.utility.rewriter
 
+import viper.silver.ast._
 import viper.silver.parser.PNode
-import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, DomainMember, ErrorTrafo, FuncApp, Info, Node, Position}
 
 import scala.reflect.runtime.{universe => reflection}
 
@@ -45,7 +45,7 @@ trait Rewritable extends Product {
         // Add additional arguments to constructor call, besides children
         val firstArgList = children
         var secondArgList = Seq.empty[Any]
-        import viper.silver.ast.{DomainType, DomainAxiom, FuncApp, DomainFunc, DomainFuncApp}
+        import viper.silver.ast.{DomainAxiom, DomainFunc, DomainFuncApp, DomainType, FuncApp}
         this match {
           // TODO: remove the following cases by implementing `HasExtraValList` on the respective classes
           case dt: DomainType => secondArgList = Seq(dt.typeParameters)
@@ -112,6 +112,7 @@ trait Rewritable extends Product {
       val arguments = this match {
         case fa: FuncApp => this.children ++ Seq(pos, info, fa.typ, trafo)
         case df: DomainFuncApp => this.children ++ Seq(pos, info, df.typ, df.domainName, trafo)
+				case bfa: BackendFuncApp => this.children ++ Seq(pos, info, bfa.typ, bfa.interpretation, trafo)
         case dm: DomainMember => this.children ++ Seq(pos, info, dm.domainName, trafo)
         case _ => this.children ++ Seq(pos, info, trafo)
       }

From 65e523a6fe967cf33a261b16d84aa2815b3ddf85 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Mon, 20 Apr 2026 10:41:04 +0200
Subject: [PATCH 25/27] fix withMeta for Adt plugin

---
 .../scala/viper/silver/ast/utility/rewriter/Rewritable.scala | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
index 296f08cb0..7a78a6585 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala
@@ -8,6 +8,7 @@ package viper.silver.ast.utility.rewriter
 
 import viper.silver.ast._
 import viper.silver.parser.PNode
+import viper.silver.plugin.standard.adt.{AdtConstructor, AdtConstructorApp, AdtDestructorApp, AdtDiscriminatorApp}
 
 import scala.reflect.runtime.{universe => reflection}
 
@@ -114,6 +115,10 @@ trait Rewritable extends Product {
         case df: DomainFuncApp => this.children ++ Seq(pos, info, df.typ, df.domainName, trafo)
 				case bfa: BackendFuncApp => this.children ++ Seq(pos, info, bfa.typ, bfa.interpretation, trafo)
         case dm: DomainMember => this.children ++ Seq(pos, info, dm.domainName, trafo)
+				case d: AdtDiscriminatorApp => this.children ++ Seq(pos, info, d.adtName, trafo)
+				case d: AdtConstructor => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo)
+				case d: AdtConstructorApp => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo)
+				case d: AdtDestructorApp => this.children ++ Seq(pos, info, d.typ, d.adtName, trafo)
         case _ => this.children ++ Seq(pos, info, trafo)
       }
 

From 5c1eeb66a0b7033ee0de117f4b2a352d8551c874 Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Tue, 12 May 2026 08:42:05 +0200
Subject: [PATCH 26/27] clean up silver

---
 .../viper/silver/ast/utility/Statements.scala | 31 -------------------
 .../silver/cfg/silver/CfgGenerator.scala      |  9 ++----
 .../AnalysisSourceInfo.scala                  |  8 -----
 .../DependencyAnalysisInfo.scala              |  2 +-
 .../dependencyAnalysis/DependencyType.scala   | 29 ++++++++---------
 .../viper/silver/parser/Translator.scala      |  2 +-
 6 files changed, 18 insertions(+), 63 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/Statements.scala b/src/main/scala/viper/silver/ast/utility/Statements.scala
index 633afcfca..4cd741e40 100644
--- a/src/main/scala/viper/silver/ast/utility/Statements.scala
+++ b/src/main/scala/viper/silver/ast/utility/Statements.scala
@@ -87,35 +87,4 @@ object Statements {
 
     writtenTo.distinct
   }
-
-  def hasProofObligations(s: Stmt, p: Program): Boolean = {
-    def goE(exp: Exp): Boolean = !Expressions.isKnownWellDefined(exp, Some(p))
-
-    def goEs(exps: Seq[Exp]): Boolean = exps exists goE
-
-    s match {
-      case _: FieldAssign | _: Exhale | _: Assert | _: Fold | _: Unfold | _: Package | _: Apply => true
-      case NewStmt(lhs, _) => goE(lhs)
-      case LocalVarAssign(lhs, rhs) => goE(lhs) || goE(rhs)
-      case MethodCall(methodName, args, targets) => p.findMethod(methodName).pres.nonEmpty || goEs(args) || goEs(targets)
-      case Inhale(exp) => goE(exp)
-      case Assume(exp) => goE(exp)
-      case Seqn(ss, _) => ss exists (hasProofObligations(_, p))
-      case If(cond, thn, els) => goE(cond) || hasProofObligations(thn, p) || hasProofObligations(els, p)
-      case While(cond, invs, body) => invs.nonEmpty || goE(cond) || hasProofObligations(body, p)
-      case Label(_, invs) => invs.nonEmpty
-      case _: Goto | _: LocalVarDeclStmt => false
-      case _: Quasihavoc | _: Quasihavocall => true
-      case _: ExtensionStmt => true // TODO ake
-    }
-  }
-
-  def introducesSmtAssumptions(s: Stmt): Boolean = s match {
-      case Seqn(ss, _) => ss exists introducesSmtAssumptions
-      case Label(_, invs) => invs.nonEmpty
-      case _: Exhale | _: Assert | _: Goto | _: LocalVarDeclStmt | _: Quasihavoc | _: Quasihavocall => false
-      case _: ExtensionStmt => true // TODO ake
-      case _ => true
-    }
-
 }
diff --git a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
index 727284162..360e162e4 100644
--- a/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
+++ b/src/main/scala/viper/silver/cfg/silver/CfgGenerator.scala
@@ -10,8 +10,8 @@ import viper.silver.ast._
 import viper.silver.cfg._
 import viper.silver.cfg.silver.SilverCfg.{SilverBlock, SilverEdge}
 import viper.silver.cfg.utility.{CfgSimplifier, IdInfo, LoopDetector}
-import java.util.concurrent.atomic.AtomicInteger
 
+import java.util.concurrent.atomic.AtomicInteger
 import scala.collection.mutable
 
 /**
@@ -363,11 +363,8 @@ object CfgGenerator {
             current = None
           case ConditionalJumpStmt(cond, thnTarget, elsTarget) =>
             current.foreach { currentIndex =>
-              val negInfo = cond.pos match {
-                case _ => cond.info
-              }
-              val neg = Not(cond)(cond.pos, negInfo, cond.errT)
-              addTmpEdge(TmpConditionalEdge(cond.withMeta(cond.pos, negInfo, cond.errT), currentIndex, resolve(thnTarget)))
+              val neg = Not(cond)(cond.pos, cond.info, cond.errT)
+              addTmpEdge(TmpConditionalEdge(cond, currentIndex, resolve(thnTarget)))
               addTmpEdge(TmpConditionalEdge(neg, currentIndex, resolve(elsTarget)))
             }
             current = None
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
index f009ac9bf..daafdcf0a 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/AnalysisSourceInfo.scala
@@ -42,10 +42,6 @@ trait AnalysisSourceInfo extends ast.Info {
 
   def getPosition: Position
 
-
-  def isAnalysisEnabled: Boolean = true
-
-
   override def comment: Seq[String] = Nil
   override def isCached: Boolean = false
 }
@@ -64,8 +60,6 @@ case class ExpAnalysisSourceInfo(source: ast.Exp, pos: Position) extends Analysi
 
   override def getPosition: Position = pos
 
-  override def isAnalysisEnabled: Boolean = true // DependencyAnalyzer.extractEnableAnalysisFromInfo(source.info).getOrElse(true)
-
   override def getDescription: String = source.toString.replaceAll("\n", "\t")
 }
 
@@ -74,8 +68,6 @@ case class StmtAnalysisSourceInfo(source: ast.Stmt, pos: Position) extends Analy
   override def toString: String = getDescription + " (" + super.toString + ")"
   override def getPosition: Position = pos
 
-  override def isAnalysisEnabled: Boolean = true // DependencyAnalyzer.extractEnableAnalysisFromInfo(source.info).getOrElse(true)
-
   override def getDescription: String = source.toString().replaceAll("\n", "\t")
 }
 
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
index 3b4cea5c3..b815a2fea 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
@@ -13,7 +13,7 @@ object DependencyTypeInfo {
 			case _: ast.Exhale | _: ast.Assert => ExplicitAssertion
 			case _: ast.Inhale | _: ast.Assume => ExplicitAssumption
 			case _: ast.Fold | _: ast.Unfold | _: ast.Package | _: ast.Apply => Rewrite
-			case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.Implicit
+			case _: ast.Quasihavoc | _: ast.Quasihavocall => DependencyType.SourceCode
 			case _ => DependencyType.make(AssumptionType.Unknown) /* TODO: should not happen */
 		}
 		DependencyTypeInfo(depType)
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index 481357cdd..75df769b1 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -2,7 +2,7 @@ package viper.silver.dependencyAnalysis
 
 object AssumptionType extends Enumeration {
   type AssumptionType = Value
-  val Explicit, LoopInvariant, PathCondition, Rewrite, SourceCode, DomainAxiom, Implicit, Internal, Trigger, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, MethodCall, FunctionBody, Precondition, Ghost, Annotation, CustomInternal, Unknown = Value
+  val Explicit, LoopInvariant, PathCondition, Rewrite, SourceCode, DomainAxiom, Implicit, Internal, Trigger, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, MethodCall, FunctionBody, Precondition, Ghost, Annotation, Unknown = Value
 
   def fromString(s: String): Option[Value] = values.find(_.toString == s)
 
@@ -10,10 +10,9 @@ object AssumptionType extends Enumeration {
   def postconditionTypes: Set[AssumptionType] = Set(ImplicitPostcondition, ExplicitPostcondition, ImportedPostcondition)
   def preconditionTypes: Set[AssumptionType] = Set(Precondition)
   def explicitAssertionTypes: Set[AssumptionType] = Set(Explicit, ImplicitPostcondition, ExplicitPostcondition)
-  def internalTypes: Set[AssumptionType] = Set(Internal, Trigger, CustomInternal) // will always be hidden from user
+  def internalTypes: Set[AssumptionType] = Set(Internal, Trigger) // will always be hidden from user
   def importedTypes: Set[AssumptionType] = Set(ImportedPostcondition)
   def verificationAnnotationTypes: Set[AssumptionType] = Set(FunctionBody /* TODO ake: review */, LoopInvariant, Rewrite, ExplicitPostcondition, ImplicitPostcondition, ImportedPostcondition, Precondition, Explicit, DomainAxiom, Annotation)
-  def sourceCodeTypes: Set[AssumptionType] = AssumptionType.values.diff(explicitAssumptionTypes ++ explicitAssertionTypes ++ verificationAnnotationTypes ++ internalTypes)
 
 
   def getPostcondType(isAbstractFunction: Boolean, dependencyType: Option[DependencyType]=None, isImported: Boolean=false): AssumptionType = {
@@ -24,7 +23,6 @@ object AssumptionType extends Enumeration {
       case AssumptionType.ImportedPostcondition => Some(AssumptionType.ImportedPostcondition)
       case AssumptionType.ImplicitPostcondition  => Some(AssumptionType.ImplicitPostcondition)
       case AssumptionType.Internal => Some(AssumptionType.Internal)
-      case AssumptionType.CustomInternal => Some(AssumptionType.CustomInternal)
       case AssumptionType.Annotation | AssumptionType.Ghost => None
       case _ => None
     }).getOrElse(
@@ -36,20 +34,19 @@ object AssumptionType extends Enumeration {
 import viper.silver.dependencyAnalysis.AssumptionType.AssumptionType
 
 object DependencyType {
-  val Implicit: DependencyType = DependencyType(AssumptionType.Implicit, AssumptionType.Implicit)
-  val SourceCode: DependencyType = DependencyType(AssumptionType.SourceCode, AssumptionType.SourceCode)
-  val Explicit: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Explicit)
+  val SourceCode: DependencyType = make(AssumptionType.SourceCode)
+  val Explicit: DependencyType = make(AssumptionType.Explicit)
   val ExplicitAssertion: DependencyType = DependencyType(AssumptionType.Internal, AssumptionType.Explicit)
   val ExplicitAssumption: DependencyType = DependencyType(AssumptionType.Explicit, AssumptionType.Implicit)
-  val PathCondition: DependencyType = DependencyType(AssumptionType.PathCondition, AssumptionType.Implicit)
-  val Invariant: DependencyType = DependencyType(AssumptionType.LoopInvariant, AssumptionType.LoopInvariant)
-  val Rewrite: DependencyType = DependencyType(AssumptionType.Rewrite, AssumptionType.Rewrite)
-  val Internal: DependencyType = DependencyType(AssumptionType.Internal, AssumptionType.Internal)
-  val Trigger: DependencyType = DependencyType(AssumptionType.Trigger, AssumptionType.Trigger)
-  val MethodCall: DependencyType = DependencyType(AssumptionType.MethodCall, AssumptionType.MethodCall)
-  val Ghost: DependencyType = DependencyType.make(AssumptionType.Ghost)
-  val Annotation: DependencyType = DependencyType.make(AssumptionType.Annotation)
-  val Axiom: DependencyType = DependencyType.make(AssumptionType.DomainAxiom)
+  val PathCondition: DependencyType = make(AssumptionType.PathCondition)
+  val Invariant: DependencyType = make(AssumptionType.LoopInvariant)
+  val Rewrite: DependencyType = make(AssumptionType.Rewrite)
+  val Internal: DependencyType = make(AssumptionType.Internal)
+  val Trigger: DependencyType = make(AssumptionType.Trigger)
+  val MethodCall: DependencyType = make(AssumptionType.MethodCall)
+  val Ghost: DependencyType = make(AssumptionType.Ghost)
+  val Annotation: DependencyType = make(AssumptionType.Annotation)
+  val Axiom: DependencyType = make(AssumptionType.DomainAxiom)
 
   def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
 }
diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala
index be4a698f1..9babebff6 100644
--- a/src/main/scala/viper/silver/parser/Translator.scala
+++ b/src/main/scala/viper/silver/parser/Translator.scala
@@ -112,7 +112,7 @@ case class Translator(program: PProgram) {
         val axiom = NamedDomainAxiom(name.name, exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
         attachInfo(axiom)
       case pa@PAxiom(anns, _, None, e) =>
-        val axiom = AnonymousDomainAxiom(exp(e.e.inner, Some(DependencyType.make(AssumptionType.DomainAxiom))))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
+        val axiom = AnonymousDomainAxiom(exp(e.e.inner, Some(DependencyType.Axiom)))(a, Translator.toInfo(anns, pa), domainName = pa.domain.idndef.name)
         attachInfo(axiom)
     }
   }

From 0f67b51b6c59f69d026e0229c0911c84b3ee5dac Mon Sep 17 00:00:00 2001
From: Andrea Keusch <andrea.keusch@hotmail.com>
Date: Tue, 12 May 2026 09:11:42 +0200
Subject: [PATCH 27/27] clean up silver

---
 .../AbstractDependencyAnalysisResult.scala                | 8 --------
 .../AbstractDependencyGraphInterpreter.scala              | 5 -----
 .../dependencyAnalysis/DependencyAnalysisInfo.scala       | 2 +-
 .../viper/silver/dependencyAnalysis/DependencyType.scala  | 2 +-
 src/main/scala/viper/silver/verifier/Verifier.scala       | 3 ---
 5 files changed, 2 insertions(+), 18 deletions(-)
 delete mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala
 delete mode 100644 src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala

diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala b/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala
deleted file mode 100644
index 0d53c72af..000000000
--- a/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyAnalysisResult.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-package viper.silver.dependencyAnalysis
-
-import viper.silver.ast.Program
-
-abstract class AbstractDependencyAnalysisResult(programName: String, program: Program, dependencyGraphInterpreters: Iterable[AbstractDependencyGraphInterpreter]) {
-
-  def getFullDependencyGraphInterpreter: AbstractDependencyGraphInterpreter
-}
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala b/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala
deleted file mode 100644
index fe906fa8f..000000000
--- a/src/main/scala/viper/silver/dependencyAnalysis/AbstractDependencyGraphInterpreter.scala
+++ /dev/null
@@ -1,5 +0,0 @@
-package viper.silver.dependencyAnalysis
-
-abstract class AbstractDependencyGraphInterpreter {
-
-}
\ No newline at end of file
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
index b815a2fea..fcf28efc0 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyAnalysisInfo.scala
@@ -111,4 +111,4 @@ trait AdditionalDependencyNodeInfo extends ast.Info {
 
 case class AdditionalAssertionNode() extends AdditionalDependencyNodeInfo
 
-case class AdditionalAssumptionNode() extends AdditionalDependencyNodeInfo
\ No newline at end of file
+case class AdditionalAssumptionNode() extends AdditionalDependencyNodeInfo
diff --git a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
index 75df769b1..cffd2dbf3 100644
--- a/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
+++ b/src/main/scala/viper/silver/dependencyAnalysis/DependencyType.scala
@@ -51,4 +51,4 @@ object DependencyType {
   def make(singleType: AssumptionType): DependencyType = DependencyType(singleType, singleType)
 }
 
-case class DependencyType(assumptionType: AssumptionType, assertionType: AssumptionType)
\ No newline at end of file
+case class DependencyType(assumptionType: AssumptionType, assertionType: AssumptionType)
diff --git a/src/main/scala/viper/silver/verifier/Verifier.scala b/src/main/scala/viper/silver/verifier/Verifier.scala
index 7eaef6430..ba8af5c26 100644
--- a/src/main/scala/viper/silver/verifier/Verifier.scala
+++ b/src/main/scala/viper/silver/verifier/Verifier.scala
@@ -8,7 +8,6 @@ package viper.silver.verifier
 
 import viper.silver.ast.Program
 import viper.silver.components.LifetimeComponent
-import viper.silver.dependencyAnalysis.AbstractDependencyAnalysisResult
 import viper.silver.reporter.{NoopReporter, Reporter}
 
 /** An abstract class for verifiers of Viper programs.
@@ -95,8 +94,6 @@ trait Verifier extends LifetimeComponent {
   def stop(): Unit
 
   def reporter: Reporter
-
-  def getDependencyAnalysisResult: Option[AbstractDependencyAnalysisResult] = None
 }
 
 /**