From b02dc7c578484bf136281547e85c2ae45305396b Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 15 Jan 2025 16:15:48 +0100 Subject: [PATCH 1/2] Removed minimal cuts to allow parsing #833 --- src/main/scala/viper/silver/parser/FastParser.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/parser/FastParser.scala b/src/main/scala/viper/silver/parser/FastParser.scala index eae845045..666e15141 100644 --- a/src/main/scala/viper/silver/parser/FastParser.scala +++ b/src/main/scala/viper/silver/parser/FastParser.scala @@ -46,7 +46,7 @@ object FastParserCompanion { implicit def PositionParsing[T](p: => P[Pos => T]) = new PositionParsing(() => p) implicit def ExtendedParsing[T](p: => P[T]) = new ExtendedParsing(() => p) implicit def reservedKw[$: P, T <: PKeyword](r: T)(implicit lineCol: LineCol, _file: Path): P[PReserved[T]] = P(P(r.token).map { _ => PReserved(r)(_) } ~~ !identContinues)./.pos - implicit def reservedSym[$: P, T <: PSymbol](r: T)(implicit lineCol: LineCol, _file: Path): P[PReserved[T]] = P(r.token./ map { _ => PReserved(r)(_) }).pos + implicit def reservedSym[$: P, T <: PSymbol](r: T)(implicit lineCol: LineCol, _file: Path): P[PReserved[T]] = P(P(r.token) map { _ => PReserved(r)(_) }).pos class LeadingWhitespace[T](val p: () => P[T]) extends AnyVal { /** @@ -422,7 +422,7 @@ class FastParser { def identifier[$: P]: P[Unit] = identStarts ~~ identContinues.repX - def annotationIdentifier[$: P]: P[PRawString] = P((identStarts ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).!./ map PRawString.apply).pos + def annotationIdentifier[$: P]: P[PRawString] = P((identStarts ~~ CharIn("0-9", "A-Z", "a-z", "$_.").repX).! map PRawString.apply).pos def ident[$: P]: P[String] = identifier.!.filter(a => !keywords.contains(a)).opaque("identifier") From 44dc671a0b004c6b0df462cf365129b413d590a9 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Wed, 15 Jan 2025 16:31:01 +0100 Subject: [PATCH 2/2] Added test --- src/test/resources/all/issues/silver/0833.vpr | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 src/test/resources/all/issues/silver/0833.vpr 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