src/kernel_internals/parsing/logic_lexer.mll · a6775b989b49098489b12d8eaa45b1be5028c42d · pub / frama-c

4 years ago

[lexer] tentative logic lexer hack for introducing generalized check · a6775b98

Just using `check` as a prefix to various keywords would lead to too many
ambiguities in the parser (notably in contracts, where you can have an empty
requires list followed by `check ensures ...` or a `check requires ...`. With
a lookahead of 1, it's difficult for the parser see which rule should apply.
Hence, the lexer will perform itself the lookahead and emit a proper token
(`CHECK_ENSURES` or `CHECK_REQUIRES` respectively).

a6775b98

History

[lexer] tentative logic lexer hack for introducing generalized check

Virgile Prevosto authored 4 years ago

Just using `check` as a prefix to various keywords would lead to too many
ambiguities in the parser (notably in contracts, where you can have an empty
requires list followed by `check ensures ...` or a `check requires ...`. With
a lookahead of 1, it's difficult for the parser see which rule should apply.
Hence, the lexer will perform itself the lookahead and emit a proper token
(`CHECK_ENSURES` or `CHECK_REQUIRES` respectively).