Fixing #833 with NoCut (#842)

viperproject · Feb 5, 2025 · 924804b · 924804b
1 parent 75fe55c
commit 924804b
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 1 deletion.
diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala
@@ -47,7 +47,7 @@ class TerminationPlugin(@unused reporter: viper.silver.reporter.Reporter,
   def decreases[$: P]: P[PSpecification[PDecreasesKeyword.type]] =
     P((P(PDecreasesKeyword) ~ (decreasesWildcard | decreasesStar | decreasesTuple)) map (PSpecification.apply _).tupled).pos
   def decreasesTuple[$: P]: P[PDecreasesTuple] =
-    P((exp.delimited(PSym.Comma) ~~~ condition.lw.?) map (PDecreasesTuple.apply _).tupled).pos
+    P((NoCut(exp).delimited(PSym.Comma) ~~~ condition.lw.?) map (PDecreasesTuple.apply _).tupled).pos
   def decreasesWildcard[$: P]: P[PDecreasesWildcard] = P((P(PWildcardSym) ~~~ condition.lw.?) map (PDecreasesWildcard.apply _).tupled).pos
   def decreasesStar[$: P]: P[PDecreasesStar] = P(P(PSym.Star) map (PDecreasesStar(_) _)).pos
   def condition[$: P]: P[(PReserved[PIfKeyword.type], PExp)] = P(P(PIfKeyword) ~ exp)

diff --git a/src/test/resources/all/issues/silver/0833.vpr b/src/test/resources/all/issues/silver/0833.vpr
@@ -0,0 +1,9 @@
+// Any copyright is dedicated to the Public Domain.
+// http://creativecommons.org/publicdomain/zero/1.0/
+
+function gggg(a: Int): Int
+  decreases
+
+@opaque()
+function hhhh(a: Int): Int
+  decreases