diff --git a/src/bin/dstar2tgba.cc b/src/bin/dstar2tgba.cc index d2985a6c8..a3a9ed4dc 100644 --- a/src/bin/dstar2tgba.cc +++ b/src/bin/dstar2tgba.cc @@ -285,8 +285,7 @@ namespace int process_formula(const spot::ltl::formula*, const char*, int) { - assert(!"should not happen"); - return 0; + SPOT_UNREACHABLE(); } diff --git a/src/bin/ltlcross.cc b/src/bin/ltlcross.cc index 94aedcacd..33208dee7 100644 --- a/src/bin/ltlcross.cc +++ b/src/bin/ltlcross.cc @@ -715,7 +715,7 @@ namespace else if (*pos == 'D') format = Dstar; else - assert(!"BUG"); + SPOT_UNREACHABLE(); if (val_) { @@ -823,7 +823,7 @@ namespace return string_ltl_wring; if (!string_ltl_lbt.val().empty()) return string_ltl_lbt; - assert(!"None of the translators need the input formula?"); + SPOT_UNREACHABLE(); return string_ltl_spot; } @@ -997,7 +997,7 @@ namespace break; } case printable_result_filename::None: - assert(!"unreachable code"); + SPOT_UNREACHABLE(); } } diff --git a/src/dstarparse/dstar2tgba.cc b/src/dstarparse/dstar2tgba.cc index a82006802..321dbee21 100644 --- a/src/dstarparse/dstar2tgba.cc +++ b/src/dstarparse/dstar2tgba.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -30,7 +31,6 @@ namespace spot case spot::Streett: return nsa_to_tgba(daut); } - assert(!"unreachable code"); - return 0; + SPOT_UNREACHABLE(); } } diff --git a/src/eltlparse/eltlparse.yy b/src/eltlparse/eltlparse.yy index 5f8d2fdd1..3ebde0e33 100644 --- a/src/eltlparse/eltlparse.yy +++ b/src/eltlparse/eltlparse.yy @@ -138,10 +138,7 @@ namespace spot res->rhs = realias(a->rhs, v); return node_ptr(res); } - - /* Unreachable code. */ - assert(0); - return node_ptr(static_cast(0)); + SPOT_UNREACHABLE(); } } } diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index d4400b037..22da058ce 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -300,9 +300,7 @@ namespace spot case UConcat: return "UConcat"; } - // Unreachable code. - assert(0); - return 0; + SPOT_UNREACHABLE(); } binop::map binop::instances; diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index 6dfb01e4c..627d4c1de 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -107,9 +107,7 @@ namespace spot case Star: return "Star"; } - // Unreachable code. - assert(0); - return 0; + SPOT_UNREACHABLE(); } std::string diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 3ead65b9a..a74ee08a1 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -100,9 +100,7 @@ namespace spot case EmptyWord: return "constant(e)"; } - // Unreachable code. - assert(0); - return "BUG"; + SPOT_UNREACHABLE(); } void @@ -123,9 +121,7 @@ namespace spot case EmptyWord: return "[*0]"; } - // Unreachable code. - assert(0); - return 0; + SPOT_UNREACHABLE(); } } } diff --git a/src/ltlast/formula_tree.cc b/src/ltlast/formula_tree.cc index ce84f44f3..1920a9582 100644 --- a/src/ltlast/formula_tree.cc +++ b/src/ltlast/formula_tree.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et +// Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -53,10 +53,7 @@ namespace spot return multop::instance(n->op, instanciate(n->lhs, v), instanciate(n->rhs, v)); - - /* Unreachable code. */ - assert(0); - return 0; + SPOT_UNREACHABLE(); } size_t @@ -78,10 +75,7 @@ namespace spot return std::max(arity(n->lhs), arity(n->rhs)); if (node_multop* n = dynamic_cast(np.get())) return std::max(arity(n->lhs), arity(n->rhs)); - - /* Unreachable code. */ - assert(0); - return 0; + SPOT_UNREACHABLE(); } } } diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index c5fdcacf9..60a1f2aa1 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -185,9 +185,7 @@ namespace spot case Fusion: return "Fusion"; } - // Unreachable code. - assert(0); - return 0; + SPOT_UNREACHABLE(); } namespace diff --git a/src/ltlast/nfa.cc b/src/ltlast/nfa.cc index cbcda5d74..36eca99c4 100644 --- a/src/ltlast/nfa.cc +++ b/src/ltlast/nfa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2008, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -106,8 +106,7 @@ namespace spot const nfa::state* nfa::get_init_state() { - if (!init_) - assert(0); + assert(init_); return init_; } diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 3a91d7e5c..24632a7ac 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -189,9 +189,7 @@ namespace spot case NegClosureMarked: return "NegClosureMarked"; } - // Unreachable code. - assert(0); - return 0; + SPOT_UNREACHABLE(); } unop::map unop::instances; diff --git a/src/ltlvisit/dotty.cc b/src/ltlvisit/dotty.cc index b1172b9cb..4a2bb2c3e 100644 --- a/src/ltlvisit/dotty.cc +++ b/src/ltlvisit/dotty.cc @@ -95,7 +95,7 @@ namespace spot void visit(const automatop*) { - assert(0); + SPOT_UNIMPLEMENTED(); } void diff --git a/src/ltlvisit/lbt.cc b/src/ltlvisit/lbt.cc index 164c5a33a..012ae0422 100644 --- a/src/ltlvisit/lbt.cc +++ b/src/ltlvisit/lbt.cc @@ -94,7 +94,7 @@ namespace spot os_ << 't'; break; case constant::EmptyWord: - assert(!"unsupported constant"); + SPOT_UNIMPLEMENTED(); break; } } @@ -129,7 +129,7 @@ namespace spot case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); break; } bo->first()->accept(*this); @@ -139,7 +139,7 @@ namespace spot void visit(const bunop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -164,7 +164,7 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); break; } uo->child()->accept(*this); @@ -173,7 +173,7 @@ namespace spot void visit(const automatop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -193,7 +193,7 @@ namespace spot case multop::AndNLM: case multop::Concat: case multop::Fusion: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); break; } diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc index a426b8b53..0466e8860 100644 --- a/src/ltlvisit/lunabbrev.cc +++ b/src/ltlvisit/lunabbrev.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -93,8 +93,7 @@ namespace spot result_ = binop::instance(op, f1, f2); return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } const formula* diff --git a/src/ltlvisit/mark.cc b/src/ltlvisit/mark.cc index 9078375da..0fc2e3e7a 100644 --- a/src/ltlvisit/mark.cc +++ b/src/ltlvisit/mark.cc @@ -1,5 +1,6 @@ -// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2010, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -94,7 +95,7 @@ namespace spot case multop::AndRat: case multop::Concat: case multop::Fusion: - assert(!"unexpected operator"); + SPOT_UNIMPLEMENTED(); case multop::Or: for (unsigned i = 0; i < mos; ++i) res->push_back(recurse(mo->nth(i))); @@ -252,8 +253,7 @@ namespace spot uo->child()->clone()); return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -280,7 +280,7 @@ namespace spot case binop::Xor: case binop::Implies: case binop::Equiv: - assert(!"mark not defined on logic abbreviations"); + SPOT_UNIMPLEMENTED(); case binop::U: case binop::W: case binop::M: @@ -297,8 +297,7 @@ namespace spot return; } } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } const formula* diff --git a/src/ltlvisit/randomltl.cc b/src/ltlvisit/randomltl.cc index 51d5f43a2..b306aefe1 100644 --- a/src/ltlvisit/randomltl.cc +++ b/src/ltlvisit/randomltl.cc @@ -189,7 +189,7 @@ namespace spot else if (proba_[i].min_n > 2) total_2_and_more_ += proba_[i].proba; else - assert(!"unexpected max_n"); + SPOT_UNREACHABLE(); // unexpected max_n } assert(total_2_and_more_ >= total_2_); } diff --git a/src/ltlvisit/simpfg.cc b/src/ltlvisit/simpfg.cc index 6b9a94dc3..0afbbd39a 100644 --- a/src/ltlvisit/simpfg.cc +++ b/src/ltlvisit/simpfg.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2010, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -84,8 +84,7 @@ namespace spot result_ = binop::instance(binop::M, f1, f2); return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } const formula* diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 1bfce7c6b..ce50db590 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -185,7 +185,7 @@ namespace spot else if (f == constant::false_instance()) result = bddfalse; else - assert(!"Unsupported operator"); + SPOT_UNIMPLEMENTED(); break; case formula::AtomicProp: result = bdd_ithvar(dict->register_proposition(f, this)); @@ -213,7 +213,7 @@ namespace spot op = bddop_biimp; break; default: - assert(!"Unsupported operator"); + SPOT_UNIMPLEMENTED(); } result = bdd_apply(as_bdd(bo->first()), as_bdd(bo->second()), op); break; @@ -244,14 +244,14 @@ namespace spot case multop::OrRat: case multop::Concat: case multop::Fusion: - assert(!"Unsupported operator"); + SPOT_UNIMPLEMENTED(); break; } break; } case formula::BUnOp: case formula::AutomatOp: - assert(!"Unsupported operator"); + SPOT_UNIMPLEMENTED(); break; } @@ -490,9 +490,7 @@ namespace spot { case unop::Not: // "Not"s should be caught by nenoform_recursively(). - assert(!"Not should not occur"); - //result_ = recurse_(f, negated_ ^ true); - return; + SPOT_UNREACHABLE(); case unop::X: /* !Xa == X!a */ result_ = unop::instance(unop::X, recurse(f)); @@ -525,8 +523,7 @@ namespace spot result_ = unop::instance(unop::Not, result_); return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -630,8 +627,7 @@ namespace spot recurse_(f1, false), recurse(f2)); return; } - // Unreachable code. - assert(0); + SPOT_UNREACHABLE(); } void @@ -2182,7 +2178,7 @@ namespace spot case binop::Xor: case binop::Equiv: case binop::Implies: - assert(!"operator not supported for implication rules"); + SPOT_UNIMPLEMENTED(); return; case binop::UConcat: case binop::EConcat: diff --git a/src/ltlvisit/snf.cc b/src/ltlvisit/snf.cc index ab7619c72..43555e749 100644 --- a/src/ltlvisit/snf.cc +++ b/src/ltlvisit/snf.cc @@ -49,7 +49,7 @@ namespace spot void visit(const atomic_prop*) { - assert(!"unexpected operator"); + SPOT_UNIMPLEMENTED(); } void @@ -76,19 +76,19 @@ namespace spot void visit(const unop*) { - assert(!"unexpected operator"); + SPOT_UNIMPLEMENTED(); } void visit(const binop*) { - assert(!"unexpected operator"); + SPOT_UNIMPLEMENTED(); } void visit(const automatop*) { - assert(!"unexpected operator"); + SPOT_UNIMPLEMENTED(); } void @@ -100,7 +100,7 @@ namespace spot case multop::And: case multop::Or: case multop::Fusion: - assert(!"unexpected operator"); + SPOT_UNIMPLEMENTED(); break; case multop::Concat: case multop::AndNLM: diff --git a/src/ltlvisit/tostring.cc b/src/ltlvisit/tostring.cc index dc1223452..d17776a58 100644 --- a/src/ltlvisit/tostring.cc +++ b/src/ltlvisit/tostring.cc @@ -847,7 +847,7 @@ namespace spot break; case multop::Concat: // Handled by resugar_concat. - assert(0); + SPOT_UNREACHABLE(); break; case multop::Fusion: k = KFusion; diff --git a/src/misc/common.hh b/src/misc/common.hh index 5a8f22c52..4f8ceeaf3 100644 --- a/src/misc/common.hh +++ b/src/misc/common.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013 Laboratoire de Recherche et Développement +// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -17,6 +17,9 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . +#include +#include + #ifndef SPOT_MISC_COMMON_HH # define SPOT_MISC_COMMON_HH @@ -73,4 +76,23 @@ #define SPOT_DELETED = delete #endif + +// Do not use those in code, prefer SPOT_UNREACHABLE() instead. +#if defined __clang__ || defined __GNU__ +# define SPOT_UNREACHABLE_BUILTIN() __builtin_unreachable() +# elif defined _MSC_VER +# define SPOT_UNREACHABLE_BUILTIN() __assume(0) +# else +# define SPOT_UNREACHABLE_BUILTIN() abort() +#endif + +// The extra parentheses in assert() is so that this +// pattern is not caught by the style checker. +#define SPOT_UNREACHABLE() do { \ + assert(!("unreachable code reached")); \ + SPOT_UNREACHABLE_BUILTIN(); \ + } while (0) + +#define SPOT_UNIMPLEMENTED() throw std::runtime_error("unimplemented"); + #endif // SPOT_MISC_COMMON_HH diff --git a/src/misc/intvcomp.cc b/src/misc/intvcomp.cc index f6d42ece9..15af57dff 100644 --- a/src/misc/intvcomp.cc +++ b/src/misc/intvcomp.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -506,7 +506,7 @@ namespace spot self().push_data(get_32_bits()); break; default: - assert(0); + SPOT_UNREACHABLE(); } } } diff --git a/src/misc/minato.cc b/src/misc/minato.cc index f7094abd3..edff46a7e 100644 --- a/src/misc/minato.cc +++ b/src/misc/minato.cc @@ -157,8 +157,7 @@ namespace spot todo_.pop(); continue; } - // Unreachable code. - assert(0); + SPOT_UNREACHABLE(); } return bddfalse; } diff --git a/src/sanity/style.test b/src/sanity/style.test index dfa58e4d6..ac8ed1464 100755 --- a/src/sanity/style.test +++ b/src/sanity/style.test @@ -240,6 +240,9 @@ for dir in "${INCDIR-..}" "${INCDIR-..}"/../iface; do egrep '(->|[.])size\(\) [=!]= 0|![a-zA-Z0-9_]*(->|[.])size\(\)|(if |while |assert)\([a-zA-Z0-9_]*(->|[.])size\(\)\)' $tmp && diag 'Prefer empty() to check emptiness.' + egrep 'assert\((0|!".*")\)' $tmp && + diag 'Prefer SPOT_UNREACHABLE or SPOT_UNIMPLEMENTED.' + egrep '^[^=*<]*([+][+]|--);' $tmp && diag 'Take good habits: use ++i instead of i++ when you have the choice.' diff --git a/src/tgba/bdddict.cc b/src/tgba/bdddict.cc index af820e300..2510d8dc3 100644 --- a/src/tgba/bdddict.cc +++ b/src/tgba/bdddict.cc @@ -529,7 +529,7 @@ namespace spot std::cerr << "some maps are not empty" << std::endl; } dump(std::cerr); - assert(0); + abort(); } diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 47e3b9dda..b6a29e6aa 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -1,8 +1,9 @@ -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// -*- coding: utf-8 -*- +// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris -// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), -// Université Pierre et Marie Curie. +// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), +// Université Pierre et Marie Curie. // // This file is part of Spot, a model checking library. // @@ -62,17 +63,15 @@ namespace spot res_ = bddfalse; return; case constant::EmptyWord: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } virtual void visit(const bunop*) { - assert(!"unsupported operator"); - return; + SPOT_UNIMPLEMENTED(); } virtual void @@ -87,15 +86,14 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); case unop::Not: { res_ = bdd_not(recurse(node->child())); return; } } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } virtual void @@ -122,16 +120,15 @@ namespace spot case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } virtual void visit(const automatop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } virtual void @@ -153,7 +150,7 @@ namespace spot case multop::AndNLM: case multop::OrRat: case multop::AndRat: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgba/tgbasafracomplement.cc b/src/tgba/tgbasafracomplement.cc index a8d33be36..dc637c108 100644 --- a/src/tgba/tgbasafracomplement.cc +++ b/src/tgba/tgbasafracomplement.cc @@ -1169,26 +1169,26 @@ namespace spot safra_tree_automaton::automaton_t::const_iterator tr = a->automaton.find(const_cast(s->get_safra())); - if (tr != a->automaton.end()) - { - bdd condition = bddfalse; - tgba_safra_complement_succ_iterator::succ_list_t succ_list; - int nb_acceptance_pairs = a->get_nb_acceptance_pairs(); - bitvect* e = make_bitvect(nb_acceptance_pairs); + assert(tr != a->automaton.end()); - if (!s->get_use_bitset()) // if \delta'(q, a) + bdd condition = bddfalse; + tgba_safra_complement_succ_iterator::succ_list_t succ_list; + int nb_acceptance_pairs = a->get_nb_acceptance_pairs(); + bitvect* e = make_bitvect(nb_acceptance_pairs); + + if (!s->get_use_bitset()) // if \delta'(q, a) { for (auto& p: tr->second) - { - state_complement* s1 = new state_complement(e->clone(), e->clone(), - p.second, false); - state_complement* s2 = new state_complement(e->clone(), e->clone(), - p.second, true); - succ_list.insert(std::make_pair(p.first, s1)); - succ_list.insert(std::make_pair(p.first, s2)); - } + { + state_complement* s1 = new state_complement(e->clone(), e->clone(), + p.second, false); + state_complement* s2 = new state_complement(e->clone(), e->clone(), + p.second, true); + succ_list.insert(std::make_pair(p.first, s1)); + succ_list.insert(std::make_pair(p.first, s2)); + } } - else + else { bitvect* l = make_bitvect(nb_acceptance_pairs); bitvect* u = make_bitvect(nb_acceptance_pairs); @@ -1205,22 +1205,23 @@ namespace spot // \delta'((q, I, J), a) if I'\subseteq J' if (newI->is_subset_of(*newJ)) - { - for (auto& p: tr->second) - { - st = new state_complement(e->clone(), e->clone(), p.second, true); - succ_list.insert(std::make_pair(p.first, st)); - } - condition = the_acceptance_cond_; - } + { + for (auto& p: tr->second) + { + st = new state_complement(e->clone(), e->clone(), + p.second, true); + succ_list.insert(std::make_pair(p.first, st)); + } + condition = the_acceptance_cond_; + } else // \delta'((q, I, J), a) - { - for (auto& p: tr->second) - { - st = new state_complement(newI, newJ, p.second, true); - succ_list.insert(std::make_pair(p.first, st)); - } - } + { + for (auto& p: tr->second) + { + st = new state_complement(newI, newJ, p.second, true); + succ_list.insert(std::make_pair(p.first, st)); + } + } delete newI; delete newJ; #else @@ -1230,11 +1231,11 @@ namespace spot *pending |= *l; *pending -= *u; for (auto& p: tr->second) - { - st = new state_complement(pending->clone(), e->clone(), - p.second, true); - succ_list.insert(std::make_pair(p.first, st)); - } + { + st = new state_complement(pending->clone(), e->clone(), + p.second, true); + succ_list.insert(std::make_pair(p.first, st)); + } delete pending; for (unsigned i = 0; i < l->size(); ++i) @@ -1244,11 +1245,8 @@ namespace spot delete u; delete l; } - delete e; - return new tgba_safra_complement_succ_iterator(succ_list, condition); - } - assert(!"Safra automaton does not find this node"); - return 0; + delete e; + return new tgba_safra_complement_succ_iterator(succ_list, condition); } bdd_dict* diff --git a/src/tgbaalgos/eltl2tgba_lacim.cc b/src/tgbaalgos/eltl2tgba_lacim.cc index fb631ca2f..36a616d5a 100644 --- a/src/tgbaalgos/eltl2tgba_lacim.cc +++ b/src/tgbaalgos/eltl2tgba_lacim.cc @@ -71,10 +71,9 @@ namespace spot res_ = bddfalse; return; case constant::EmptyWord: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -103,16 +102,15 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void visit(const bunop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -139,10 +137,9 @@ namespace spot case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -170,7 +167,7 @@ namespace spot case multop::AndNLM: case multop::AndRat: case multop::OrRat: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgbaalgos/ltl2taa.cc b/src/tgbaalgos/ltl2taa.cc index a07eba63a..c67a24b1f 100644 --- a/src/tgbaalgos/ltl2taa.cc +++ b/src/tgbaalgos/ltl2taa.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -103,11 +103,9 @@ namespace spot case constant::False: return; case constant::EmptyWord: - assert(!"unsupported operator"); - return; + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -134,7 +132,7 @@ namespace spot } case unop::F: case unop::G: - assert(0); // TBD + SPOT_UNIMPLEMENTED(); // TBD return; case unop::Not: // Done in recurse @@ -144,17 +142,15 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - assert(!"unsupported operator"); - return; + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void visit(const bunop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -254,14 +250,12 @@ namespace spot case binop::Xor: case binop::Implies: case binop::Equiv: - assert(0); // TBD case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -335,18 +329,15 @@ namespace spot case multop::AndNLM: case multop::AndRat: case multop::OrRat: - assert(!"unsupported operator"); - return; + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void - visit(const automatop* node) + visit(const automatop*) { - (void) node; - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } ltl2taa_visitor diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 53d5136b1..b5848ef99 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -615,8 +615,7 @@ namespace spot res_ = now_to_concat(); return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -631,8 +630,7 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - assert(!"not a rational operator"); - return; + SPOT_UNREACHABLE(); // Because not rational operator case unop::Not: { // Not can only appear in front of Boolean @@ -644,8 +642,7 @@ namespace spot return; } } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -726,20 +723,19 @@ namespace spot } return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void visit(const binop*) { - assert(!"not a rational operator"); + SPOT_UNREACHABLE(); // Not a rational operator } void visit(const automatop*) { - assert(!"not a rational operator"); + SPOT_UNREACHABLE(); // Not a rational operator } void @@ -938,7 +934,7 @@ namespace spot } case multop::And: case multop::Or: - assert(!"not a rational operator"); + SPOT_UNREACHABLE(); // Not a rational operator } } @@ -1238,11 +1234,9 @@ namespace spot res_ = bddfalse; return; case constant::EmptyWord: - assert(!"Not an LTL operator"); - return; + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -1443,15 +1437,14 @@ namespace spot break; case unop::Finish: - assert(!"unsupported operator"); - break; + SPOT_UNIMPLEMENTED(); } } void visit(const bunop*) { - assert(!"Not an LTL operator"); + SPOT_UNREACHABLE(); // Not an LTL operator } void @@ -1468,8 +1461,7 @@ namespace spot // These operators should only appear in Boolean formulas, // which must have been dealt with earlier (in // translate_dict::ltl_to_bdd()). - assert(!"unexpected operator"); - break; + SPOT_UNREACHABLE(); case binop::U: { bdd f1 = recurse(node->first()); @@ -1651,7 +1643,7 @@ namespace spot void visit(const automatop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -1712,8 +1704,7 @@ namespace spot case multop::AndNLM: case multop::AndRat: case multop::OrRat: - assert(!"Not an LTL operator"); - break; + SPOT_UNREACHABLE(); // Not an LTL operator } } @@ -1839,20 +1830,19 @@ namespace spot // FIXME: we might need to add Acc[1] return; } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void visit(const automatop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void visit(const bunop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void diff --git a/src/tgbaalgos/ltl2tgba_lacim.cc b/src/tgbaalgos/ltl2tgba_lacim.cc index 17d8671a7..b4dda91b5 100644 --- a/src/tgbaalgos/ltl2tgba_lacim.cc +++ b/src/tgbaalgos/ltl2tgba_lacim.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Copyright (C) 2009, 2010, 2012, 2014 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -76,10 +76,9 @@ namespace spot res_ = bddfalse; return; case constant::EmptyWord: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void @@ -152,16 +151,15 @@ namespace spot case unop::Closure: case unop::NegClosure: case unop::NegClosureMarked: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void visit(const bunop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -230,17 +228,15 @@ namespace spot case binop::UConcat: case binop::EConcat: case binop::EConcatMarked: - assert(!"unsupported operator"); - break; + SPOT_UNIMPLEMENTED(); } - /* Unreachable code. */ - assert(0); + SPOT_UNREACHABLE(); } void visit(const automatop*) { - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } void @@ -268,7 +264,7 @@ namespace spot case multop::AndNLM: case multop::AndRat: case multop::OrRat: - assert(!"unsupported operator"); + SPOT_UNIMPLEMENTED(); } assert(op != -1); unsigned s = node->size(); diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index 577c56377..21aee1394 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -1026,7 +1026,7 @@ namespace spot } else - assert(0); + SPOT_UNREACHABLE(); } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index e23f3779c..a532adafe 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1901,7 +1901,7 @@ main(int argc, char** argv) } default: - assert(!"unknown output option"); + SPOT_UNREACHABLE(); } tm.stop("producing output"); }