diff --git a/NEWS b/NEWS index cb068bce8..74e1765b7 100644 --- a/NEWS +++ b/NEWS @@ -11,6 +11,12 @@ New in spot 2.5.1.dev (not yet released) update an external structure that references states of the twa that we want to purge. + Bugs fixed: + + - acc_cond::is_generalized_rabin() and + acc_cond::is_generalized_streett() would segfault on weird + acceptance conditions such as "3 t" or "3 f". + New in spot 2.5.1 (2018-02-20) Library: diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc index c6df13210..1b94f802e 100644 --- a/spot/twa/acc.cc +++ b/spot/twa/acc.cc @@ -660,7 +660,10 @@ namespace spot pairs.resize(num_); return true; } - if (code_.is_t() + // "Acceptance: 0 f" is caught by is_generalized_rabin() above. + // Therefore is_f() below catches "Acceptance: n f" with n>0. + if (code_.is_f() + || code_.is_t() || code_.back().sub.op != acc_op::Or) return false; @@ -741,7 +744,10 @@ namespace spot pairs.resize(num_); return true; } - if (code_.is_f() + // "Acceptance: 0 t" is caught by is_generalized_buchi() above. + // Therefore is_t() below catches "Acceptance: n t" with n>0. + if (code_.is_t() + || code_.is_f() || code_.back().sub.op != acc_op::And) return false;