From ecc03b5360ad4983451b99981151b2fafd51da76 Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 2 Sep 2022 17:29:14 +0200
Subject: [PATCH 1/2] Ignoring function bodies as well for finding
 qpFields/qpPredicates

---
 .../viper/silver/ast/utility/QuantifiedPermissions.scala    | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 76e589655..7568e05c4 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -104,6 +104,9 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
+        case Function(_, _, _, pres, posts, _) =>
+          // use only specification of called functions
+          pres ++ posts
         case _ => Seq(currentRoot)
       }
 
@@ -134,6 +137,9 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
+        case Function(_, _, _, pres, posts, _) =>
+          // use only specification of called functions
+          pres ++ posts
         case _ => Seq(currentRoot)
       }
 

From bac52241529d58f6a572cb3ac05d3fc57710240a Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Fri, 2 Sep 2022 17:59:51 +0200
Subject: [PATCH 2/2] Forgot to always include body of root function

---
 .../viper/silver/ast/utility/QuantifiedPermissions.scala      | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
index 7568e05c4..6b994cef9 100644
--- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
+++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
@@ -104,7 +104,7 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
-        case Function(_, _, _, pres, posts, _) =>
+        case f@Function(_, _, _, pres, posts, _) if f != root=>
           // use only specification of called functions
           pres ++ posts
         case _ => Seq(currentRoot)
@@ -137,7 +137,7 @@ object QuantifiedPermissions {
         case m@Method(_, _, _, pres, posts, _) if m != root =>
           // use only specification of called methods
           pres ++ posts
-        case Function(_, _, _, pres, posts, _) =>
+        case f@Function(_, _, _, pres, posts, _) if f != root =>
           // use only specification of called functions
           pres ++ posts
         case _ => Seq(currentRoot)