From 924804b27ea5f1663e4dcaed9a6f13bedf26979d Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 5 Feb 2025 12:19:56 +0100 Subject: [PATCH] Fixing #833 with NoCut (#842) --- .../plugin/standard/termination/TerminationPlugin.scala | 2 +- src/test/resources/all/issues/silver/0833.vpr | 9 +++++++++ 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 src/test/resources/all/issues/silver/0833.vpr diff --git a/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala b/src/main/scala/viper/silver/plugin/standard/termination/TerminationPlugin.scala index 1aa3261f9..50f8fe5c8 100644 --- 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 new file mode 100644 index 000000000..8bc891639 --- /dev/null +++ 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 \ No newline at end of file