more warnings

src/main/vct/importer/Util.scala

@@ -36,7 +36,7 @@ case object Util {
 
   def loadJavaClass[G](readable: Readable): JavaClass[G] =
     ColJavaParser(ReadableOriginProvider(readable), ConstantBlameProvider(LibraryFileBlame)).parse(readable).decls match {
-      case Seq(javaNamespace: JavaNamespace[G]) => javaNamespace.declarations match {
+      case Seq(javaNamespace: JavaNamespace[G @unchecked]) => javaNamespace.declarations match {
         case Seq(javaClass: JavaClass[G]) => javaClass
         case seq => throw JavaLoadError("Expected to load exactly one Java class but found " + seq.size)
       }

src/main/vct/main/modes/Verify.scala

@@ -91,8 +91,8 @@ case object Verify extends LazyLogging {
   }
 
   def friendlyHandleBipReport(report: VerificationReport, path: Option[PathOrStd]): Unit = (report, path) match {
-    case (report, Some(path)) if report.nonEmpty() => path.write(w => w.write(report.toJson()))
-    case (report, None) if report.nonEmpty() => logger.warn("JavaBIP verification report was produced, but no output path was specified. Use `--bip-report-file` to specify an output. See `--help` for more info.")
-    case (report, None) if report.isEmpty() =>
+    case (report, _) if report.isEmpty() =>
+    case (report, Some(path)) => path.write(w => w.write(report.toJson()))
+    case (report, None) => logger.warn("JavaBIP verification report was produced, but no output path was specified. Use `--bip-report-file` to specify an output. See `--help` for more info.")
   }
 }

src/parsers/vct/parsers/transform/LLVMContractToCol.scala

@@ -9,6 +9,7 @@ import vct.col.ast._
 import vct.col.origin.{ExpectedError, Origin, SourceNameOrigin}
 import vct.col.ref.{Ref, UnresolvedRef}
 import vct.col.util.AstBuildHelpers.{ff, foldAnd, implies, tt}
+import vct.parsers.ParseError
 
 import scala.annotation.nowarn
 import scala.collection.immutable.{AbstractSeq, LinearSeq}
@@ -144,6 +145,7 @@ case class LLVMContractToCol[G](override val originProvider: OriginProvider,
           case LLVMSpecParserPatterns.Or(_) => BitOr(left, right)
           case Xor(_) => BitXor(left, right)
         }
+        case other => throw ParseError(left.o, s"Expected an integer or boolean expression here, but got `$other`")
       }
     }
   }

src/rewrite/vct/rewrite/ClassToRef.scala

@@ -268,6 +268,9 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
       case function: InstanceFunction[Pre] => Result[Post](functionSucc.ref(function))(e.o)
       case procedure: Procedure[Pre] => Result[Post](succ(procedure))(e.o)
       case method: InstanceMethod[Pre] => Result[Post](methodSucc.ref(method))(e.o)
+      case function: InstanceOperatorFunction[Pre] => throw ExcludedByPassOrder("Instance operator functions are already compiled away", Some(function))
+      case method: InstanceOperatorMethod[Pre] => throw ExcludedByPassOrder("Instance operator methods are already compiled away", Some(method))
+      case function: LlvmSpecFunction[Pre] => throw ExcludedByPassOrder("Llvm spec functions are already compiled away", Some(function))
     }
     case _ => rewriteDefault(e)
   }

src/rewrite/vct/rewrite/EncodeCurrentThread.scala

