Skip to content

Commit f1af469

Browse files
committed
Updated NGrammar.
1 parent ee06e0a commit f1af469

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed

library/shared/src/main/scala/org/sireum/parser/NGrammar.scala

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -338,6 +338,18 @@ object NGrammar {
338338
pt.predict(alts.num, lookahead(i)) match {
339339
case Some(n) => return parseRule(alts.alts(n), i)
340340
case _ =>
341+
// For synthetic choice rules (star/opt), if the last alt is an empty
342+
// synthetic rule, use it as a default stop/skip when prediction fails.
343+
// This handles cases where FOLLOW_k is incomplete (e.g., the start rule
344+
// has no FOLLOW, or the lookahead is shorter than k near end of input).
345+
if (alts.isSynthetic) {
346+
val lastAltNum = alts.alts(alts.alts.size - 1)
347+
ruleMap.get(lastAltNum).get match {
348+
case lastAlt: NRule.Elements if lastAlt.isSynthetic && lastAlt.elements.isEmpty =>
349+
return parseElements(lastAlt, i)
350+
case _ =>
351+
}
352+
}
341353
val expectedTokens: ISZ[String] = pt.rules.get(alts.num) match {
342354
case Some(n: PredictiveNode.Branch) =>
343355
val m = pt.reverseNameMap

0 commit comments

Comments
 (0)