Fix some compiler warnings (#423)

* Fix some compiler warnings

* Address Linard's comments

* Add .gobra to gitignore

.gitignore

@@ -18,6 +18,7 @@ logger.log
 /src/main/java/viper/gobra/frontend/GobraParser.interp
 /src/main/java/viper/gobra/frontend/GobraParser.tokens
 /gen/
+/.gobra/
 
 .bloop/
 .metals/

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -16,7 +16,6 @@ import viper.gobra.reporting.VerifierError
 import viper.gobra.util.{Decimal, NumBase}
 import viper.silver.ast.{LineColumnPosition, SourcePosition}
 
-import java.security.MessageDigest
 import scala.collection.immutable
 
 // TODO: comment describing identifier positions (resolution)

src/main/scala/viper/gobra/frontend/InformativeErrorListener.scala

@@ -9,12 +9,13 @@ package viper.gobra.frontend
 import org.antlr.v4.runtime.misc.IntervalSet
 import org.antlr.v4.runtime.{BaseErrorListener, CommonTokenStream, FailedPredicateException, InputMismatchException, Lexer, NoViableAltException, Parser, RecognitionException, Recognizer, Token}
 import org.bitbucket.inkytonik.kiama.util.{FileSource, Source}
-import viper.gobra.frontend.GobraParser.{CapContext, EosContext, ExpressionContext, ImplementationProofContext, RULE_blockWithBodyParameterInfo, RULE_eos, RULE_shortVarDecl, RULE_type_, RULE_varDecl, Slice_Context, TypeSpecContext, Type_Context, VarSpecContext, ruleNames}
+import viper.gobra.frontend.GobraParser._
 import viper.gobra.frontend.Source.FromFileSource
 import viper.gobra.reporting.ParserError
 import viper.silver.ast.SourcePosition
 
 import java.nio.file.Path
+import scala.annotation.unused
 import scala.collection.mutable.ListBuffer
 
 class InformativeErrorListener(val messages: ListBuffer[ParserError], val source: Source) extends BaseErrorListener {
@@ -32,9 +33,8 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     // We don't analyze Lexer errors any further: The defaults are sufficient
     val error = recognizer match {
       case lexer: Lexer => DefaultErrorType()(LexerErrorContext(lexer, null, line, charPositionInLine, msg))
-      case parser: Parser => {
+      case parser: Parser =>
         analyzeParserError(ParserErrorContext(parser, offendingSymbol.asInstanceOf[Token], line, charPositionInLine, msg), e)
-      }
     }
 
     // Depending on the source, get the applicable type of position information
@@ -80,12 +80,12 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     * @param exception
     * @return
     */
-  def analyzeFailedPredicate(implicit context: ParserErrorContext, exception: FailedPredicateException): ErrorType = {
+  def analyzeFailedPredicate(implicit context: ParserErrorContext, @unused exception: FailedPredicateException): ErrorType = {
     val parser = context.recognizer
     parser.getContext match {
       // One example of a known pattern: Parser reads ':=' when expecting the end of statement: The user probably
       // used ':=' instead of '='
-      case _ : GobraParser.EosContext => {
+      case _: GobraParser.EosContext => {
         context.offendingSymbol.getType match {
           // An unexpected := was encountered, perhaps the user meant =
           case GobraParser.DECLARE_ASSIGN => GotAssignErrorType()
@@ -123,7 +123,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     * @param exception
     * @return
     */
-  def analyzeInputMismatch(implicit context: ParserErrorContext, exception: InputMismatchException): ErrorType = {
+  def analyzeInputMismatch(implicit context: ParserErrorContext, @unused exception: InputMismatchException): ErrorType = {
     (context.offendingSymbol.getType, context.recognizer.getContext) match {
       case (Token.EOF, _) => DefaultMismatch()
       // Again, we have an unexpected :=, so suggest using a =
@@ -145,18 +145,18 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     val parser = context.recognizer
     val ctx = parser.getContext
     ctx match {
-      case slice : Slice_Context => {
+      case _: Slice_Context => {
         // Missing either the second or second and third argument (or completely wrong)
         SliceMissingIndex()
       }
-      case _ : VarSpecContext | _ : Type_Context if context.offendingSymbol.getType == GobraParser.DECLARE_ASSIGN => GotAssignErrorType()
-      case eos : EosContext => {
+      case _: VarSpecContext | _: Type_Context if context.offendingSymbol.getType == GobraParser.DECLARE_ASSIGN => GotAssignErrorType()
+      case _: EosContext => {
         parser.getTokenStream.LT(2).getType match {
           case GobraParser.DECLARE_ASSIGN => GotAssignErrorType()(context.copy(offendingSymbol = parser.getTokenStream.LT(2)))
           case _ => DefaultNoViable(exception)
         }
       }
-      case e : ExpressionContext if e.parent.isInstanceOf[CapContext] => SliceMissingIndex(3)
+      case e: ExpressionContext if e.parent.isInstanceOf[CapContext] => SliceMissingIndex(3)
       case _ if new_reserved.contains(context.offendingSymbol.getType) => ReservedWord()
       case _ => DefaultNoViable(exception)
     }
@@ -184,14 +184,10 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     var message = lines(offendingToken.getLine - 1)
     val rest = message.length
     message += "\n"
-    for (i <- 0 until offendingToken.getCharPositionInLine) {
-      message += " "
-    }
+    message += " " * offendingToken.getCharPositionInLine
     val start = offendingToken.getCharPositionInLine
     val stop = if (restOfTheLine) rest else offendingToken.getCharPositionInLine + offendingToken.getText.length
-    if (start >= 0 && stop >= 0) for (_ <- start until stop) {
-      message += "^"
-    }
+    if (start >= 0 && stop >= 0) { message += "^" * (stop - start) }
     message += "\n"
     message
   }
@@ -203,7 +199,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     * @param context
     * @return
     */
-  def getRuleDisplay(index : Int)(implicit context : ParserErrorContext): String = {
+  def getRuleDisplay(index : Int): String = {
     betterRuleNames.getOrElse(index, ruleNames(index))
   }
 
@@ -221,10 +217,9 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
   /**
     * The same as [[betterRuleNames]], but for tokens.
     * @param t
-    * @param context
     * @return
     */
-  def getTokenDisplay(t : Token)(implicit context : ParserErrorContext): String = {
+  def getTokenDisplay(t : Token): String = {
     t.getText match {
       case "\n" => "end of line"
       case s => s
@@ -259,7 +254,7 @@ class InformativeErrorListener(val messages: ListBuffer[ParserError], val source
     val context: ErrorContext
     val msg : String
     lazy val expected : IntervalSet = context.recognizer match {
-      case lexer: Lexer => IntervalSet.EMPTY_SET
+      case _: Lexer => IntervalSet.EMPTY_SET
       case parser: Parser => parser.getExpectedTokens
     }
     lazy val underlined : String = underlineError(context)

src/main/scala/viper/gobra/frontend/ParseTreeTranslator.scala

@@ -377,8 +377,8 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     */
   override def visitResult(ctx: GobraParser.ResultContext): PResult = {
     super.visitResult(ctx) match {
-      case res : Vector[Vector[PParameter]] => PResult(res.flatten).at(ctx)
-      case typ : PType => PResult(Vector(PUnnamedParameter(typ).at(typ))).at(ctx)
+      case res: Vector[Vector[PParameter]] => PResult(res.flatten).at(ctx)
+      case typ: PType => PResult(Vector(PUnnamedParameter(typ).at(typ))).at(ctx)
     }
   }
 
@@ -931,6 +931,7 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
       case idnUseLike(id) => id match {
         case id@PIdnUse(_) => PNamedOperand(id).at(id)
         case PWildcard() => PBlankIdentifier().at(ctx)
+        case _ => unexpected(ctx)
       }
       case _ => unexpected(ctx)
     }
@@ -1573,10 +1574,10 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
       }
       PAssignmentWithOp(right match {
         case Vector(r) => r
-        case Vector(_*) => fail(ctx.expressionList(0), "Assignments with operators can only have exactly one right-hand expression.")
+        case _ => fail(ctx.expressionList(0), "Assignments with operators can only have exactly one right-hand expression.")
       }, ass_op, left match {
         case Vector(l) => l
-        case Vector(_*) => fail(ctx.expressionList(0), "Assignments with operators can only have exactly one left-hand expression.")
+        case _ => fail(ctx.expressionList(0), "Assignments with operators can only have exactly one left-hand expression.")
       }).at(ctx)
     }
     else {
@@ -1770,11 +1771,12 @@ class ParseTreeTranslator(pom: PositionManager, source: Source, specOnly : Boole
     val cond = visitNodeOrNone[PExpression](ctx.expression())
     visitExpressionList(ctx.expressionList()) match {
       case Vector(PBlankIdentifier()) => PWildcardMeasure(cond).at(ctx)
-      case exprs@Vector(_, _*) => PTupleTerminationMeasure(exprs, cond).at(ctx)
+      case exprs if exprs.nonEmpty => PTupleTerminationMeasure(exprs, cond).at(ctx)
       case Vector() => PTupleTerminationMeasure(Vector.empty, cond).at(ctx.parent match {
         case s : SpecStatementContext => s.DEC()
         case l : LoopSpecContext => l.DEC()
       })
+      case _ => unexpected(ctx)
     }
   }
 

src/main/scala/viper/gobra/frontend/Parser.scala

@@ -313,12 +313,11 @@ object Parser {
     }
 
     def parse(rule : => Rule): Either[Vector[ParserError], Node] = {
-      val name = source.name
       val tree = try rule
       catch {
         case _: AmbiguityException => parse_LL(rule) // Resolve `<IDENTIFIER> { }` ambiguities in switch/if-statements
         case _: ParseCancellationException => parse_LL(rule) // For even faster parsing, replace with `new ParserRuleContext()`.
-        case e => errors.append(ParserError(e.getMessage, Some(SourcePosition(source.toPath, 0, 0)))); new ParserRuleContext()
+        case e: Throwable => errors.append(ParserError(e.getMessage, Some(SourcePosition(source.toPath, 0, 0)))); new ParserRuleContext()
       }
       if(errors.isEmpty) {
         val translator = new ParseTreeTranslator(pom, source, specOnly)
@@ -330,13 +329,13 @@ object Parser {
                 case _ => None
               }
               return Left(Vector(ParserError(e.getMessage + " " + e.getStackTrace.toVector(1), pos)))
-            case e : UnsupportedOperatorException =>
+            case e: UnsupportedOperatorException =>
               val pos = source match {
                 case fileSource: FromFileSource => Some(SourcePosition(fileSource.path, e.cause.startPos.line, e.cause.endPos.column))
                 case _ => None
               }
               return Left(Vector(ParserError(e.getMessage + " " + e.getStackTrace.toVector(0), pos)))
-            case e =>
+            case e: Throwable =>
               val pos = source match {
                 case fileSource: FromFileSource => Some(SourcePosition(fileSource.path, 0, 0))
                 case _ => None

src/main/scala/viper/gobra/frontend/ReportFirstErrorStrategy.scala

@@ -7,7 +7,7 @@
 package viper.gobra.frontend
 
 import org.antlr.v4.runtime.misc.ParseCancellationException
-import org.antlr.v4.runtime.{BailErrorStrategy, DefaultErrorStrategy, FailedPredicateException, InputMismatchException, Parser, ParserRuleContext, RecognitionException, Token}
+import org.antlr.v4.runtime.{BailErrorStrategy, DefaultErrorStrategy, FailedPredicateException, InputMismatchException, Parser, RecognitionException, Token}
 import viper.gobra.frontend.GobraParser.{BlockContext, ExprSwitchStmtContext}
 
 /**

src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala

@@ -53,6 +53,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl =>
     attr[PExpression, AddrMod] {
       case PNamedOperand(id) => addressableVar(id)
       case PBlankIdentifier() => AddrMod.defaultValue
+      case _: PTypeExpr => AddrMod.defaultValue
       case _: PDeref => AddrMod.dereference
       case PIndexedExp(base, _) =>
         val baseType = underlyingType(exprType(base))

src/main/scala/viper/gobra/frontend/info/implementation/typing/BuiltInMemberTyping.scala

@@ -153,6 +153,7 @@ trait BuiltInMemberTyping extends BaseTyping { this: TypeInfoImpl =>
         FunctionT(Vector(predArgType), AssertionT)
       })
     }
+    case t: BuiltInTypeTag => Violation.violation(s"typ not defined for ${t.name}")
   }
 
   /** ghost typing for arguments of BuiltInMemberTag tag */
@@ -175,6 +176,8 @@ trait BuiltInMemberTyping extends BaseTyping { this: TypeInfoImpl =>
           Violation.violation(s"argGhostTyping not defined for ${t.name}")
         }
     }
+
+    case t: BuiltInTypeTag => Violation.violation(s"argGhostTyping not defined for ${t.name}")
   }
 
   /** ghost typing for return values of BuiltInMemberTag tag */
@@ -201,6 +204,7 @@ trait BuiltInMemberTyping extends BaseTyping { this: TypeInfoImpl =>
           Violation.violation(s"returnGhostTyping not defined for ${t.name}")
         }
     }
+    case t: BuiltInTypeTag => Violation.violation(s"returnGhostTyping not defined for ${t.name}")
 
   }
 

src/main/scala/viper/gobra/frontend/info/implementation/typing/ExprTyping.scala

@@ -929,6 +929,8 @@ trait ExprTyping extends BaseTyping { this: TypeInfoImpl =>
             val typeRight = exprOrTypeType(bExpr.right)
             typeMerge(typeLeft, typeRight).getOrElse(UnknownType)
         }
+
+      case e => violation(s"unexpected expression $e while type-checking integer expressions.")
     }
 
     // handle cases where it returns a SingleMultiTuple and we only care about a single type

src/main/scala/viper/gobra/frontend/info/implementation/typing/IdTyping.scala

@@ -132,7 +132,7 @@ trait IdTyping extends BaseTyping { this: TypeInfoImpl =>
       case NamedType(decl, _, context) => DeclaredT(decl, context)
       case TypeAlias(decl, _, context) => context.symbType(decl.right)
       case Import(decl, _) => ImportT(decl)
-      case BuiltInType(tag, rep, context) => tag.typ
+      case BuiltInType(tag, _, _) => tag.typ
       case _ => violation(s"expected type, but got $id")
     }
   }

src/main/scala/viper/gobra/frontend/info/implementation/typing/ghost/GhostExprTyping.scala

@@ -315,7 +315,7 @@ trait GhostExprTyping extends BaseTyping { this: TypeInfoImpl =>
 
       case _: PMagicWand => !strong
 
-      case _: PBoolLit | _: PIntLit | _: PNilLit | _: PStringLit => true
+      case _: PBoolLit | _: PIntLit | _: PNilLit | _: PStringLit | _: PFloatLit => true
 
       // Might change at some point
       case n: PInvoke => (exprOrType(n.base), resolve(n)) match {

src/test/scala/viper/gobra/erasing/GhostErasureUnitTests.scala

@@ -293,7 +293,6 @@ class GhostErasureUnitTests extends AnyFunSuite with Matchers with Inside {
     }
 
     def testProg(inputProg: String, expectedErasedProg: String): Assertion = {
-      val config = Config()
       val inputParseAst = Parser.parseProgram(StringSource(inputProg, "Input Program"))
       val ghostlessProg = inputParseAst match {
         case Right(prog) => ghostLessProg(prog)