Merge pull request #605 from viperproject/meilers_precise_quantified_…

…fields Ignoring function bodies as well for finding qpFields/qpPredicates
viperproject · Sep 2, 2022 · 9b7d6bc · 9b7d6bc
2 parents 3007816 + bac5224
commit 9b7d6bc
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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 f@Function(_, _, _, pres, posts, _) if f != root=>
+          // 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 f@Function(_, _, _, pres, posts, _) if f != root =>
+          // use only specification of called functions
+          pres ++ posts
         case _ => Seq(currentRoot)
       }