Skip to content

Commit

Permalink
Merge pull request #836 from viperproject/arquintl-fix-predicate-inst…
Browse files Browse the repository at this point in the history
…ance-position

Fixes missing positional information in error reason caused by PredicateInstance plugin
  • Loading branch information
ArquintL authored Jan 31, 2025
2 parents 4833685 + 1ee7b4d commit 16a0027
Showing 1 changed file with 3 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 16a0027

Please sign in to comment.