From 267d03574582a937ea9a97458154301374e39690 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 | 8 ++++---- 2 files changed, 8 insertions(+), 8 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..1616421a0 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 @@ -42,7 +42,7 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) { arg <- ctx.expression(m.recv) func = genConversion(m.recv.typ, m.meth)(ctx) call = vpr.FuncApp(func = func, args = Seq(arg))(pos, info, errT) - _ <- errorT(receiverNilErr(m, call)) + _ <- errorT(receiverNilErr(m)) } yield call } @@ -101,8 +101,8 @@ class MethodObjectEncoder(domain: ClosureDomainEncoder) { private def getterFunctionProxy(meth: in.MethodProxy): in.MethodProxy = 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 => + private def receiverNilErr(m: in.MethodObject): ErrorTransformer = { + case e@vprerr.PreconditionInAppFalse(offendingNode, _, _) if e causedBy offendingNode => val info = m.vprMeta._2.asInstanceOf[Source.Verifier.Info] val recvInfo = m.recv.vprMeta._2.asInstanceOf[Source.Verifier.Info] MethodObjectGetterPreconditionError(info).dueTo(InterfaceReceiverIsNilReason(recvInfo))