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") 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