Gobra reports reveal parser error if there is a parser error somewhere else
Similar to #899 using a reveal clause will mark the location of the reveal clause as a parser error if there is a syntax error somewhere else. For example, in the following snippet, the line with the reveal will be marked as incorrect, despite the parser error being on the next line.
opaque
decreases
pure func tmp() bool{
return 1 > 0
}
preserves acc(arr)
func tmp2(arr []int) {
reveal tmp()
thismakesnosense*/
}
For this, the following error is printed:
> unexpected end of line, expecting arguments
[info] reveal tmp()
A fix like the one from #940 does not seem to work. Probably because primaryExpr can also contain parentheses. Maybe we can find a similar syntactic way
So far, I found two possible solutions for an improved syntax. In the rule for reveal (REVEAL primaryExpr arguments) we can either put the parentheses only around primaryExpr (allowing something like REVEAL (func)()) or use characters that are not in use to put primaryExpr and arguments together within those characters, e.g. REVEAL ~func()~. Again (like in #940), in both cases, we can make the grammar alternative, s.t. the old syntax is still accepted but one can also use the improved one to prevent the parser from showing a syntax error at the reveal clause even if the error is somewhere else.