Skip to content

Commit 16a0027

Browse files
authored
Merge pull request #836 from viperproject/arquintl-fix-predicate-instance-position
Fixes missing positional information in error reason caused by PredicateInstance plugin
2 parents 4833685 + 1ee7b4d commit 16a0027

1 file changed

Lines changed: 3 additions & 1 deletion

File tree

src/main/scala/viper/silver/plugin/standard/predicateinstance/PredicateInstancePlugin.scala

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -64,11 +64,13 @@ class PredicateInstancePlugin(@unused reporter: viper.silver.reporter.Reporter,
6464
case None =>
6565
val piFunctionName = s"PI_${predicateInstance.p}"
6666
val pred = program.findPredicate(predicateInstance.p)
67+
val predicateAccess = PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)
68+
val predicateAccessPredicate = PredicateAccessPredicate(predicateAccess, Some(WildcardPerm()()))(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)
6769
val newPIFunction =
6870
Function(piFunctionName,
6971
pred.formalArgs,
7072
DomainType(PredicateInstanceDomain.get, Map()),
71-
Seq(PredicateAccessPredicate(PredicateAccess(pred.formalArgs.map(_.localVar), pred.name)(), Some(WildcardPerm()()))(predicateInstance.pos, predicateInstance.info, predicateInstance.errT)),
73+
Seq(predicateAccessPredicate),
7274
Seq(),
7375
None
7476
)(PredicateInstanceDomain.get.pos, PredicateInstanceDomain.get.info)

0 commit comments

Comments
 (0)