From 133264d5a400fad85f1f17e2c48ecff166f5094b Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 9 Oct 2024 19:48:21 +0200 Subject: [PATCH 1/2] Allow custom error message for assertion failures via @msg annotation --- .../silver/verifier/VerificationError.scala | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala index 4ee3f6d45..ba1f0b7aa 100644 --- a/src/main/scala/viper/silver/verifier/VerificationError.scala +++ b/src/main/scala/viper/silver/verifier/VerificationError.scala @@ -399,6 +399,24 @@ object errors { val id = "assert.failed" val text = "Assert might fail." + val customMessageAnnotation = "msg" + + def customErrorMessage = offendingNode.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains(customMessageAnnotation) && ai.values(customMessageAnnotation).nonEmpty => + Some(ai.values("msg").head) + case _ => None + } + + override def readableMessage: String = customErrorMessage match { + case Some(msg) => msg + case None => super.readableMessage + } + + override def readableMessage(withId: Boolean, withPosition: Boolean): String = customErrorMessage match { + case Some(msg) => msg + case None => super.readableMessage(withId, withPosition) + } + override def pos = offendingNode.exp.pos def withNode(offendingNode: errors.ErrorNode = this.offendingNode) = AssertFailed(offendingNode.asInstanceOf[Assert], this.reason, this.cached) def withReason(r: ErrorReason) = AssertFailed(offendingNode, r, cached) From f77c1b82fa8ad5a0ef41ed0521b9f2e31021fd5c Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 8 Nov 2024 14:51:27 +0100 Subject: [PATCH 2/2] Allowing message annotations on any offending node --- .../silver/verifier/VerificationError.scala | 26 ++++++++++++++----- 1 file changed, 20 insertions(+), 6 deletions(-) diff --git a/src/main/scala/viper/silver/verifier/VerificationError.scala b/src/main/scala/viper/silver/verifier/VerificationError.scala index ba1f0b7aa..c14de9b9d 100644 --- a/src/main/scala/viper/silver/verifier/VerificationError.scala +++ b/src/main/scala/viper/silver/verifier/VerificationError.scala @@ -231,7 +231,23 @@ sealed abstract class AbstractVerificationError extends VerificationError { def pos = offendingNode.pos - def readableMessage(withId: Boolean, withPosition: Boolean) = { + val customMessageAnnotation = "msg" + + def customErrorMessage = offendingNode match { + case i: Infoed => i.info.getUniqueInfo[AnnotationInfo] match { + case Some(ai) if ai.values.contains(customMessageAnnotation) && ai.values(customMessageAnnotation).nonEmpty => + Some(ai.values("msg").head) + case _ => None + } + case _ => None + } + + def readableMessage(withId: Boolean, withPosition: Boolean) = customErrorMessage match { + case Some(msg) => msg + case _ => defaultReadableMessage(withId, withPosition) + } + + def defaultReadableMessage(withId: Boolean, withPosition: Boolean) = { val idStr = if (withId) s"[$fullId] " else "" val posStr = if (withPosition) s" ($pos)" else "" @@ -399,20 +415,18 @@ object errors { val id = "assert.failed" val text = "Assert might fail." - val customMessageAnnotation = "msg" - - def customErrorMessage = offendingNode.info.getUniqueInfo[AnnotationInfo] match { + def customAssertErrorMessage = offendingNode.info.getUniqueInfo[AnnotationInfo] match { case Some(ai) if ai.values.contains(customMessageAnnotation) && ai.values(customMessageAnnotation).nonEmpty => Some(ai.values("msg").head) case _ => None } - override def readableMessage: String = customErrorMessage match { + override def readableMessage: String = customAssertErrorMessage match { case Some(msg) => msg case None => super.readableMessage } - override def readableMessage(withId: Boolean, withPosition: Boolean): String = customErrorMessage match { + override def readableMessage(withId: Boolean, withPosition: Boolean): String = customAssertErrorMessage match { case Some(msg) => msg case None => super.readableMessage(withId, withPosition) }