Fix all compiler warnings

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

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)

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))

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
   }

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

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 _ =>

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))

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]

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) =