Clean up error transformations for closures

viperproject · Jul 9, 2024 · 267d035 · 267d035
1 parent 6bfc8a0
commit 267d035
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 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
@@ -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
@@ -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))