From bca538c32115d5dd3267123526f1afaa353de57a Mon Sep 17 00:00:00 2001 From: Lea Salome Brugger Date: Tue, 9 Jul 2024 15:02:53 +0200 Subject: [PATCH] Clean up error transformations for closures --- .../encodings/closures/ClosureSpecsEncoder.scala | 8 ++++---- .../encodings/closures/MethodObjectEncoder.scala | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala index 611748049..4a94e9d59 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala +++ b/src/main/scala/viper/gobra/translator/encodings/closures/ClosureSpecsEncoder.scala @@ -8,7 +8,7 @@ package viper.gobra.translator.encodings.closures import viper.gobra.ast.internal.FunctionLikeMemberOrLit import viper.gobra.ast.{internal => in} -import viper.gobra.reporting.BackTranslator.ErrorTransformer +import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage} import viper.gobra.reporting.{GoCallPreconditionReason, PreconditionError, Source, SpecNotImplementedByClosure} import viper.gobra.theory.Addressability import viper.gobra.translator.Names @@ -313,10 +313,10 @@ protected class ClosureSpecsEncoder { } private var implementAssertionSpecOriginToStr: Map[Source.AbstractOrigin, String] = Map.empty - private def doesNotImplementSpecErr(callNode: vpr.Node, closureStr: String): ErrorTransformer = { - case vprerr.PreconditionInCallFalse(node@Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (callNode eq node) && implementAssertionSpecOriginToStr.contains(assInfo.origin) => + private def doesNotImplementSpecErr(callNode: vpr.Node with vpr.Positioned, closureStr: String): ErrorTransformer = { + case e@vprerr.PreconditionInCallFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (e causedBy callNode) && implementAssertionSpecOriginToStr.contains(assInfo.origin) => PreconditionError(info).dueTo(SpecNotImplementedByClosure(info, closureStr, implementAssertionSpecOriginToStr(assInfo.origin))) - case vprerr.PreconditionInAppFalse(node@Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (callNode eq node) && implementAssertionSpecOriginToStr.contains(assInfo.origin) => + case e@vprerr.PreconditionInAppFalse(Source(info), reasons.AssertionFalse(Source(assInfo)), _) if (e causedBy callNode) && implementAssertionSpecOriginToStr.contains(assInfo.origin) => PreconditionError(info).dueTo(SpecNotImplementedByClosure(info, closureStr, implementAssertionSpecOriginToStr(assInfo.origin))) } diff --git a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala b/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala index d5d368920..a4a0e7d9b 100644 --- a/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala +++ b/src/main/scala/viper/gobra/translator/encodings/closures/MethodObjectEncoder.scala @@ -7,7 +7,7 @@ package viper.gobra.translator.encodings.closures import viper.gobra.ast.{internal => in} -import viper.gobra.reporting.BackTranslator.ErrorTransformer +import viper.gobra.reporting.BackTranslator.{ErrorTransformer, RichErrorMessage} import viper.gobra.reporting.{InterfaceReceiverIsNilReason, MethodObjectGetterPreconditionError, Source} import viper.gobra.translator.Names import viper.gobra.translator.context.Context @@ -102,7 +102,7 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) { in.MethodProxy(s"${Names.closureGetter}$$${meth.name}", s"${Names.closureGetter}$$${meth.uniqueName}")(meth.info) private def receiverNilErr(m: in.MethodObject, call: vpr.Exp): ErrorTransformer = { - case vprerr.PreconditionInAppFalse(offendingNode, _, _) if call eq offendingNode => + case e@vprerr.PreconditionInAppFalse(_, _, _) if e causedBy call=> val info = m.vprMeta._2.asInstanceOf[Source.Verifier.Info] val recvInfo = m.recv.vprMeta._2.asInstanceOf[Source.Verifier.Info] MethodObjectGetterPreconditionError(info).dueTo(InterfaceReceiverIsNilReason(recvInfo))