@@ -46,6 +46,7 @@ case class EncodeCurrentThread[Pre <: Generation]() extends Rewriter[Pre] {
     // PB: although a pure method will become a function, it should really be possible to mark a pure method as thread
     // local.
     case m: AbstractMethod[Pre] => !m.pure
+    case m: LlvmFunctionDefinition[Pre] => !m.pure
 
     case _: ADTFunction[Pre] => false
     case _: ProverFunction[Pre] => false

src/rewrite/vct/rewrite/EncodeExtract.scala

@@ -2,7 +2,7 @@ package vct.col.rewrite
 import vct.col.ast._
 import vct.col.origin._
 import vct.col.ref.Ref
-import vct.col.rewrite.EncodeExtract.{ExtractMayNotJumpOut, ExtractMayNotReturn, ExtractedOnlyPost, FramedProofPostconditionFailed, FramedProofPreconditionFailed, LoopInvariantPreconditionFailed}
+import vct.col.rewrite.EncodeExtract.{ExtractMayNotJumpOut, ExtractMayNotReturn, ExtractedOnlyPost, FramedProofPostconditionFailed, FramedProofPreconditionFailed, LoopInvariantPreconditionFailed, WrongExtractNode}
 import vct.col.util.AstBuildHelpers.contract
 import vct.col.util.Substitute
 import vct.result.VerificationError.UserError
@@ -11,6 +11,11 @@ case object EncodeExtract extends RewriterBuilder {
   override def key: String = "extract"
   override def desc: String = "Extract contracted nodes into separate methods"
 
+  case class WrongExtractNode(node: Statement[_]) extends UserError {
+    override def code: String = "wrongExtract"
+    override def text: String = node.o.messageInContext("This kind of node cannot be extracted into a separate method")
+  }
+
   case class ExtractedOnlyPost(blame: Blame[PostconditionFailed]) extends Blame[CallableFailure] {
     override def blame(error: CallableFailure): Unit = error match {
       case error: PostconditionFailed => blame.blame(error)
@@ -142,6 +147,8 @@ case class EncodeExtract[Pre <: Generation]() extends Rewriter[Pre] {
           post,
           FramedProofPostconditionFailed(proof),
         )(extract.o)
+
+      case other => throw WrongExtractNode(other)
     }
 
     case other => rewriteDefault(other)

src/rewrite/vct/rewrite/EncodeForkJoin.scala

@@ -51,9 +51,9 @@ object EncodeForkJoin extends RewriterBuilder {
   case class ForkInstanceInvocation(fork: Fork[_]) extends Blame[InstanceInvocationFailure] {
     override def blame(error: InstanceInvocationFailure): Unit = error match {
       case InstanceNull(_) => fork.blame.blame(ForkNull(fork))
-      case PreconditionFailed(Nil, _, _) => throw BlamePathError
       case PreconditionFailed(FailLeft +: _, _, _) => fork.blame.blame(RunnableNotIdle(fork))
       case PreconditionFailed(FailRight +: _, failure, _) => fork.blame.blame(RunnablePreconditionNotEstablished(fork, failure))
+      case PreconditionFailed(_, _, _) => throw BlamePathError
       case ContextEverywhereFailedInPre(_, _) => PanicBlame("fork method does not have c_e").blame(error)
     }
   }

src/rewrite/vct/rewrite/EncodeProofHelpers.scala

@@ -42,6 +42,7 @@ case object EncodeProofHelpers extends RewriterBuilderArg[Boolean] {
         proof.blame.blame(FramedProofPreFailed(failure, proof))
       case LoopInvariantNotMaintained(failure, _) =>
         proof.blame.blame(FramedProofPostFailed(failure, proof))
+      case LoopTerminationMeasureFailed(_) => PanicBlame("There is no termination measure here").blame(error)
     }
   }
 }

src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala

@@ -134,6 +134,7 @@ case class LangSpecificToCol[Pre <: Generation]() extends Rewriter[Pre] with Laz
         case RefInstanceMethod(decl) => Result[Post](anySucc(decl))
         case RefInstanceOperatorFunction(decl) => Result[Post](anySucc(decl))
         case RefInstanceOperatorMethod(decl) => Result[Post](anySucc(decl))
+        case RefLlvmSpecFunction(decl) => Result[Post](anySucc(decl))
       }
 
     case diz @ AmbiguousThis() =>

src/rewrite/vct/rewrite/veymont/StructureCheck.scala

@@ -88,6 +88,7 @@ case class StructureCheck[Pre <: Generation]() extends Rewriter[Pre] {
           else throw VeyMontStructCheckError(st, "A method call on a thread object may only refer to same thread in its arguments!")
         case _ => throw VeyMontStructCheckError(st, "This kind of method call is not allowed in seq_program")
       }
+      case _ => throw VeyMontStructCheckError(st, "This is not a method call")
     }
   }
 }

src/viper/viper/api/backend/silicon/Util.scala

@@ -18,7 +18,7 @@ case object Util {
     o match {
       case None => ProgressRender(message)
       case Some(o) if short => ProgressRender(s"$message `${o.inlineContext}`")
-      case Some(o) if !short =>
+      case Some(o) =>
         val lines = o.messageInContext(message).split("\n")
         ProgressRender(lines, lines.size - 2)
     }

src/viper/viper/api/transform/ColToSilver.scala

@@ -358,6 +358,7 @@ case class ColToSilver(program: col.Program[_]) {
         silver.FieldAccessPredicate(silver.FieldAccess(exp(obj), fields(field.decl))(pos=pos(loc), info=expInfo(e)), silver.WildcardPerm()())(pos=pos(e), info=expInfo(e))
       case col.PredicateLocation(predicate, args) =>
         silver.PredicateAccessPredicate(silver.PredicateAccess(args.map(exp), ref(predicate))(pos = pos(loc), NodeInfo(loc)), silver.WildcardPerm()())(pos = pos(e), expInfo(e))
+      case default => ??(default)
     }
     case col.Local(v) => silver.LocalVar(ref(v), typ(v.decl.t))(pos=pos(e), info=expInfo(e))
     case col.SilverDeref(obj, ref) => silver.FieldAccess(exp(obj), fields(ref.decl))(pos=pos(e), info=expInfo(e))

src/viper/viper/api/transform/SilverToCol.scala

@@ -259,6 +259,9 @@ case class SilverToCol[G](program: silver.Program, blameProvider: BlameProvider)
 
     case silver.Package(wand, proofScript) => ??(s)
     case silver.Apply(exp) => ??(s)
+    case silver.Quasihavoc(_, _) => ??(s)
+    case silver.Quasihavocall(_, _, _) => ??(s)
+
     case stmt: silver.ExtensionStmt => ??(stmt)
   }
 
@@ -364,6 +367,7 @@ case class SilverToCol[G](program: silver.Program, blameProvider: BlameProvider)
       case silver.Or(left, right) => col.Or(f(left), f(right))
       case silver.PermAdd(left, right) => col.Plus(f(left), f(right))
       case silver.PermDiv(left, right) => col.Div(f(left), f(right))(blame(e))
+      case silver.PermPermDiv(left, right) => col.Div(f(left), f(right))(blame(e))
       case silver.PermGeCmp(left, right) => col.GreaterEq(f(left), f(right))
       case silver.PermGtCmp(left, right) => col.Greater(f(left), f(right))
       case silver.PermLeCmp(left, right) => col.LessEq(f(left), f(right))