Merge branch 'master' into meilers_pretty_printer_linebreaks

Author: jcp19

build.sbt

@@ -14,7 +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
+  "-Ypatmat-exhaust-depth", "40",     // 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/Ast.scala

@@ -358,9 +358,9 @@ trait Info {
       case _ => Seq.empty
     }
 
-  def removeUniqueInfo[T <: Info]: Info = this match {
+  def removeUniqueInfo[T <: Info : ClassTag]: Info = this match {
     case ConsInfo(a, b) => MakeInfoPair(a.removeUniqueInfo[T], b.removeUniqueInfo[T])
-    case t: T => NoInfo
+    case _: T => NoInfo
     case info => info
   }
 }

src/main/scala/viper/silver/ast/Expression.scala

@@ -396,7 +396,7 @@ case class DomainFuncApp(funcname: String, args: Seq[Exp], typVarMap: Map[TypeVa
   //Strangely, the copy method is not a member of the DomainFuncApp case class,
   //therefore, We need this method that does the copying manually
   def copy(funcname: String = this.funcname, args: Seq[Exp] = this.args, typVarMap: Map[TypeVar, Type] = this.typVarMap): (Position, Info, Type, String, ErrorTrafo) => DomainFuncApp ={
-    DomainFuncApp(this.funcname,args,typVarMap)
+    DomainFuncApp(funcname,args,typVarMap)
   }
 }
 object DomainFuncApp {
@@ -410,7 +410,7 @@ case class BackendFuncApp(backendFunc: BackendFunc, args: Seq[Exp])
                          (val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos)
   extends AbstractDomainFuncApp {
   override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
-  override def func = (p: Program) => backendFunc
+  override def func = (_: Program) => backendFunc
   def funcname = backendFunc.name
   override def typ = backendFunc.typ
 }
@@ -565,6 +565,7 @@ case class Forall(variables: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp
   //require(isValid, s"Invalid quantifier: { $this } .")
   override lazy val check : Seq[ConsistencyError] =
     (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of universal quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++
+    (if (variables.isEmpty) Seq(ConsistencyError("Quantifier must have at least one quantified variable.", pos)) else Seq()) ++
     Consistency.checkAllVarsMentionedInTriggers(variables, triggers) ++
     checkNoNestedQuantsForQuantPermissions ++
     checkQuantifiedPermission
@@ -631,7 +632,8 @@ case class Forall(variables: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp
 /** Existential quantification. */
 case class Exists(variables: Seq[LocalVarDecl], triggers: Seq[Trigger], exp: Exp)(val pos: Position = NoPosition, val info: Info = NoInfo, val errT: ErrorTrafo = NoTrafos) extends QuantifiedExp {
   override lazy val check : Seq[ConsistencyError] = Consistency.checkPure(exp) ++
-    (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of existential quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq())
+    (if(!(exp isSubtype Bool)) Seq(ConsistencyError(s"Body of existential quantifier must be of Bool type, but found ${exp.typ}", exp.pos)) else Seq()) ++
+    (if (variables.isEmpty) Seq(ConsistencyError("Quantifier must have at least one quantified variable.", pos)) else Seq())
 
   /** Returns an identical forall quantification that has some automatically generated triggers
     * if necessary and possible.

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -8,7 +8,7 @@ package viper.silver.ast.utility
 
 import viper.silver.ast._
 import viper.silver.ast.utility.rewriter.Traverse
-import viper.silver.parser.{FastParser, FastParserCompanion}
+import viper.silver.parser.FastParserCompanion
 import viper.silver.verifier.ConsistencyError
 import viper.silver.{FastMessage, FastMessaging}
 

src/main/scala/viper/silver/ast/utility/Functions.scala

@@ -25,7 +25,7 @@ object Functions {
   def allSubexpressionsIncludingUnfoldings(program: Program)(func: Function): Seq[Exp] = {
     var visitedPredicates = Set[String]()
     var subexpressions = allSubexpressions(func)
-    var unfoldings = new ListBuffer[Unfolding]
+    val unfoldings = new ListBuffer[Unfolding]
     unfoldings ++= (subexpressions map (e => e.deepCollect{case u@Unfolding(_, _) => u})).flatten
     var i = 0
     while (i < unfoldings.length){

src/main/scala/viper/silver/ast/utility/ViperStrategy.scala

@@ -179,13 +179,13 @@ object ViperStrategy {
               Trafos(
                 newMetaData._3.eTransformations,
                 newMetaData._3.rTransformations,
-                newMetaData._3.nTransformations.orElse(Some(n.asInstanceOf[ErrorNode])))
+                newMetaData._3.nTransformations.orElse(Some(n)))
             } else {
               /* Keep already attached transformations (if any) */
               newMetaData._3
             }
           }
-          now
+          now.withMeta(newMetaData._1, newMetaData._2, newNodeTrafo)
         } else {
           now
         }

src/main/scala/viper/silver/ast/utility/rewriter/Strategy.scala

@@ -7,6 +7,7 @@
 package viper.silver.ast.utility.rewriter
 import viper.silver.ast.utility.rewriter.Traverse.Traverse
 
+import scala.annotation.unused
 import scala.collection.mutable
 import scala.reflect.runtime.{universe => reflection}
 
@@ -92,7 +93,7 @@ trait StrategyInterface[N <: Rewritable] {
     *                          rewritten.
     * @return Updated node that will be built into the AST
     */
-  protected def preserveMetaData(old: N, now: N, directlyRewritten: Boolean): N = now
+  protected def preserveMetaData(@unused old: N, now: N, @unused directlyRewritten: Boolean): N = now
 }
 
 /**

src/main/scala/viper/silver/ast/utility/rewriter/TRegex.scala

@@ -6,6 +6,7 @@
 
 package viper.silver.ast.utility.rewriter
 
+import scala.annotation.unused
 import scala.reflect.runtime.{universe => reflection}
 
 /*
@@ -140,10 +141,10 @@ class NMatch[N <: Rewritable : TypeTag](val pred: N => Boolean, val rewrite: Boo
 
   /**
     * Provide information about the actions that occur if node n matches on this matcher
-    * @param n node used for traversion
-    * @return list of traversion infos
+    * @param n node used for traversal
+    * @return list of traversal infos
     */
-  def getTransitionInfo(n: Rewritable): Seq[TransitionInfo] = if (rewrite) Seq(MarkedForRewrite()) else Seq.empty[TransitionInfo]
+  def getTransitionInfo(@unused n: Rewritable): Seq[TransitionInfo] = if (rewrite) Seq(MarkedForRewrite()) else Seq.empty[TransitionInfo]
 
 }
 

src/main/scala/viper/silver/cfg/utility/LoopDetector.scala

@@ -8,7 +8,6 @@ package viper.silver.cfg.utility
 
 import java.util.concurrent.atomic.AtomicInteger
 
-import viper.silver.ast.utility.ViperStrategy
 import viper.silver.ast.utility.rewriter.Traverse
 import viper.silver.ast.{Exp, If, Info, Infoed, LocalVar, MakeInfoPair, NoInfo, Seqn, Stmt}
 import viper.silver.cfg._

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -242,7 +242,7 @@ trait SilFrontend extends DefaultFrontend {
                 Succ({e.initProperties(); e})
               }
               else Fail(err_list)
-            case fail @ Parsed.Failure(_, index, extra) =>
+            case fail @ Parsed.Failure(_, index, _) =>
               val msg = fail.trace().longAggregateMsg
               val (line, col) = fp.lineCol.getPos(index)
               Fail(List(ParseError(s"Expected $msg", SourcePosition(file, line, col))))