diff --git a/src/hoaparse/hoaparse.yy b/src/hoaparse/hoaparse.yy index 63c60a475..b50c13033 100644 --- a/src/hoaparse/hoaparse.yy +++ b/src/hoaparse/hoaparse.yy @@ -428,7 +428,7 @@ header-item: "States:" INT } res.states = std::max(res.states, (int) $2); } - | "Start:" state-conj-2 + | "Start:" init-state-conj-2 { error(@2, "alternation is not yet supported"); YYABORT; @@ -587,6 +587,11 @@ header-spec: | header-spec BOOLEAN state-conj-2: checked-state-num '&' checked-state-num | state-conj-2 '&' checked-state-num + // Currently we do not check the number of these states + // since we do not support alternation. +init-state-conj-2: state-num '&' state-num + | init-state-conj-2 '&' state-num + label-expr: 't' { $$ = bddtrue.id(); diff --git a/src/tests/hoaparse.test b/src/tests/hoaparse.test index e5454b9ad..9bfe868ea 100755 --- a/src/tests/hoaparse.test +++ b/src/tests/hoaparse.test @@ -1672,3 +1672,62 @@ input:13.9: state 2 has no definition input:17.7: state 5 has no definition input:14.9: state 8 has no definition EOF + + +# This input caused a segfault at some point. +# Not supporting alternation is not an excuse for segfaulting. +cat >input <