From 7fc491462d6683f44dd668f3cc0f9a36a96ebe23 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Mon, 24 Apr 2023 12:25:11 +0200
Subject: [PATCH] Fixes in termination plugin, consistency for perm in function
 posts, tests

---
 src/main/scala/viper/silver/ast/Program.scala |  1 +
 .../termination/TerminationPlugin.scala       |  3 +++
 .../permission_introspection/forpermCheck.vpr |  4 +++
 .../termination/methods/basic/someTypes.vpr   | 25 +++++++++++++++++++
 4 files changed, 33 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala
index 3362a0e26..f9a409985 100644
--- 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
index 0fe3f9612..8baa5fb3d 100644
--- 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
index 43b8b6001..2ef01d6a6 100644
--- 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
index 65c5cc29d..b3a55f7f2 100644
--- 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)
 }
\ No newline at end of file