fixes PredicateInstance plugin to propagate a predicate instance's po…

…sitional information to not only the generatated PredicateAccessPredicate but also PredicateAccess as the latter is used as offending node in the resulting reason
viperproject · Jan 31, 2025 · 1ee7b4d · 1ee7b4d
1 parent 4833685
commit 1ee7b4d
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala b/src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala
@@ -64,11 +64,13 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
         case None =>
           val piFunctionName = s"PI_${predicateInstance.p}"
           val pred = program.findPredicate(predicateInstance.p)
+          val predicateAccess = PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)
+          val predicateAccessPredicate = PredicateAccessPredicate(predicateAccess, Some(WildcardPerm()()))(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)
           val newPIFunction =
             Function(piFunctionName,
               pred.formalArgs,
               DomainType(PredicateInstanceDomain.get, Map()),
-              Seq(PredicateAccessPredicate(PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(), Some(WildcardPerm()()))(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)),
+              Seq(predicateAccessPredicate),
               Seq(),
               None
             )(PredicateInstanceDomain.get.pos, PredicateInstanceDomain.get.info)