diff --git a/src/main/vct/importer/Util.scala b/src/main/vct/importer/Util.scala index 780eadd871..2e4139e0a4 100644 --- a/src/main/vct/importer/Util.scala +++ b/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) } diff --git a/src/main/vct/main/modes/Verify.scala b/src/main/vct/main/modes/Verify.scala index 2f96e274df..f16c47a5d4 100644 --- a/src/main/vct/main/modes/Verify.scala +++ b/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.") } } diff --git a/src/parsers/vct/parsers/transform/LLVMContractToCol.scala b/src/parsers/vct/parsers/transform/LLVMContractToCol.scala index 955fd67ba8..0ca0568770 100644 --- a/src/parsers/vct/parsers/transform/LLVMContractToCol.scala +++ b/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`") } } } diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala index ba1d8b1466..7f9df92a2b 100644 --- a/src/rewrite/vct/rewrite/ClassToRef.scala +++ b/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) } diff --git a/src/rewrite/vct/rewrite/EncodeCurrentThread.scala b/src/rewrite/vct/rewrite/EncodeCurrentThread.scala index ecc98b7ff8..0828875966 100644 --- a/src/rewrite/vct/rewrite/EncodeCurrentThread.scala +++ b/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 diff --git a/src/rewrite/vct/rewrite/EncodeExtract.scala b/src/rewrite/vct/rewrite/EncodeExtract.scala index 328d6c78d8..b7c324324e 100644 --- a/src/rewrite/vct/rewrite/EncodeExtract.scala +++ b/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) diff --git a/src/rewrite/vct/rewrite/EncodeForkJoin.scala b/src/rewrite/vct/rewrite/EncodeForkJoin.scala index 5d0039785b..f9010545c8 100644 --- a/src/rewrite/vct/rewrite/EncodeForkJoin.scala +++ b/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) } } diff --git a/src/rewrite/vct/rewrite/EncodeProofHelpers.scala b/src/rewrite/vct/rewrite/EncodeProofHelpers.scala index 5ff2991999..744ffd566c 100644 --- a/src/rewrite/vct/rewrite/EncodeProofHelpers.scala +++ b/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) } } } diff --git a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala b/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala index 0b131c0fe7..7e1786bb06 100644 --- a/src/rewrite/vct/rewrite/lang/LangSpecificToCol.scala +++ b/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() => diff --git a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala b/src/rewrite/vct/rewrite/veymont/StructureCheck.scala index 28380a2822..fdbfb52ce4 100644 --- a/src/rewrite/vct/rewrite/veymont/StructureCheck.scala +++ b/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") } } } diff --git a/src/viper/viper/api/backend/silicon/Util.scala b/src/viper/viper/api/backend/silicon/Util.scala index 60d548f3c3..439b41c52c 100644 --- a/src/viper/viper/api/backend/silicon/Util.scala +++ b/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) } diff --git a/src/viper/viper/api/transform/ColToSilver.scala b/src/viper/viper/api/transform/ColToSilver.scala index 928de29efd..0b1bfa1377 100644 --- a/src/viper/viper/api/transform/ColToSilver.scala +++ b/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)) diff --git a/src/viper/viper/api/transform/SilverToCol.scala b/src/viper/viper/api/transform/SilverToCol.scala index b99284ad80..85d2a994be 100644 --- a/src/viper/viper/api/transform/SilverToCol.scala +++ b/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))