From 0b1e2ccd2dd278c290aa4051001f65d71f85b88d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Fri, 21 Feb 2025 17:54:58 +0100
Subject: [PATCH 1/2] fix compiler warnings

---
 build.sbt                                     |  4 +-
 .../scala/viper/silver/ast/Expression.scala   | 10 ++---
 .../scala/viper/silver/ast/Statement.scala    |  7 +--
 .../silver/ast/utility/Consistency.scala      | 19 ++++----
 .../silver/ast/utility/Expressions.scala      |  4 +-
 .../ast/utility/QuantifiedPermissions.scala   |  7 ++-
 .../viper/silver/ast/utility/Simplifier.scala |  3 +-
 .../ast/utility/rewriter/RegexStrategy.scala  | 13 +++---
 .../ast/utility/rewriter/Strategy.scala       | 43 +++++++------------
 .../silver/ast/utility/rewriter/TRegex.scala  | 19 ++++----
 src/main/scala/viper/silver/cfg/Cfg.scala     |  4 ++
 .../viper/silver/cfg/silver/SilverCfg.scala   |  4 +-
 .../viper/silver/parser/MacroExpander.scala   |  2 +-
 .../transformation/MethodCheck.scala          |  2 +-
 14 files changed, 69 insertions(+), 72 deletions(-)

diff --git a/build.sbt b/build.sbt
index 741a51f7c..b20f82ea9 100644
--- a/build.sbt
+++ b/build.sbt
@@ -14,8 +14,8 @@ ThisBuild / scalacOptions ++= Seq(
   "-unchecked",                       // Warn on generated code assumptions
   "-feature",                         // Warn on features that requires explicit import
   "-Wunused",                         // Warn on unused imports
-  "-Ypatmat-exhaust-depth", "40",     // Increase depth of pattern matching analysis
-  // "-Xfatal-warnings",                 // Treat Warnings as errors to guarantee code quality in future changes
+  "-Ypatmat-exhaust-depth", "80",     // Increase depth of pattern matching analysis
+  "-Xfatal-warnings",                 // Treat Warnings as errors to guarantee code quality in future changes
 )
 
 // Enforce UTF-8, instead of relying on properly set locales
diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
index 105acfbe9..5f52689ff 100644
--- a/src/main/scala/viper/silver/ast/Expression.scala
+++ b/src/main/scala/viper/silver/ast/Expression.scala
@@ -16,21 +16,21 @@ import viper.silver.verifier.{ConsistencyError, VerificationResult}
 /** Expressions. */
 sealed trait Exp extends Hashable with Typed with Positioned with Infoed with TransformableErrors with PrettyExpression {
   var simplified: Option[Exp] = None
-  lazy val isPure = Expressions.isPure(this)
-  def isHeapDependent(p: Program) = Expressions.isHeapDependent(this, p)
-  def isTopLevelHeapDependent(p: Program) = Expressions.isTopLevelHeapDependent(this, p)
+  lazy val isPure: Boolean = Expressions.isPure(this)
+  def isHeapDependent(p: Program): Boolean = Expressions.isHeapDependent(this, p)
+  def isTopLevelHeapDependent(p: Program): Boolean = Expressions.isTopLevelHeapDependent(this, p)
 
   /**
    * Returns a representation of this expression as it looks when it is used as a proof obligation, i.e. all
    * InhaleExhaleExp are replaced by the inhale part.
    */
-  lazy val whenInhaling = Expressions.whenInhaling(this)
+  lazy val whenInhaling: Exp = Expressions.whenInhaling(this)
 
   /**
    * Returns a representation of this expression as it looks when it is used as a proof obligation, i.e. all
    * InhaleExhaleExp are replaced by the exhale part.
    */
-  lazy val whenExhaling = Expressions.whenExhaling(this)
+  lazy val whenExhaling: Exp = Expressions.whenExhaling(this)
 
   /** Returns the subexpressions of this expression */
   lazy val subExps = Expressions.subExps(this)
diff --git a/src/main/scala/viper/silver/ast/Statement.scala b/src/main/scala/viper/silver/ast/Statement.scala
index 4ce312014..242517386 100644
--- a/src/main/scala/viper/silver/ast/Statement.scala
+++ b/src/main/scala/viper/silver/ast/Statement.scala
@@ -25,12 +25,12 @@ sealed trait Stmt extends Hashable with Infoed with Positioned with Transformabl
     * Returns a list of all undeclared local variables contained in this statement and
     * throws an exception if the same variable is used with different types.
     */
-  def undeclLocalVars = Statements.undeclLocalVars(this)
+  def undeclLocalVars: Seq[LocalVar] = Statements.undeclLocalVars(this)
 
   /**
     * Computes all local variables that are written to in this statement.
     */
-  def writtenVars = Statements.writtenVars(this)
+  def writtenVars: Seq[LocalVar] = Statements.writtenVars(this)
 
   override def getMetadata:Seq[Any] = {
     Seq(pos, info, errT)
@@ -54,9 +54,10 @@ sealed trait AbstractAssign extends Stmt {
 }
 
 object AbstractAssign {
-  def apply(lhs: Lhs, rhs: Exp)(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos) = lhs match {
+  def apply(lhs: Lhs, rhs: Exp)(pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AbstractAssign with Serializable = lhs match {
     case l: LocalVar => LocalVarAssign(l, rhs)(pos, info, errT)
     case l: FieldAccess => FieldAssign(l, rhs)(pos, info, errT)
+    case _ => ???
   }
 
   def unapply(a: AbstractAssign) = Some((a.lhs, a.rhs))
diff --git a/src/main/scala/viper/silver/ast/utility/Consistency.scala b/src/main/scala/viper/silver/ast/utility/Consistency.scala
index 8b4d71dc2..dbd4a824d 100644
--- a/src/main/scala/viper/silver/ast/utility/Consistency.scala
+++ b/src/main/scala/viper/silver/ast/utility/Consistency.scala
@@ -177,14 +177,17 @@ object Consistency {
     val argVars = args.map(_.localVar).toSet
     var s = Seq.empty[ConsistencyError]
 
-    for (a@LocalVarAssign(l, _) <- b if argVars.contains(l)) {
-      s :+= ConsistencyError(s"$a is a reassignment of formal argument $l.", a.pos)
-    }
-    for (c@MethodCall(_, _, targets) <- b; t <- targets if argVars.contains(t)) {
-      s :+= ConsistencyError(s"$c is a reassignment of formal argument $t.", c.pos)
-    }
-    for (n@NewStmt(l, _) <- b if argVars.contains(l)) {
-      s :+= ConsistencyError(s"$n is a reassignment of formal argument $l.", n.pos)
+    b foreach {
+      case a@LocalVarAssign(l, _) if argVars.contains(l) =>
+        s :+= ConsistencyError(s"$a is a reassignment of formal argument $l.", a.pos)
+      case n@NewStmt(l, _) if argVars.contains(l) =>
+        s :+= ConsistencyError(s"$n is a reassignment of formal argument $l.", n.pos)
+      case c@MethodCall(_, _, targets) =>
+        targets foreach { t =>
+          if (argVars.contains(t))
+            s :+= ConsistencyError(s"$c is a reassignment of formal argument $t.", c.pos)
+        }
+      case _ =>
     }
     s
   }
diff --git a/src/main/scala/viper/silver/ast/utility/Expressions.scala b/src/main/scala/viper/silver/ast/utility/Expressions.scala
index bcab52dbf..bdd58d61e 100644
--- a/src/main/scala/viper/silver/ast/utility/Expressions.scala
+++ b/src/main/scala/viper/silver/ast/utility/Expressions.scala
@@ -25,10 +25,12 @@ object Expressions {
     case CondExp(cnd, thn, els) => isPure(cnd) && isPure(thn) && isPure(els)
     case unf: Unfolding => isPure(unf.body)
     case app: Applying => isPure(app.body)
-    case Asserting(a, e) => isPure(e)
+    case Asserting(_, e) => isPure(e)
     case QuantifiedExp(_, e0) => isPure(e0)
     case Let(_, _, body) => isPure(body)
     case e: ExtensionExp => e.extensionIsPure
+    case Forall(_, _, e) => isPure(e)
+    case Exists(_, _, e) => isPure(e)
 
     case   _: Literal
          | _: PermExp
diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 5d99d4e62..e2d0284dd 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -40,7 +40,7 @@ object QuantifiedPermissions {
         case Forall(_, _, implies: Implies) =>
           Some((forall, implies))
         case Forall(_, _, expr) =>
-          Some(forall, Implies(BoolLit(true)(forall.pos, forall.info, forall.errT), expr)(forall.pos, forall.info, forall.errT))
+          Some(forall, Implies(BoolLit(b = true)(forall.pos, forall.info, forall.errT), expr)(forall.pos, forall.info, forall.errT))
         case _ =>
           None
       }
@@ -252,13 +252,16 @@ object QuantifiedPermissions {
             // desugar the let-body
             val desugaredWithoutLet = desugarSourceQuantifiedPermissionSyntax(forallWithoutLet)
             desugaredWithoutLet.map{
-              case SourceQuantifiedPermissionAssertion(iqp, Implies(icond, irhs)) if (!irhs.isPure) =>
+              case SourceQuantifiedPermissionAssertion(iqp, Implies(icond, irhs)) if !irhs.isPure =>
                 // Since the rhs cannot be a let-binding, we expand the let-expression in it.
                 // However, we still use a let in the condition; this preserves well-definedness if v isn't used anywhere
                 Forall(iqp.variables, iqp.triggers.map(t => t.replace(v.localVar, e)), Implies(And(cond, Let(v, e, icond)(lt.pos, lt.info, lt.errT))(lt.pos, lt.info, lt.errT), irhs.replace(v.localVar, e))(iqp.pos, iqp.info, iqp.errT))(iqp.pos, iqp.info, iqp.errT)
               case iforall@Forall(ivars, itriggers, Implies(icond, ibod)) =>
                 // For all pure parts of the quantifier, we just re-wrap the body into a let.
                 Forall(ivars, itriggers, Implies(cond, Let(v, e, Implies(icond, ibod)(lt.pos, lt.info))(lt.pos, lt.info, lt.errT))(lt.pos, lt.info, lt.errT))(iforall.pos, iforall.info)
+              case _ =>
+                // suppress error: "Exhaustivity analysis reached max recursion depth, not all missing cases are reported."
+                ???
             }
           }
           case _ =>
diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
index e440383f2..7014a25b7 100644
--- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala
+++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala
@@ -51,7 +51,6 @@ object Simplifier {
       case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
       case Implies(_, tl@TrueLit()) if assumeWelldefinedness => tl
       case Implies(TrueLit(), consequent) => consequent
-      case root@Implies(FalseLit(), _) => TrueLit()(root.pos, root.info)
       case root@Implies(l1, Implies(l2, r)) => Implies(And(l1, l2)(), r)(root.pos, root.info)
 
       // TODO: Consider checking if Expressions.proofObligations(left) is empty (requires adding the program as parameter).
@@ -216,7 +215,7 @@ object Simplifier {
   private val bigIntZero = BigInt(0)
   private val bigIntOne = BigInt(1)
 
-  object AnyPermLiteral {
+  private object AnyPermLiteral {
     def unapply(p: Exp): Option[(BigInt, BigInt)] = p match {
       case FullPerm() => Some((bigIntOne, bigIntOne))
       case NoPerm() => Some((bigIntZero, bigIntOne))
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/RegexStrategy.scala b/src/main/scala/viper/silver/ast/utility/rewriter/RegexStrategy.scala
index bae6bffea..9608475eb 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/RegexStrategy.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/RegexStrategy.scala
@@ -6,8 +6,6 @@
 
 package viper.silver.ast.utility.rewriter
 
-import scala.reflect.runtime.{universe => reflection}
-
 /**
   * Extension of the Strategy context. Encapsulates all the required information for the rewriting
  *
@@ -85,7 +83,7 @@ case class SimpleRegexContext[N <: Rewritable](p: PartialFunction[N, N]) extends
   * @param p Partial function used for rewriting
   * @tparam N Common supertype of every node in the tree
   */
-class SlimRegexStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag](a: TRegexAutomaton, p: PartialFunction[N, N]) extends RegexStrategy[N, Any](a, SimpleRegexContext(p), new PartialContextR(null, (x, _) => x, (_, _) => true))
+class SlimRegexStrategy[N <: Rewritable : scala.reflect.ClassTag](a: TRegexAutomaton, p: PartialFunction[N, N]) extends RegexStrategy[N, Any](a, SimpleRegexContext(p), new PartialContextR(null, (x, _) => x, (_, _) => true))
 
 /**
   * A strategy that performs rewriting according to the Regex and Rewriting function specified
@@ -95,7 +93,7 @@ class SlimRegexStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.Cla
   * @tparam N Common supertype of every node in the tree
   * @tparam COLL Type of custom context
   */
-class RegexStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, COLL](a: TRegexAutomaton, p: PartialFunction[(N, RegexContext[N, COLL]), (N, RegexContext[N, COLL])], default: PartialContextR[N, COLL]) extends Strategy[N, RegexContext[N, COLL]](p) {
+class RegexStrategy[N <: Rewritable : scala.reflect.ClassTag, COLL](a: TRegexAutomaton, p: PartialFunction[(N, RegexContext[N, COLL]), (N, RegexContext[N, COLL])], default: PartialContextR[N, COLL]) extends Strategy[N, RegexContext[N, COLL]](p) {
 
   type CTXT = RegexContext[N, COLL]
 
@@ -128,7 +126,7 @@ class RegexStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTa
 
     }
     // Get the tuple that matches parameter node
-    def get(node: N, ancList: Seq[N]): Option[CTXT] = {
+    def get(node: N): Option[CTXT] = {
       // Get all matching nodes together with their index (only way to delete them later)
       val candidates = map.zipWithIndex.filter( _._1._1 eq node )
 
@@ -237,10 +235,8 @@ class RegexStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTa
         case Some(value) => Some(replaceTopDown(value, matches, ancList)).asInstanceOf[A]
 
         case n: N => {
-          val newAncList = ancList ++ Seq(n)
-
           // Find out if this node is going to be replaced
-          val replaceInfo = matches.get(n, newAncList.asInstanceOf[Seq[N]])
+          val replaceInfo = matches.get(n)
 
           // get resulting node from rewriting
           val resultNodeO = replaceInfo match {
@@ -258,6 +254,7 @@ class RegexStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTa
             newNode.asInstanceOf[A]
           else {
             val allowedToRecurse = recursionFunc.applyOrElse(newNode, (_: N) => newNode.children).toSet
+            val newAncList = ancList ++ Seq(n)
             val children = newNode.children.map(child => if (allowedToRecurse(child)) replaceTopDown(child, matches, newAncList) else child)
 
             newNode.withChildren(children).asInstanceOf[A]
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala b/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
index d04e27be9..d701d0999 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala
@@ -9,7 +9,7 @@ import viper.silver.ast.utility.rewriter.Traverse.Traverse
 
 import scala.annotation.unused
 import scala.collection.mutable
-import scala.reflect.runtime.{universe => reflection}
+import scala.collection.mutable.ListBuffer
 
 /**
   * An enumeration that represents traversal modes:
@@ -20,6 +20,7 @@ import scala.reflect.runtime.{universe => reflection}
   */
 object Traverse extends Enumeration {
   type Traverse = Value
+  @unused
   val TopDown, BottomUp, Innermost, Outermost = Value
 }
 
@@ -33,7 +34,7 @@ trait StrategyInterface[N <: Rewritable] {
   // Store every special node we don't want to recurse on
   // A hash set would be more efficient but then we get problems with circular dependencies (calculating hash never terminates)
 
-  protected val noRecursion = mutable.ListBuffer.empty[NodeEq]
+  protected val noRecursion: ListBuffer[NodeEq] = mutable.ListBuffer.empty[NodeEq]
 
   case class NodeEq(node: Rewritable) {
     override def equals(that: Any): Boolean = that match {
@@ -109,7 +110,7 @@ object StrategyBuilder {
     * @tparam N Common supertype of every node in the tree
     * @return Strategy object ready to execute on a tree
     */
-  def Slim[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag](p: PartialFunction[N, N], t: Traverse = Traverse.TopDown) = {
+  def Slim[N <: Rewritable](p: PartialFunction[N, N], t: Traverse = Traverse.TopDown): Strategy[N, SimpleContext[N]] = {
     new SlimStrategy[N](p) defaultContext new NoContext[N] traverse t
   }
 
@@ -121,7 +122,7 @@ object StrategyBuilder {
     * @tparam N Common supertype of every node in the tree
     * @return Strategy object ready to execute on a tree
     */
-  def Ancestor[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag](p: PartialFunction[(N, ContextA[N]), (N, ContextA[N])], t: Traverse = Traverse.TopDown) = {
+  def Ancestor[N <: Rewritable](p: PartialFunction[(N, ContextA[N]), (N, ContextA[N])], t: Traverse = Traverse.TopDown): Strategy[N, ContextA[N]] = {
     new Strategy[N, ContextA[N]](p) defaultContext new PartialContextA[N] traverse t
   }
 
@@ -135,7 +136,7 @@ object StrategyBuilder {
     * @tparam C Type of the context
     * @return Strategy object ready to execute on a tree
     */
-  def Context[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C](p: PartialFunction[(N, ContextC[N, C]), (N, ContextC[N, C])], default: C, t: Traverse = Traverse.TopDown) = {
+  def Context[N <: Rewritable, C](p: PartialFunction[(N, ContextC[N, C]), (N, ContextC[N, C])], default: C, t: Traverse = Traverse.TopDown): Strategy[N, ContextC[N, C]] = {
     new Strategy[N, ContextC[N, C]](p) defaultContext new PartialContextC[N, C](default) traverse t
   }
 
@@ -149,7 +150,7 @@ object StrategyBuilder {
     * @tparam C Type of the context
     * @return Strategy object ready to execute on a tree
     */
-  def CustomContext[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C](p: PartialFunction[(N, C), (N, C)], default: C, t: Traverse = Traverse.TopDown) = {
+  def CustomContext[N <: Rewritable, C](p: PartialFunction[(N, C), (N, C)], default: C, t: Traverse = Traverse.TopDown): Strategy[N, ContextCustom[N, C]] = {
     new Strategy[N, ContextCustom[N, C]]({ // rewrite partial function taking context with parent access etc. to one just taking the custom context
       case (node, context) if p.isDefinedAt(node, context.c) =>
         val (n, c) = p((node, context.c))
@@ -167,7 +168,7 @@ object StrategyBuilder {
     * @tparam C         Type of the context
     * @return           Strategy object ready to execute on a tree
     */
-  def RewriteNodeAndContext[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C](p: PartialFunction[(N, C), (N, C)], context: C, t: Traverse = Traverse.TopDown) = {
+  def RewriteNodeAndContext[N <: Rewritable, C](p: PartialFunction[(N, C), (N, C)], context: C, t: Traverse = Traverse.TopDown): Strategy[N, ContextC[N, C]] = {
     val f: PartialFunction[(N, ContextC[N, C]), (N, ContextC[N, C])] = {
       case (node, context) if p.isDefinedAt(node, context.c) =>
         val (n, c) = p((node, context.c))
@@ -208,7 +209,7 @@ object StrategyBuilder {
     * @tparam C Type of the context
     * @return Visitor object ready to use
     */
-  def ContextVisitor[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C](f: (N, ContextC[N, C]) => ContextC[N, C], default: C) = {
+  def ContextVisitor[N <: Rewritable, C](f: (N, ContextC[N, C]) => ContextC[N, C], default: C): Strategy[N, ContextC[N, C]] = {
     val p: PartialFunction[(N, ContextC[N, C]), (N, ContextC[N, C])] = {
       case (n, c) => (n, f(n, c))
     }
@@ -234,20 +235,13 @@ class AddArtificialContext[N <: Rewritable](p: PartialFunction[N, N]) extends Pa
   * @param p Partial function from node to node
   * @tparam N Type of the
   */
-class SlimStrategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag](p: PartialFunction[N, N]) extends Strategy[N, SimpleContext[N]](new AddArtificialContext(p))
+class SlimStrategy[N <: Rewritable](p: PartialFunction[N, N]) extends Strategy[N, SimpleContext[N]](new AddArtificialContext(p))
 
 // Generic Strategy class. Includes all the required functionality
-class Strategy[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, C <: Context[N]](p: PartialFunction[(N, C), (N, C)]) extends StrategyInterface[N] {
+class Strategy[N <: Rewritable, C <: Context[N]](p: PartialFunction[(N, C), (N, C)]) extends StrategyInterface[N] {
 
   // Defines the traversion mode
-  protected var traversionMode: Traverse = Traverse.TopDown
-
-  /**
-    * Access to the current traversion mode
-    *
-    * @return Traversion mode
-    */
-  def getTraversionMode = traversionMode
+  private var traversionMode: Traverse = Traverse.TopDown
 
   /**
     * Define the traversion mode
@@ -796,13 +790,13 @@ class ContextC[N <: Rewritable, CUSTOM](aList: Seq[N], val c: CUSTOM, transforme
   }
 
   // Perform the custom update part of the update
-  def updateCustom(n: N): ContextC[N, CUSTOM] = {
+  def updateCustom(): ContextC[N, CUSTOM] = {
     new ContextC[N, CUSTOM](ancestorList, c, transformer)
   }
 
   // Update the context with node and custom context
   override def update(n: N): ContextC[N, CUSTOM] = {
-    replaceNode(n).updateCustom(node)
+    replaceNode(n).updateCustom()
   }
 
   def updateContext(c: CUSTOM) =
@@ -819,14 +813,9 @@ class ContextC[N <: Rewritable, CUSTOM](aList: Seq[N], val c: CUSTOM, transforme
   */
 class ContextCustom[N <: Rewritable, CUSTOM](val c: CUSTOM, override protected val transformer: StrategyInterface[N]) extends SimpleContext[N](transformer) {
 
-  // Perform the custom update part of the update
-  def updateCustom(n: N): ContextCustom[N, CUSTOM] = {
-    new ContextCustom[N, CUSTOM](c, transformer)
-  }
-
   // Update the context with node and custom context
-  override def update(n: N): ContextCustom[N, CUSTOM] = {
-    updateCustom(n)
+  override def update(@unused n: N): ContextCustom[N, CUSTOM] = {
+    new ContextCustom[N, CUSTOM](c, transformer)
   }
 
   def updateContext(c: CUSTOM) =
diff --git a/src/main/scala/viper/silver/ast/utility/rewriter/TRegex.scala b/src/main/scala/viper/silver/ast/utility/rewriter/TRegex.scala
index e1f47389f..56bfecb46 100644
--- a/src/main/scala/viper/silver/ast/utility/rewriter/TRegex.scala
+++ b/src/main/scala/viper/silver/ast/utility/rewriter/TRegex.scala
@@ -7,7 +7,6 @@
 package viper.silver.ast.utility.rewriter
 
 import scala.annotation.unused
-import scala.reflect.runtime.{universe => reflection}
 
 /*
  * This Source Code Form is subject to the terms of the Mozilla Public
@@ -94,7 +93,7 @@ trait Match {
 class NMatch[N <: Rewritable : TypeTag](val pred: N => Boolean, val rewrite: Boolean) extends Match {
 
   // Checks if node n (of type T) is a valid subtype of generic parameter N
-  protected def matches[T: TypeTag](n: T): Boolean = {
+  protected def matches[T](n: T): Boolean = {
     // TODO: This code works but im not really familiar with reflection. Is there a better solution?
     val mirror = runtimeMirror(n.getClass.getClassLoader) // obtain runtime mirror
     val sym = mirror.staticClass(n.getClass.getName) // obtain class symbol for `n`
@@ -102,7 +101,7 @@ class NMatch[N <: Rewritable : TypeTag](val pred: N => Boolean, val rewrite: Boo
 
     // create a type tag which contains above type object
     val t1 = TypeTag(mirror, new api.TypeCreator {
-      def apply[U <: api.Universe with Singleton](m: api.Mirror[U]) =
+      def apply[U <: api.Universe with Singleton](m: api.Mirror[U]): U#Type =
         if (m eq mirror) tpe.asInstanceOf[U#Type]
         else throw new IllegalArgumentException(s"Type tag defined in $mirror cannot be migrated to other mirrors.")
     }).tpe
@@ -283,7 +282,7 @@ class Questionmark(m: Match) extends Match {
   * @tparam N Type of the AST
   * @tparam COLL Type of the context
   */
-class TreeRegexBuilder[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, COLL](val accumulator: (COLL, COLL) => COLL, val combinator: (COLL, COLL) => COLL, val default: COLL) {
+class TreeRegexBuilder[N <: Rewritable : scala.reflect.ClassTag, COLL](val accumulator: (COLL, COLL) => COLL, val combinator: (COLL, COLL) => COLL, val default: COLL) {
 
   /**
     * Generates a TreeRegexBuilderWithMatch by adding the matching part to the mix
@@ -300,7 +299,7 @@ class TreeRegexBuilder[N <: Rewritable : reflection.TypeTag : scala.reflect.Clas
   * @tparam N Type of the AST
   * @tparam COLL Type of the context
   */
-class TreeRegexBuilderWithMatch[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, COLL](tbuilder: TreeRegexBuilder[N, COLL], regex: Match) {
+class TreeRegexBuilderWithMatch[N <: Rewritable : scala.reflect.ClassTag, COLL](tbuilder: TreeRegexBuilder[N, COLL], regex: Match) {
 
   /**
     * Generate the regex strategy by adding the rewriting function into the mix
@@ -314,7 +313,7 @@ class TreeRegexBuilderWithMatch[N <: Rewritable : reflection.TypeTag : scala.ref
   * Same as TreeRegexBuilder just without context
   * @tparam N Type of all AST nodes
   */
-class SimpleRegexBuilder[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag]() {
+class SimpleRegexBuilder[N <: Rewritable : scala.reflect.ClassTag]() {
 
   /**
     * Generates a TreeRegexBuilderWithMatch by adding the matching part to the mix
@@ -329,7 +328,7 @@ class SimpleRegexBuilder[N <: Rewritable : reflection.TypeTag : scala.reflect.Cl
   * @param regex Regular expression used for matching
   * @tparam N Type of all AST nodes
   */
-class SimpleRegexBuilderWithMatch[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag](regex: Match) {
+class SimpleRegexBuilderWithMatch[N <: Rewritable : scala.reflect.ClassTag](regex: Match) {
 
   /**
     * Generate the regex strategy by adding the rewriting function into the mix
@@ -353,21 +352,21 @@ object TreeRegexBuilder {
     * @tparam COLL Type of the context
     * @return
     */
-  def context[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag, COLL](accumulator: (COLL, COLL) => COLL, combinator: (COLL, COLL) => COLL, default: COLL) = new TreeRegexBuilder[N, COLL](accumulator, combinator, default)
+  def context[N <: Rewritable : scala.reflect.ClassTag, COLL](accumulator: (COLL, COLL) => COLL, combinator: (COLL, COLL) => COLL, default: COLL) = new TreeRegexBuilder[N, COLL](accumulator, combinator, default)
 
   /**
     * Don't care about the custom context but want ancestor/sibling information
     * @tparam N Type of the AST
     * @return TreeRegexBuilder object
     */
-  def ancestor[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag] = new TreeRegexBuilder[N, Any]((x, _) => x, (_, _) => true, null)
+  def ancestor[N <: Rewritable : scala.reflect.ClassTag] = new TreeRegexBuilder[N, Any]((x, _) => x, (_, _) => true, null)
 
   /**
     * Don't care about context at all
     * @tparam N Type of the AST
     * @return SimpleRegexBuilder
     */
-  def simple[N <: Rewritable : reflection.TypeTag : scala.reflect.ClassTag] = new SimpleRegexBuilder[N]
+  def simple[N <: Rewritable : scala.reflect.ClassTag] = new SimpleRegexBuilder[N]
 }
 
 
diff --git a/src/main/scala/viper/silver/cfg/Cfg.scala b/src/main/scala/viper/silver/cfg/Cfg.scala
index 966cf4e1d..5a7765a36 100644
--- a/src/main/scala/viper/silver/cfg/Cfg.scala
+++ b/src/main/scala/viper/silver/cfg/Cfg.scala
@@ -114,6 +114,8 @@ trait Cfg[S, E] {
         case PostconditionBlock(posts) => PostconditionBlock(posts.map(expMap))
         case LoopHeadBlock(invs, stmts, loopId) => LoopHeadBlock(invs.map(expMap), stmts.flatMap(stmtMap), loopId)
         //case ConstrainingBlock(vars, body) => ConstrainingBlock(vars.map(expMap), body.map[C, S2, E2](factory)(stmtMap, expMap))
+        case _ =>
+          ??? // suppress "match may not be exhaustive"
       }
       block -> mapped
     }.toMap
@@ -162,6 +164,8 @@ trait Cfg[S, E] {
         block.toString + "|" + posts.map(_.toString).map(escape).mkString("|")
       case LoopHeadBlock(invs, stmts, _) =>
         block.toString + "|" + invs.map(inv => "invariant " + escape(inv.toString)).mkString("|") + "|" + stmts.map(_.toString).map(escape).mkString("|")
+      case _ =>
+        ??? // suppress "match may not be exhaustive"
     }
 
     val blockStr = new StringBuilder()
diff --git a/src/main/scala/viper/silver/cfg/silver/SilverCfg.scala b/src/main/scala/viper/silver/cfg/silver/SilverCfg.scala
index 9e9c6aa91..1d5984bbb 100644
--- a/src/main/scala/viper/silver/cfg/silver/SilverCfg.scala
+++ b/src/main/scala/viper/silver/cfg/silver/SilverCfg.scala
@@ -104,9 +104,9 @@ class SilverCfg(val blocks: Seq[SilverBlock], val edges: Seq[SilverEdge], val en
   : (Option[SilverBlock], mutable.Map[SilverBlock, SilverBlock]) = {
 
     var queue = mutable.Queue.from(queueInit)
-    var visited: mutable.Set[SilverBlock] = mutable.Set.from(visitedInit)
+    val visited: mutable.Set[SilverBlock] = mutable.Set.from(visitedInit)
     val map = mutable.Map[SilverBlock, SilverBlock]()
-    var loopHeads: mutable.Set[SilverBlock] = mutable.Set.from(loopHeadsSeen)
+    val loopHeads: mutable.Set[SilverBlock] = mutable.Set.from(loopHeadsSeen)
 
     // BFS traversal of CFG.
     while (queue.nonEmpty) {
diff --git a/src/main/scala/viper/silver/parser/MacroExpander.scala b/src/main/scala/viper/silver/parser/MacroExpander.scala
index 0a5bcfee9..753f5090b 100644
--- a/src/main/scala/viper/silver/parser/MacroExpander.scala
+++ b/src/main/scala/viper/silver/parser/MacroExpander.scala
@@ -537,7 +537,7 @@ object MacroExpander {
           val replacement = ctx.c.paramToArgMap(lName.name).deepCopyAll
           val replaced = replacement match {
             case r: PIdnUseExp => PIdnDef(r.name)(r.pos)
-            case r =>
+            case _ =>
               throw MacroException(s"macro expansion cannot substitute expression `${replacement.pretty}` at ${replacement.pos._1} in non-expression position at ${lName.pos._1}.", replacement.pos)
           }
           (PLabel(lbl, replaced, invs)(label.pos), ctx.updateContext(ctx.c.copy(paramToArgMap = ctx.c.paramToArgMap.empty)))
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/transformation/MethodCheck.scala b/src/main/scala/viper/silver/plugin/standard/termination/transformation/MethodCheck.scala
index b754f5977..3c9df0cc5 100644
--- a/src/main/scala/viper/silver/plugin/standard/termination/transformation/MethodCheck.scala
+++ b/src/main/scala/viper/silver/plugin/standard/termination/transformation/MethodCheck.scala
@@ -242,7 +242,7 @@ trait MethodCheck extends ProgramManager with DecreasesCheck with NestedPredicat
    * Mark already traversed and transformed nodes.
    * Used for while loops because a while node is potentially traversed twice.
    */
-  private final case class Transformed() extends Info {
+  private case class Transformed() extends Info {
     override val comment: Seq[String] = Nil
 
     override val isCached: Boolean = false

From 70498396423c13b781c766e6f00c850c0ca10620 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Wed, 26 Feb 2025 14:54:39 +0100
Subject: [PATCH 2/2] fix test compilation issues

---
 src/test/scala/RewriteWithCycles.scala |  4 +---
 src/test/scala/UtilityTests.scala      | 20 ++++++++------------
 2 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/src/test/scala/RewriteWithCycles.scala b/src/test/scala/RewriteWithCycles.scala
index faf8548a6..d9f6f21f7 100644
--- a/src/test/scala/RewriteWithCycles.scala
+++ b/src/test/scala/RewriteWithCycles.scala
@@ -7,8 +7,6 @@
 import org.scalatest.funsuite.AnyFunSuite
 import viper.silver.ast.utility.rewriter.{Rewritable, StrategyBuilder}
 
-import scala.reflect.runtime.{universe => reflection}
-
 class RewriteWithCycles extends AnyFunSuite {
 
 
@@ -44,7 +42,7 @@ class RewriteWithCycles extends AnyFunSuite {
   }
 
   // Visit all reachable nodes in the graph and call func on them.
-  def visitAll[I : reflection.TypeTag](s:SlimGraph[I], func:I=>I) = {
+  def visitAll[I](s:SlimGraph[I], func:I=>I) = {
     val strat = StrategyBuilder.Ancestor[SlimGraph[I]]({
       case (sG, c) => {
         if(c.ancestorList.dropRight(1).contains(sG))
diff --git a/src/test/scala/UtilityTests.scala b/src/test/scala/UtilityTests.scala
index c98e62f92..ab8027c2b 100644
--- a/src/test/scala/UtilityTests.scala
+++ b/src/test/scala/UtilityTests.scala
@@ -6,24 +6,20 @@
 
 import org.scalatest.funsuite.AnyFunSuite
 import org.scalatest.matchers.should.Matchers
-import viper.silver.ast._
-import viper.silver.ast.utility.ImpureAssumeRewriter
-
 
 class UtilityTests extends AnyFunSuite with Matchers {
 
   /* These tests exercise utility methods on the AST (transformers, visitors, rewriters etc.) */
 
   test("Assume rewriter (direct)"){ // assume acc(x.f) -> rewritten to -> assume perm(x.f) >= write
-    val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), Some(FullPerm()(NoPosition)))(NoPosition)
-    val testMethod : Method = Method("m1", Seq(), Seq(), Seq(), Seq(),
-      Some(Seqn(Seq(
-        Assume(assumeBody)(NoPosition)
-      ), Seq())(NoPosition, NoInfo, NoTrafos))
-      )(NoPosition)
-
-    val testProgram : Program = Program(Seq(), Seq(Field("f",Int)(NoPosition)), Seq(), Seq(), Seq(testMethod), Seq())(NoPosition)
-
+    // val assumeBody = FieldAccessPredicate(FieldAccess(LocalVar("x", Ref)(),Field("f",Int)(NoPosition))(NoPosition), Some(FullPerm()(NoPosition)))(NoPosition)
+    // val testMethod : Method = Method("m1", Seq(), Seq(), Seq(), Seq(),
+    //  Some(Seqn(Seq(
+    //    Assume(assumeBody)(NoPosition)
+    //  ), Seq())(NoPosition, NoInfo, NoTrafos))
+    //  )(NoPosition)
+
+    // val testProgram : Program = Program(Seq(), Seq(Field("f",Int)(NoPosition)), Seq(), Seq(), Seq(testMethod), Seq())(NoPosition)
     // val rewritten = AssumeRewriter.rewrite(assumeBody,testProgram)
 
     // rewritten should be (TrueLit()(NoPosition)) // this (spurious) test seems to cause an infinite recursion bug..