gobra icon indicating copy to clipboard operation
gobra copied to clipboard

Gobra reports reveal parser error if there is a parser error somewhere else

Open ThomasMayerl opened this issue 8 months ago • 2 comments

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

ThomasMayerl avatar May 13 '25 08:05 ThomasMayerl

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

ThomasMayerl avatar Jun 29 '25 09:06 ThomasMayerl

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.

ThomasMayerl avatar Jul 01 '25 07:07 ThomasMayerl