-
Notifications
You must be signed in to change notification settings - Fork 48
Closed
Description
The following viper program leads to a parse error even though it is a valid program:
function gggg(a: Int): Int
decreases
@opaque()
function hhhh(a: Int): Int
decreasesError:
[info] Silicon found 1 error in 0.73s:
[info] [0] Parse error: Expected (parens | atom):31:1, found "function h". Occurred while parsing: annotated:26:1 / functionDecl:26:10 / delimitedTrailing:26:27 / precondition:27:3 / decreases:27:3 / decreasesTuple:30:1 / delimited:30:1 / exp:30:1 / expParen:30:1 / iteExpr:30:1 / iffExp:30:1 / implExp:30:1 / magicWandExp:30:1 / orExp:30:1 / andExp:30:1 / eqExpParen:30:1 / cmpExp:30:1 / sum:30:1 / term:30:1 / suffixExpr:30:1 / atomParen:30:1 / atom:30:1 / annotatedAtom:30:1 / atomParen:31:1 (playground.vpr@31.1--31.1)
Surprisingly, adding a body fixes to the function before the opaque annotation fixes the issue. The following program is accepted.
function gggg(a: Int): Int
decreases
{ 0 }
@opaque()
function hhhh(a: Int): Int
decreasesReactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels