Merge pull request #749 from pieter-bos/seal-verification-errors

Seal VerificationError and ErrorReason?

Author: marcoeilers

src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstanceErrors.scala

@@ -6,10 +6,12 @@
 
 package viper.silver.plugin.standard.predicateinstance
 
-import viper.silver.verifier.{AbstractVerificationError, ErrorMessage, ErrorReason}
+import viper.silver.verifier.{AbstractVerificationError, ErrorMessage, ErrorReason, ExtensionAbstractVerificationError}
 import viper.silver.verifier.reasons.ErrorNode
 
-case class PredicateInstanceNoAccess(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean) extends AbstractVerificationError {
+sealed abstract class PredicateInstanceError extends ExtensionAbstractVerificationError
+
+case class PredicateInstanceNoAccess(override val offendingNode: ErrorNode, override val reason: ErrorReason, override val cached: Boolean) extends PredicateInstanceError {
   override protected def text: String = "Accessing predicate instance might fail."
 
   override def withReason(reason: ErrorReason): AbstractVerificationError = PredicateInstanceNoAccess(this.offendingNode, this.reason, cached)

src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala

@@ -8,7 +8,10 @@ package viper.silver.plugin.standard.refute
 
 import viper.silver.verifier._
 
-case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends AbstractVerificationError {
+sealed abstract class RefuteError extends ExtensionAbstractVerificationError
+sealed abstract class RefuteErrorReason extends ExtensionAbstractErrorReason
+
+case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends RefuteError {
   override val id = "refute.failed"
   override val text = "Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
 
@@ -18,7 +21,7 @@ case class RefuteFailed(override val offendingNode: Refute, override val reason:
   override def withReason(r: ErrorReason): RefuteFailed = RefuteFailed(offendingNode, r, cached)
 }
 
-case class RefutationTrue(offendingNode: reasons.ErrorNode) extends AbstractErrorReason {
+case class RefutationTrue(offendingNode: reasons.ErrorNode) extends RefuteErrorReason {
   override val id: String = "refutation.true"
 
   override val readableMessage: String = s"Assertion $offendingNode definitely holds."

src/main/scala/viper/silver/plugin/standard/termination/TerminationErrors.scala

@@ -17,10 +17,12 @@ import viper.silver.verifier._
 /**
  * Error for all termination related failed assertions.
  */
-abstract class AbstractTerminationError() extends AbstractVerificationError {
+sealed abstract class AbstractTerminationError extends ExtensionAbstractVerificationError {
   override val id = "termination.failed"
 }
 
+sealed abstract class TerminationErrorReason extends ExtensionAbstractErrorReason
+
 case class FunctionTerminationError(override val offendingNode: ErrorNode,
                                     override val reason: ErrorReason,
                                     override val cached: Boolean = false) extends AbstractTerminationError {
@@ -59,39 +61,39 @@ case class LoopTerminationError(override val offendingNode: ErrorNode,
  Reasons for all termination related failed assertions.
  */
 
-case class TerminationConditionFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TerminationConditionFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "termination.condition.false"
 
   override val readableMessage: String = s"Required termination condition might not hold."
 
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TerminationConditionFalse(offendingNode)
 }
 
-case class TupleConditionFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleConditionFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.condition.false"
 
   override val readableMessage: String = s"Required tuple condition might not hold."
 
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TupleConditionFalse(offendingNode)
 }
 
-case class TupleSimpleFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleSimpleFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.false"
 
   override val readableMessage: String = s"Termination measure might not decrease or might not be bounded."
 
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TupleSimpleFalse(offendingNode)
 }
 
-case class TupleDecreasesFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleDecreasesFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.false"
 
   override val readableMessage: String = s"Termination measure might not decrease."
 
   override def withNode(offendingNode: ErrorNode): ErrorMessage = TupleDecreasesFalse(offendingNode)
 }
 
-case class TupleBoundedFalse(offendingNode: ErrorNode) extends AbstractErrorReason {
+case class TupleBoundedFalse(offendingNode: ErrorNode) extends TerminationErrorReason {
   override val id: String = "tuple.false"
 
   override val readableMessage: String = s"Termination measure might not bounded."

src/main/scala/viper/silver/verifier/VerificationError.scala

@@ -160,7 +160,7 @@ trait ErrorMessage {
   }
 }
 
-trait VerificationError extends AbstractError with ErrorMessage {
+sealed trait VerificationError extends AbstractError with ErrorMessage {
   def reason: ErrorReason
   def readableMessage(withId: Boolean = false, withPosition: Boolean = false): String
   override def readableMessage: String = {
@@ -196,7 +196,7 @@ case object DummyReason extends AbstractErrorReason {
   def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = DummyReason
 }
 
-trait ErrorReason extends ErrorMessage
+sealed trait ErrorReason extends ErrorMessage
 
 trait PartialVerificationError {
   def f: ErrorReason => VerificationError
@@ -226,7 +226,7 @@ case object NullPartialVerificationError extends PartialVerificationError {
   def f = _ => null
 }
 
-abstract class AbstractVerificationError extends VerificationError {
+sealed abstract class AbstractVerificationError extends VerificationError {
   protected def text: String
 
   def pos = offendingNode.pos
@@ -253,11 +253,15 @@ abstract class AbstractVerificationError extends VerificationError {
   override def toString = readableMessage(true, true) + (if (cached) " - cached" else "")
 }
 
-abstract class AbstractErrorReason extends ErrorReason {
+abstract class ExtensionAbstractVerificationError extends AbstractVerificationError
+
+sealed abstract class AbstractErrorReason extends ErrorReason {
   def pos = offendingNode.pos
   override def toString = readableMessage
 }
 
+abstract class ExtensionAbstractErrorReason extends AbstractErrorReason
+
 object errors {
   type ErrorNode = Node with Positioned with TransformableErrors with Rewritable
 

src/test/scala/IOTests.scala

@@ -165,14 +165,16 @@ class IOTests extends AnyFunSuite with Matchers {
 
     override def verify(program: Program): VerificationResult = {
       if (pass) Success
-      else Failure(Seq(new VerificationError {
+      else Failure(Seq(new ExtensionAbstractVerificationError {
         override def reason: ErrorReason = DummyReason
         override def readableMessage(withId: Boolean, withPosition: Boolean): String =
           "MockIOVerifier failed the verification (as requested)."
-        override def withNode(offendingNode: ErrorNode): ErrorMessage = DummyReason
+        override def withNode(offendingNode: ErrorNode): ErrorMessage = this
         override def pos: Position = NoPosition
         override def offendingNode: ErrorNode = DummyNode
         override def id: String = "MockIOVerifier.verification.failure"
+        override protected def text: String = ""
+        override def withReason(reason: ErrorReason): AbstractVerificationError = this
       }))
     }