Skip to content

Cannot parse a macro containing a perm expression #502

Open
@fpoli

Description

@fpoli

Is it possible to apply a perm expression on a parameter of a macro? The following doesn't parse:

define check(expr) {
    assert perm(expr) < write
}

Error message:

Parse error: Expected found "perm(expr) < write\n}", expected predicateInstance | strInteger.filter(viper.silver.parser.FastParser$$$Lambda$1326/408618700@133d64fa) | booltrue | boolfalse | nul | old | result | unExp | "(" ~ exp ~ ")" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | applying | collectionTypedEmpty | explicitSetNonEmpty | collectionTypedEmpty | explicitMultisetNonEmpty | collectionTypedEmpty | seqLength | explicitSeqNonEmpty | seqRange | fapp | typedFapp | idnuse | Fail at index 32
    assert perm(expr) < write
           ^ ([email protected])

By the way, "Expected found" looks like a bug in the construction of error messages.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions