Fixing #833 with NoCut (#842)

Author: marcoeilers

Diff for: 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 for: 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