Merge pull request #681 from viperproject/meilers_term_pred_fix

Two fixes for VerifyThis issues
viperproject · Apr 24, 2023 · 8101fe1 · 8101fe1
2 parents 6e2ce95 + cb4f1e5
commit 8101fe1
Show file tree

Hide file tree

Showing 4 changed files with 33 additions and 0 deletions.
diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
@@ -464,6 +464,7 @@ case class Function(name: String, formalArgs: Seq[LocalVarDecl], typ: Type, pres
       Seq(ConsistencyError("Function post-conditions must not have old expressions.", p.pos)) else Seq()}) ++
     (pres ++ posts).flatMap(Consistency.checkNoPermForpermExceptInhaleExhale) ++
     (if(!(body forall (_ isSubtype typ))) Seq(ConsistencyError("Type of function body must match function type.", pos)) else Seq() ) ++
+    (posts flatMap (p => if (!Consistency.noPerm(p) || !Consistency.noForPerm(p)) Seq(ConsistencyError("perm and forperm expressions are not allowed in function postconditions", p.pos)) else Seq() )) ++
     pres.flatMap(Consistency.checkPre) ++
     posts.flatMap(Consistency.checkPost) ++
     posts.flatMap(p => if (!Consistency.noPermissions(p))

diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -79,6 +79,9 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
       case pc@PCall(idnUse, args, None) if input.predicates.exists(_.idndef.name == idnUse.name) =>
         // PCall represents the predicate access before the translation into the AST
         PPredicateInstance(args, idnUse)(pc.pos)
+      case PAccPred(pa@PPredicateAccess(args, idnuse), _) => PPredicateInstance(args, idnuse)(pa.pos)
+      case PAccPred(pc@PCall(idnUse, args, None), _) if input.predicates.exists(_.idndef.name == idnUse.name) =>
+        PPredicateInstance(args, idnUse)(pc.pos)
       case d => d
     }).recurseFunc({
       case PUnfolding(_, exp) => // ignore predicate access when it is used for unfolding

diff --git a/src/test/resources/all/permission_introspection/forpermCheck.vpr b/src/test/resources/all/permission_introspection/forpermCheck.vpr
@@ -3,6 +3,10 @@
 
 field f1: Int
 
+function permInPost(x: Ref): Int
+  //:: ExpectedOutput(consistency.error)
+  ensures [perm(x.f1) == none, true]
+
 method permUse()
 {
   var r1: Ref

diff --git a/src/test/resources/termination/methods/basic/someTypes.vpr b/src/test/resources/termination/methods/basic/someTypes.vpr
@@ -33,4 +33,29 @@ method predicateTest2(xs: Ref)
     fold list(xs)
     //:: ExpectedOutput(termination.failed:tuple.false)
     predicateTest2(xs)
+}
+
+method predicateTest3(xs: Ref)
+    requires acc(list(xs), 2/3)
+    decreases acc(list(xs), 2/3)
+    ensures acc(list(xs), 2/3)
+{
+    unfold acc(list(xs), 2/3)
+    if (xs.next != null) {
+        predicateTest3(xs.next)
+    }
+    fold acc(list(xs), 2/3)
+}
+
+method predicateTest4(xs: Ref)
+    requires acc(list(xs), 2/3)
+    decreases acc(list(xs), 2/3)
+    ensures acc(list(xs), 2/3)
+{
+    unfold acc(list(xs), 2/3)
+    if (xs.next != null) {
+    }
+    fold acc(list(xs), 2/3)
+    //:: ExpectedOutput(termination.failed:tuple.false)
+    predicateTest4(xs)
 }