From 1ee7b4da82841b6e34f541f0b7906fbd718ad1ff Mon Sep 17 00:00:00 2001 From: Linard Arquint Date: Fri, 31 Jan 2025 10:19:13 +0100 Subject: [PATCH] fixes PredicateInstance plugin to propagate a predicate instance's positional information to not only the generatated PredicateAccessPredicate but also PredicateAccess as the latter is used as offending node in the resulting reason --- .../standard/predicateinstance/PredicateInstancePlugin.scala | 4 +++- 1 file changed, 3 insertions(+), 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 index 450f72ff5..637bb7027 100644 --- 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)