Skip to content

Commit 18fd658

Browse files
committed
Disallow newlines between fn idn and opening paren
1 parent c0dd2c8 commit 18fd658

2 files changed

Lines changed: 11 additions & 2 deletions

File tree

src/main/scala/viper/silver/parser/FastParser.scala

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -705,9 +705,11 @@ class FastParser {
705705

706706
def newExpFields[$: P]: P[Option[Seq[PIdnUse]]] = P(P("*").map(_ => None) | P(idnuse.rep(sep = ","./)).map(Some(_)))
707707

708-
def funcApp[$: P]: P[PCall] = FP(idnuse ~ parens(actualArgList)).map {
709-
case (pos, (func, args)) =>
708+
def funcApp[$: P]: P[PCall] = FP(idnuse ~~ FP(" ".repX(1)).? ~~ parens(actualArgList)).map {
709+
case (pos, (func, Some((space, _)), args)) =>
710+
_warnings = _warnings :+ ParseWarning("Whitespace between a function identifier and the opening paren is deprecated, remove the spaces", SourcePosition(_file, space._1, space._2))
710711
PCall(func, args, None)(pos)
712+
case (pos, (func, None, args)) => PCall(func, args, None)(pos)
711713
}
712714

713715
def maybeTypedFuncApp[$: P](bracketed: Boolean): P[PCall] = P(if (!bracketed) funcApp else FP(funcApp ~~~ (":" ~/ typ).lw.?).map {
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
field f: Bool
2+
method bar(a: Bool, b: Seq[Ref])
3+
requires |b| > 0 && acc(b[0].f)
4+
{
5+
assume a
6+
(b[..1][0]).f := a
7+
}

0 commit comments

Comments
 (0)