Apply suggestions from code review

Co-authored-by: Linard Arquint <[email protected]>
viperproject · Jun 24, 2024 · 9bb7f88 · 9bb7f88
1 parent 695c91b
commit 9bb7f88
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraphMap.scala b/src/main/scala/viper/silver/plugin/standard/reasoning/analysis/VarAnalysisGraphMap.scala
@@ -44,9 +44,9 @@ object AnalysisUtils {
     LocalVarDecl(l.name, l.typ)()
   }
 
-  def containsDecreasesAnnotations(m: Method): (Boolean, Boolean) = {
-    val presContain = m.pres.collect({ case DecreasesTuple(_, _) | DecreasesWildcard(_) | DecreasesStar() => true }).nonEmpty
-    val postsContain = m.posts.collect({ case DecreasesTuple(_, _) | DecreasesWildcard(_) | DecreasesStar() => true }).nonEmpty
+  def specifiesTermination(m: Method): (Boolean, Boolean) = {
+    val presContain = m.pres.collect({ case DecreasesTuple(_, _) | DecreasesWildcard(_) => true }).nonEmpty
+    val postsContain = m.posts.collect({ case DecreasesTuple(_, _) | DecreasesWildcard(_) => true }).nonEmpty
 
     val presContainStar = m.pres.collect({ case DecreasesStar() => true }).nonEmpty
     val postsContainStar = m.posts.collect({ case DecreasesStar() => true }).nonEmpty
@@ -63,7 +63,7 @@ object AnalysisUtils {
       case _ => false
     }
 
-    val containsTerminationMeasure = presContain | postsContain | presContainStar | postsContainStar | infoContains
+    val containsTerminationMeasure = presContain | postsContain | presContainStar | postsContainStar | infoContains | infoContainsStar
     val mightNotTerminate = !containsTerminationMeasure | presContainStar | postsContainStar | infoContainsStar
 
     (containsTerminationMeasure, mightNotTerminate)