Enable fatal warnings and fix compiler warnings throughout codebase

build.sbt

@@ -17,6 +17,9 @@ lazy val carbon = (project in file("."))
         organization := "viper",
         version := "1.0-SNAPSHOT",
 
+        // Compilation settings
+        scalacOptions += "-Xfatal-warnings",    // Treat warnings as errors to guarantee code quality in future changes
+
         // Fork test to a different JVM than SBT's, avoiding SBT's classpath interfering with
         // classpath used by Scala's reflection.
         Test / fork := true,

src/main/scala/viper/carbon/Carbon.scala

@@ -21,7 +21,7 @@ object Carbon extends CarbonFrontend(StdIOReporter("carbon_reporter"), ViperStdO
     val submitter = new FileProgramSubmitter(this)
     submitter.setArgs(args)
 
-    execute(args)
+    execute(args.toIndexedSeq)
     specifyAppExitCode()
 
     submitter.submit()

src/main/scala/viper/carbon/boogie/BoogieModelTransformer.scala

@@ -1,7 +1,7 @@
 package viper.carbon.boogie
 
 import viper.carbon.verifier.FailureContextImpl
-import viper.silver.verifier.{AbstractError, Counterexample, FailureContext, Model, ModelEntry, SimpleCounterexample, VerificationError}
+import viper.silver.verifier.{AbstractError, Model, ModelEntry, SimpleCounterexample, VerificationError}
 
 import scala.collection.mutable
 

src/main/scala/viper/carbon/boogie/Implicits.scala

@@ -14,8 +14,8 @@ import language.implicitConversions
  */
 object Implicits {
   implicit def lift[T](t: T): Seq[T] = Seq(t)
-  implicit def liftStmt(ss: Seq[Stmt]) = Seqn(ss)
-  implicit def liftSeq(ss: Seq[Exp]) = new BoolSeq(ss)
+  implicit def liftStmt(ss: Seq[Stmt]): Seqn = Seqn(ss)
+  implicit def liftSeq(ss: Seq[Exp]): BoolSeq = new BoolSeq(ss)
 
   /**
    * Adds methods to turn a sequence of expressions into their conjunction or disjunction.

src/main/scala/viper/carbon/boogie/UnicodeString.scala

@@ -21,5 +21,5 @@ class UnicodeString(val s: String) {
   }
 }
 object UnicodeString {
-  implicit def string2unicodestring(s: String) = new UnicodeString(s)
+  implicit def string2unicodestring(s: String): UnicodeString = new UnicodeString(s)
 }

src/main/scala/viper/carbon/boogie/boogie.scala

@@ -11,6 +11,7 @@ import viper.silver.ast.Member
 import viper.silver.ast.pretty._
 import viper.silver.verifier.VerificationError
 
+import scala.annotation.unused
 import scala.collection.mutable
 
 /** The root of the Boogie AST. */
@@ -48,23 +49,23 @@ sealed trait Node {
    * Applies the function `f1` to the AST node, then visits all subnodes,
    * and finally calls `f2` to the AST node.
    */
-  def visit(n: Node, f1: PartialFunction[Node, Unit], f2: PartialFunction[Node, Unit]): Unit = {
+  def visit(@unused n: Node, f1: PartialFunction[Node, Unit], f2: PartialFunction[Node, Unit]): Unit = {
     Visitor.visit(this, f1, f2)
   }
 
   /**
    * Applies the function `f` to the AST node, then visits all subnodes if `f`
    * returned true.
    */
-  def visitOpt(n: Node)(f: Node => Boolean): Unit = {
+  def visitOpt(@unused n: Node)(f: Node => Boolean): Unit = {
     Visitor.visitOpt(this)(f)
   }
 
   /**
    * Applies the function `f1` to the AST node, then visits all subnodes if `f1`
    * returned true, and finally calls `f2` to the AST node.
    */
-  def visitOpt(n: Node, f1: Node => Boolean, f2: Node => Unit): Unit = {
+  def visitOpt(@unused n: Node, f1: Node => Boolean, f2: Node => Unit): Unit = {
     Visitor.visitOpt(this, f1, f2)
   }
 

src/main/scala/viper/carbon/boogie/utility.scala

@@ -154,13 +154,13 @@ object Nodes {
       case Some(ee) => ee
       case None =>
         exp match {
-          case IntLit(i) => exp
-          case BoolLit(b) => exp
-          case RealLit(b) => exp
+          case IntLit(_) => exp
+          case BoolLit(_) => exp
+          case RealLit(_) => exp
           case RealConv(exp) => RealConv(func(exp))
-          case LocalVar(n, tt) => exp
-          case GlobalVar(n, tt) => exp
-          case Const(i) => exp
+          case LocalVar(_, _) => exp
+          case GlobalVar(_, _) => exp
+          case Const(_) => exp
           case MapSelect(map, idxs) => MapSelect(func(map), idxs map func)
           case MapUpdate(map, idxs, value) => MapUpdate(func(map), idxs map func, func(value))
           case Old(e) => Old(func(e))

src/main/scala/viper/carbon/modules/ExhaleModule.scala

@@ -6,7 +6,7 @@
 
 package viper.carbon.modules
 
-import components.{ComponentRegistry, DefinednessState, ExhaleComponent}
+import components.{ComponentRegistry, ExhaleComponent}
 import viper.silver.{ast => sil}
 import viper.carbon.boogie.Stmt
 import viper.silver.verifier.PartialVerificationError

src/main/scala/viper/carbon/modules/HeapModule.scala

@@ -9,8 +9,6 @@ package viper.carbon.modules
 import viper.silver.{ast => sil}
 import viper.carbon.boogie._
 import viper.carbon.modules.components.CarbonStateComponent
-import viper.carbon.utility.PolyMapDesugarHelper
-import viper.silver.ast.{LocationAccess, MagicWand}
 
 /**
  * A module for translating heap expressions (access, updating) and determining

src/main/scala/viper/carbon/modules/Module.scala

@@ -59,5 +59,5 @@ trait Module extends LifetimeComponent with StatefulComponent with viper.carbon.
  * Trait to extend in modules which promise *not* to require a reset method
  */
 trait StatelessComponent {
-  final def reset = { }
+  final def reset(): Unit = { }
 }

src/main/scala/viper/carbon/modules/components/DefinednessComponent.scala

@@ -10,6 +10,8 @@ import viper.carbon.boogie.{Statements, Stmt}
 import viper.silver.{ast => sil}
 import viper.silver.verifier.PartialVerificationError
 
+import scala.annotation.unused
+
 /**
  * Takes care of determining whether expressions are well-formed.
  */
@@ -18,7 +20,7 @@ trait DefinednessComponent extends Component {
   /**
    * Free assumptions about an expression.
    */
-  def freeAssumptions(e: sil.Exp): Stmt = Statements.EmptyStmt
+  def freeAssumptions(@unused e: sil.Exp): Stmt = Statements.EmptyStmt
 
   /**
     * Well-definedness check for `e` itself (not its subnodes). This check is invoked *before* invoking the
@@ -30,15 +32,17 @@ trait DefinednessComponent extends Component {
     * definedness check should be made, otherwise these checks should be done in the currently active state.
     * Expressions should be evaluated in the currently active state.
    */
-  def simplePartialCheckDefinednessBefore(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean,
-                                          definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
+  def simplePartialCheckDefinednessBefore(@unused e: sil.Exp, @unused error: PartialVerificationError,
+                                          @unused makeChecks: Boolean,
+                                          @unused definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
 
   /**
     * Same as [[simplePartialCheckDefinednessBefore]], except that this well-definedness check is invoked and emitted
     * *after* the well-definedness checks of `e`'s subnodes are invoked and emitted.
     */
-  def simplePartialCheckDefinednessAfter(e: sil.Exp, error: PartialVerificationError, makeChecks: Boolean,
-                                         definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
+  def simplePartialCheckDefinednessAfter(@unused e: sil.Exp, @unused error: PartialVerificationError,
+                                         @unused makeChecks: Boolean,
+                                         @unused definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
 
   /**
    * Proof obligations for a given expression.  The first part of the result is used before

src/main/scala/viper/carbon/modules/components/ExhaleComponent.scala

@@ -10,6 +10,8 @@ import viper.carbon.boogie.{Statements, Stmt}
 import viper.silver.{ast => sil}
 import viper.silver.verifier.PartialVerificationError
 
+import scala.annotation.unused
+
 /**
  * Takes care of exhaling one or several kinds of expressions.
 
@@ -19,7 +21,8 @@ trait ExhaleComponent extends Component {
   /**
    * Exhale a single expression.
    */
-  def exhaleExp(e: sil.Exp, error: PartialVerificationError, definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
+  def exhaleExp(@unused e: sil.Exp, @unused error: PartialVerificationError,
+                @unused definednessStateOpt: Option[DefinednessState]): Stmt = Statements.EmptyStmt
 
   /**
     */

src/main/scala/viper/carbon/modules/components/StmtComponent.scala

@@ -10,6 +10,8 @@ import viper.silver.{ast => sil}
 import viper.carbon.boogie._
 import viper.silver.ast.LocalVar
 
+import scala.annotation.unused
+
 /**
  * Contributes to the translation of one or several statements.
  */
@@ -35,5 +37,5 @@ trait StmtComponent extends Component {
   /**
    * This method is called when translating a "fresh" statement, and by default does nothing
    */
-  def freshReads(fb: Seq[LocalVar]): Stmt = Statements.EmptyStmt
+  def freshReads(@unused fb: Seq[LocalVar]): Stmt = Statements.EmptyStmt
 }

src/main/scala/viper/carbon/modules/impls/DefaultDomainModule.scala

@@ -25,7 +25,7 @@ class DefaultDomainModule(val verifier: Verifier) extends DomainModule with Stat
 
   def name = "Domain module"
 
-  implicit val namespace = verifier.freshNamespace("domain")
+  implicit val namespace: Namespace = verifier.freshNamespace("domain")
 
   // name for output identifier (to try to avoid clashes - should be improved for robustness (see issue #19)
   def outputName(domain: sil.Domain) : String = domain.name + "DomainType"

src/main/scala/viper/carbon/modules/impls/DefaultExhaleModule.scala

@@ -23,14 +23,13 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
 
   import verifier._
   import expModule._
-  import permModule._
   import heapModule._
   import mainModule._
   import stateModule._
 
   def name = "Exhale module"
 
-  override def reset = { }
+  override def reset(): Unit = { }
 
   override def start(): Unit = {
     register(this)
@@ -111,7 +110,7 @@ class DefaultExhaleModule(val verifier: Verifier) extends ExhaleModule {
     *                  Access to the current state is needed during translation of an exhale during packaging a wand
    */
   private def exhaleConnective(e: sil.Exp, error: PartialVerificationError, definednessCheckData: DefinednessCheckData,
-                               havocHeap: Boolean = true, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false,
+                               havocHeap: Boolean, statesStackForPackageStmt: List[Any], insidePackageStmt: Boolean,
                                isAssert: Boolean, currentStateForPackage: StateRep): Stmt = {
 
     e match {

src/main/scala/viper/carbon/modules/impls/DefaultExpModule.scala

@@ -13,9 +13,10 @@ import viper.carbon.verifier.Verifier
 import viper.silver.verifier.{PartialVerificationError, reasons}
 import viper.carbon.boogie.Implicits._
 import viper.carbon.modules.components.{DefinednessComponent, DefinednessState}
-import viper.silver.ast.{LocationAccess, MagicWand, PredicateAccess, Ref}
 import viper.silver.ast.utility.Expressions
 
+import scala.annotation.unused
+
 /**
  * The default implementation of [[viper.carbon.modules.ExpModule]].
  */
@@ -480,7 +481,7 @@ class DefaultExpModule(val verifier: Verifier) extends ExpModule with Definednes
     * checks self-framedness of both sides of wand
     * GP: maybe should "MagicWandNotWellFormed" error
     */
-  private def checkDefinednessWand(e: sil.MagicWand, error: PartialVerificationError, makeChecks: Boolean): Stmt = {
+  private def checkDefinednessWand(e: sil.MagicWand, error: PartialVerificationError, @unused makeChecks: Boolean): Stmt = {
     val (initStmtLHS, curState): (Stmt, stateModule.StateSnapshot) = stateModule.freshEmptyState("WandDefLHS", true)
     val defStateLHS = stateModule.state
     val (initStmtRHS, _): (Stmt, stateModule.StateSnapshot) = stateModule.freshEmptyState("WandDefRHS", true)

src/main/scala/viper/carbon/modules/impls/DefaultFuncPredModule.scala

@@ -41,7 +41,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
   import heapModule._
   import permModule._
 
-  implicit val fpNamespace = verifier.freshNamespace("funcpred")
+  implicit val fpNamespace: Namespace = verifier.freshNamespace("funcpred")
 
   /* Maps function names to their height.
    * Previously mapped Function AST nodes to their height, but this prevents looking up functions
@@ -53,8 +53,6 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
   private val assumeFunctionsAboveName = Identifier("AssumeFunctionsAbove")
   private val assumeFunctionsAbove: Const = Const(assumeFunctionsAboveName)
-  private val specialRefName = Identifier("special_ref")
-  private val specialRef = Const(specialRefName)
 
   /* limitedPostfix is appended to the actual function name to get the name of the limited function.
    * It must be a string that cannot appear in Viper identifiers to ensure that we can easily check if a given identifier
@@ -321,7 +319,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
          pacc.args.forall(arg => !arg.existsDefined[Unit]({case v:sil.LocalVar if !silArgsLocalVar.contains(v) => }  ))
 
       outerUnfoldings.flatMap {
-        case Unfolding(PredicateAccessPredicate(predacc: PredicateAccess, perm), exp)
+        case Unfolding(PredicateAccessPredicate(predacc: PredicateAccess, _), _)
           if hasOnlyDefinedVars(predacc) => Some(predicateTrigger(heap map (_.l), predacc))
         case _ => None}.flatten
     }
@@ -345,7 +343,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
    * Transform all function applications to their limited form (or form used in triggers, if the "triggerForm" Boolean is passed as true.
    * If height is provided (i.e., non-negative), functions of above that height need not have their applications replaced with the limited form.
    */
-  private def transformFuncAppsToLimitedOrTriggerForm(exp: Exp, heightToSkip : Int = -1, triggerForm: Boolean = false): Exp = {
+  private def transformFuncAppsToLimitedOrTriggerForm(exp: Exp, heightToSkip : Int, triggerForm: Boolean): Exp = {
     def transformer: PartialFunction[Exp, Option[Exp]] = {
       case FuncApp(recf, recargs, t) if recf.namespace == fpNamespace &&
         // recf might refer to a limited function already if the function was marked as opaque.
@@ -447,7 +445,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
       pacc.args.forall(arg => !arg.existsDefined[Unit]({case v:sil.LocalVar if !silArgsLocalVar.contains(v) => }  ))
 
     val predicateTriggers : Seq[Exp] = outerUnfoldings.flatMap {
-      case Unfolding(PredicateAccessPredicate(predacc: PredicateAccess, perm), exp)
+      case Unfolding(PredicateAccessPredicate(predacc: PredicateAccess, _), _)
         if hasOnlyDefinedVars(predacc) => Some(predicateTrigger(heap map (_.l), predacc))
       case _ => None}.flatten
 
@@ -554,7 +552,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
     def frameFragment(e: Exp) = {
       FuncApp(frameFragmentName, Seq(e), frameType)
     }
-    assertion match {
+    (assertion: @unchecked) match {
       case s@sil.AccessPredicate(la, perm) =>
         val fragmentBody = translateResourceAccess(renaming(la).asInstanceOf[sil.LocationAccess])
         val fragment = if (s.isInstanceOf[PredicateAccessPredicate]) fragmentBody else frameFragment(fragmentBody)
@@ -600,7 +598,6 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
           val (_, curState) = stateModule.freshTempState("Heap2")
           val heap1 = heapModule.currentStateContributions
-          val mask1 = permModule.currentStateContributions
 
 
 
@@ -616,7 +613,6 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
           val (_, _) = stateModule.freshTempState("Heap1")
 
           val heap2 = heapModule.currentStateContributions
-          val mask2 = permModule.currentStateContributions
 
           val locationAccess2 = translateResourceAccess(locationAccess)
           val translatedCond2 = translateExp(renamedCond)
@@ -985,7 +981,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
   override def translateFold(fold: sil.Fold, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): (Stmt,Stmt) = {
     fold match {
-      case sil.Fold(acc@sil.PredicateAccessPredicate(pa@sil.PredicateAccess(_, _), perm)) => {
+      case sil.Fold(acc@sil.PredicateAccessPredicate(sil.PredicateAccess(_, _), perm)) => {
         {
           val (foldFirst, foldLast) = foldPredicate(acc, errors.FoldFailed(fold), statesStackForPackageStmt, insidePackageStmt)
           if(insidePackageStmt){
@@ -1005,7 +1001,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
   private var duringFold = false
   private var foldInfo: sil.PredicateAccessPredicate = null
   private def foldPredicate(acc: sil.PredicateAccessPredicate, error: PartialVerificationError
-                           , statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): (Stmt,Stmt) = {
+                           , statesStackForPackageStmt: List[Any], insidePackageStmt: Boolean): (Stmt,Stmt) = {
     duringFold = true
     foldInfo = acc
     val stmt = Assert(permModule.isStrictlyPositivePerm(acc.perm), error.dueTo(NonPositivePermission(acc.perm))) ++
@@ -1030,7 +1026,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
   private var unfoldInfo: sil.PredicateAccessPredicate = null
   override def translateUnfold(unfold: sil.Unfold, statesStackForPackageStmt: List[Any] = null, insidePackageStmt: Boolean = false): Stmt = {
     unfold match {
-      case sil.Unfold(acc@sil.PredicateAccessPredicate(pa@sil.PredicateAccess(_, _), perm)) =>
+      case sil.Unfold(acc@sil.PredicateAccessPredicate(sil.PredicateAccess(_, _), perm)) =>
         checkDefinedness(acc, errors.UnfoldFailed(unfold), insidePackageStmt = insidePackageStmt) ++
           // If no permission amount is supplied explicitly, we always use the default FullPerm; this is
           // okay even if we are inside a function and only want to check for some positive amount, because permission
@@ -1121,8 +1117,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
 
           (before, after)
       }
-      case pap@sil.PredicateAccessPredicate(loc@sil.PredicateAccess(args, predicateName), _) if duringUnfold =>
-        val oldVersion = LocalVar(Identifier("oldVersion"), predicateVersionType)
+      case sil.PredicateAccessPredicate(loc@sil.PredicateAccess(args, predicateName), _) if duringUnfold =>
         val newVersion = LocalVar(Identifier("newVersion"), predicateVersionType)
         val stmt: Stmt = if (exhaleTmpStateId >= 0 || duringUnfolding) Nil else //(oldVersion := curVersion) ++
            Havoc(Seq(newVersion)) ++
@@ -1168,7 +1163,7 @@ with DefinednessComponent with ExhaleComponent with InhaleComponent {
         CommentBlock("Execute unfolding (for extra information)",stmts)
       }
 
-      case pap@sil.PredicateAccessPredicate(loc@sil.PredicateAccess(_, _), perm) =>
+      case pap@sil.PredicateAccessPredicate(loc@sil.PredicateAccess(_, _), _) =>
         val res: Stmt = if (extraUnfolding) {
           exhaleTmpStateId += 1
           extraUnfolding = false