Merge pull request #721 from mimo31/pred-acc-arg-purity-check

Add purity checks for predicate access arguments
viperproject · Jul 13, 2023 · a28b06f · a28b06f
2 parents d769c1e + 828d434
commit a28b06f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 0 deletions.
diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala
@@ -455,6 +455,7 @@ case class PredicateAccess(args: Seq[Exp], predicateName: String)
 
   def loc(p:Program) = p.findPredicate(predicateName)
   lazy val typ = Bool
+  override lazy val check : Seq[ConsistencyError] = args.flatMap(Consistency.checkPure)
 
   /** The body of the predicate with the arguments instantiated correctly. */
   def predicateBody(program : Program, scope: Set[String]) = {

diff --git a/src/test/resources/all/issues/silver/0720.vpr b/src/test/resources/all/issues/silver/0720.vpr
@@ -0,0 +1,9 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+predicate p(flag: Bool)
+
+method client() {
+    //:: ExpectedOutput(consistency.error)
+    inhale p(p(false))
+}