Clean up error transformations for closures

viperproject · Jul 10, 2024 · bca538c · bca538c
1 parent 6bfc8a0
commit bca538c
Show file tree

Hide file tree

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