From 20cf43b3ea3bc1c430484ddb5d833594a9406dda Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sun, 24 Jul 2016 23:26:59 +0200 Subject: [PATCH] use SPOT_ASSERT instead of assert For #184. * spot/graph/graph.hh, spot/kripke/kripkegraph.hh, spot/misc/bitvect.hh, spot/misc/common.hh, spot/misc/fixpool.hh, spot/misc/mspool.hh, spot/misc/timer.hh, spot/tl/formula.hh, spot/twa/acc.hh, spot/twa/taatgba.hh, spot/twa/twa.hh, spot/twa/twagraph.hh, spot/twaalgos/emptiness_stats.hh, spot/twaalgos/mask.hh, spot/twaalgos/ndfs_result.hxx, spot/twaalgos/sccinfo.hh, spot/twaalgos/translate.hh: Replace assert() by SPOT_ASSERT(), or an exception, or nothing, depending on the case. * tests/sanity/style.test: Flag all asserts in headers. * HACKING: Discuss assertions. --- HACKING | 19 ++++++++++++- spot/graph/graph.hh | 26 ++++++----------- spot/kripke/kripkegraph.hh | 14 ++++++---- spot/misc/bitvect.hh | 32 ++++++++++----------- spot/misc/common.hh | 20 ++++++++++--- spot/misc/fixpool.hh | 6 ++-- spot/misc/mspool.hh | 6 ++-- spot/misc/timer.hh | 14 ++++++---- spot/tl/formula.hh | 16 +++++++---- spot/twa/acc.hh | 6 ++-- spot/twa/taatgba.hh | 6 ++-- spot/twa/twa.hh | 12 ++++---- spot/twa/twagraph.hh | 29 ++++++++++++------- spot/twaalgos/emptiness_stats.hh | 6 ++-- spot/twaalgos/mask.hh | 6 ++-- spot/twaalgos/ndfs_result.hxx | 48 ++++++++++++++++---------------- spot/twaalgos/sccinfo.hh | 8 ++---- spot/twaalgos/translate.hh | 4 +-- tests/sanity/style.test | 9 ++++-- 19 files changed, 163 insertions(+), 124 deletions(-) diff --git a/HACKING b/HACKING index 39ed1da3f..19f630f1d 100644 --- a/HACKING +++ b/HACKING @@ -346,6 +346,22 @@ Exporting symbols * Read http://www.akkadia.org/drepper/dsohowto.pdf for more information about how shared libraries work and why. +Assertions +---------- + + * There are different types of assertions. Plain assert() is OK for + invariants or post-conditions. When asserting a pre-condition, + carefully consider who the caller might be: if it can be in + user-code (either in C++ or Python), throw an exception + (std::runtime_error, std::invalid_argument, and spot::parse_error + are the three exception types catched by the Python bindings). + + * Do not call assert() in public *.hh files: even if the installed + libspot has been compiled with -DNDEBUG, the *.hh files will be + recompiled by users, probably without -DNDEBUG. So use + SPOT_ASSERT() instead of assert(), this ensure asserts are only + used inside libspot for debug builds. + Comments -------- @@ -361,7 +377,8 @@ Comments Formating --------- - * Braces are always on their own line. + * Braces around instruction blocks are always on their own line. + Braces around initializers lists need not be on their own. * Text within braces is two-space indented. diff --git a/spot/graph/graph.hh b/spot/graph/graph.hh index ba2ee41e2..9201316b4 100644 --- a/spot/graph/graph.hh +++ b/spot/graph/graph.hh @@ -373,7 +373,7 @@ namespace spot if (src_.succ_tail == this->t_) { src_.succ_tail = prev_; - assert(next == 0); + SPOT_ASSERT(next == 0); } // Erased edges have themselves as next_succ. @@ -678,14 +678,12 @@ namespace spot state_storage_t& state_storage(state s) { - assert(s < states_.size()); return states_[s]; } const state_storage_t& state_storage(state s) const { - assert(s < states_.size()); return states_[s]; } ///@} @@ -698,14 +696,12 @@ namespace spot typename state_storage_t::data_t& state_data(state s) { - assert(s < states_.size()); return states_[s].data(); } const typename state_storage_t::data_t& state_data(state s) const { - assert(s < states_.size()); return states_[s].data(); } ///@} @@ -718,14 +714,12 @@ namespace spot edge_storage_t& edge_storage(edge s) { - assert(s < edges_.size()); return edges_[s]; } const edge_storage_t& edge_storage(edge s) const { - assert(s < edges_.size()); return edges_[s]; } ///@} @@ -738,14 +732,12 @@ namespace spot typename edge_storage_t::data_t& edge_data(edge s) { - assert(s < edges_.size()); return edges_[s].data(); } const typename edge_storage_t::data_t& edge_data(edge s) const { - assert(s < edges_.size()); return edges_[s].data(); } ///@} @@ -759,13 +751,11 @@ namespace spot edge new_edge(state src, out_state dst, Args&&... args) { - assert(src < states_.size()); - edge t = edges_.size(); edges_.emplace_back(dst, 0, src, std::forward(args)...); edge st = states_[src].succ_tail; - assert(st < t || !st); + SPOT_ASSERT(st < t || !st); if (!st) states_[src].succ = t; else @@ -777,14 +767,14 @@ namespace spot /// Convert a storage reference into a state number state index_of_state(const state_storage_t& ss) const { - assert(!states_.empty()); + SPOT_ASSERT(!states_.empty()); return &ss - &states_.front(); } /// Conveart a storage reference into an edge number edge index_of_edge(const edge_storage_t& tt) const { - assert(!edges_.empty()); + SPOT_ASSERT(!edges_.empty()); return &tt - &edges_.front(); } @@ -1012,7 +1002,7 @@ namespace spot /// any iteration on the successor of a state is performed. void rename_states_(const std::vector& newst) { - assert(newst.size() == states_.size()); + SPOT_ASSERT(newst.size() == states_.size()); unsigned tend = edges_.size(); for (unsigned t = 1; t < tend; t++) { @@ -1028,8 +1018,8 @@ namespace spot /// \param used_states the number of states used (after renumbering) void defrag_states(std::vector&& newst, unsigned used_states) { - assert(newst.size() == states_.size()); - assert(used_states > 0); + SPOT_ASSERT(newst.size() == states_.size()); + SPOT_ASSERT(used_states > 0); //std::cerr << "\nbefore defrag\n"; //dump_storage(std::cerr); @@ -1080,7 +1070,7 @@ namespace spot tr.next_succ = newidx[tr.next_succ]; tr.dst = newst[tr.dst]; tr.src = newst[tr.src]; - assert(tr.dst != -1U); + SPOT_ASSERT(tr.dst != -1U); } // Adjust succ and succ_tails pointers in all states. diff --git a/spot/kripke/kripkegraph.hh b/spot/kripke/kripkegraph.hh index 1a6e8d976..8dd037faf 100644 --- a/spot/kripke/kripkegraph.hh +++ b/spot/kripke/kripkegraph.hh @@ -42,7 +42,7 @@ namespace spot virtual int compare(const spot::state* other) const override { auto o = down_cast(other); - assert(o); + SPOT_ASSERT(o); // Do not simply return "other - this", it might not fit in an int. if (o < this) @@ -129,7 +129,7 @@ namespace spot virtual kripke_graph_state* dst() const override { - assert(!done()); + SPOT_ASSERT(!done()); return const_cast (&g_->state_data(g_->edge_storage(p_).dst)); } @@ -169,7 +169,9 @@ namespace spot void set_init_state(graph_t::state s) { - assert(s < num_states()); + if (SPOT_UNLIKELY(s >= num_states())) + throw std::invalid_argument + ("set_init_state() called with nonexisiting state"); init_number_ = s; } @@ -193,8 +195,8 @@ namespace spot succ_iter(const spot::state* st) const override { auto s = down_cast(st); - assert(s); - assert(!s->succ || g_.is_valid_edge(s->succ)); + SPOT_ASSERT(s); + SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ)); if (this->iter_cache_) { @@ -212,7 +214,7 @@ namespace spot state_number(const state* st) const { auto s = down_cast(st); - assert(s); + SPOT_ASSERT(s); return s - &g_.state_storage(0); } diff --git a/spot/misc/bitvect.hh b/spot/misc/bitvect.hh index cdc4472d7..68ce81548 100644 --- a/spot/misc/bitvect.hh +++ b/spot/misc/bitvect.hh @@ -191,7 +191,7 @@ namespace spot bool get(size_t pos) const { - assert(pos < size_); + SPOT_ASSERT(pos < size_); const size_t bpb = 8 * sizeof(block_t); return storage_[pos / bpb] & (1UL << (pos % bpb)); } @@ -248,21 +248,21 @@ namespace spot void set(size_t pos) { - assert(pos < size_); + SPOT_ASSERT(pos < size_); const size_t bpb = 8 * sizeof(block_t); storage_[pos / bpb] |= 1UL << (pos % bpb); } void clear(size_t pos) { - assert(pos < size_); + SPOT_ASSERT(pos < size_); const size_t bpb = 8 * sizeof(block_t); storage_[pos / bpb] &= ~(1UL << (pos % bpb)); } void flip(size_t pos) { - assert(pos < size_); + SPOT_ASSERT(pos < size_); const size_t bpb = 8 * sizeof(block_t); storage_[pos / bpb] ^= (1UL << (pos % bpb)); } @@ -270,7 +270,7 @@ namespace spot bitvect& operator|=(const bitvect& other) { - assert(other.size_ <= size_); + SPOT_ASSERT(other.size_ <= size_); unsigned m = std::min(other.block_count_, block_count_); for (size_t i = 0; i < m; ++i) storage_[i] |= other.storage_[i]; @@ -279,7 +279,7 @@ namespace spot bitvect& operator&=(const bitvect& other) { - assert(other.size_ <= size_); + SPOT_ASSERT(other.size_ <= size_); unsigned m = std::min(other.block_count_, block_count_); for (size_t i = 0; i < m; ++i) storage_[i] &= other.storage_[i]; @@ -288,7 +288,7 @@ namespace spot bitvect& operator^=(const bitvect& other) { - assert(other.size_ <= size_); + SPOT_ASSERT(other.size_ <= size_); unsigned m = std::min(other.block_count_, block_count_); for (size_t i = 0; i < m; ++i) storage_[i] ^= other.storage_[i]; @@ -297,7 +297,7 @@ namespace spot bitvect& operator-=(const bitvect& other) { - assert(other.block_count_ <= block_count_); + SPOT_ASSERT(other.block_count_ <= block_count_); for (size_t i = 0; i < other.block_count_; ++i) storage_[i] &= ~other.storage_[i]; return *this; @@ -305,7 +305,7 @@ namespace spot bool is_subset_of(const bitvect& other) const { - assert(other.block_count_ >= block_count_); + SPOT_ASSERT(other.block_count_ >= block_count_); size_t i; const size_t bpb = 8 * sizeof(bitvect::block_t); @@ -391,8 +391,8 @@ namespace spot // to \a end (excluded). bitvect* extract_range(size_t begin, size_t end) { - assert(begin <= end); - assert(end <= size()); + SPOT_ASSERT(begin <= end); + SPOT_ASSERT(end <= size()); size_t count = end - begin; bitvect* res = make_bitvect(count); res->make_empty(); @@ -423,13 +423,13 @@ namespace spot ++indexb; res->push_back(storage_[indexb], bpb); count -= bpb; - assert(indexb != indexe || count == 0); + SPOT_ASSERT(indexb != indexe || count == 0); } if (count > 0) { ++indexb; - assert(indexb == indexe); - assert(count == end % bpb); + SPOT_ASSERT(indexb == indexe); + SPOT_ASSERT(count == end % bpb); res->push_back(storage_[indexb], count); } } @@ -495,7 +495,7 @@ namespace spot /// Return the bit-vector at \a index. bitvect& at(const size_t index) { - assert(index < size_); + SPOT_ASSERT(index < size_); return *reinterpret_cast(storage() + index * bvsize_); } @@ -510,7 +510,7 @@ namespace spot /// Return the bit-vector at \a index. const bitvect& at(const size_t index) const { - assert(index < size_); + SPOT_ASSERT(index < size_); return *reinterpret_cast(storage() + index * bvsize_); } diff --git a/spot/misc/common.hh b/spot/misc/common.hh index 369ecdea4..83d5c4a31 100644 --- a/spot/misc/common.hh +++ b/spot/misc/common.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -58,6 +58,18 @@ #define SPOT_DLL #endif + +// We should not call assert() in headers. For the rare cases where +// we do really want to call assert(), use spot_assert__ instead. +// Else use SPOT_ASSERT so the assert() are removed from user's +// builds. +#define spot_assert__ assert +#if defined(SPOT_BUILD) or defined(SPOT_DEBUG) + #define SPOT_ASSERT(x) spot_assert__(x) +#else + #define SPOT_ASSERT(x) while (0) +#endif + // SPOT_API is used for the public API symbols. It either DLL imports // or DLL exports (or does nothing for static build) SPOT_LOCAL is // used for non-api symbols that may occur in header files. @@ -93,9 +105,9 @@ // 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(); \ +#define SPOT_UNREACHABLE() do { \ + SPOT_ASSERT(!("unreachable code reached")); \ + SPOT_UNREACHABLE_BUILTIN(); \ } while (0) #define SPOT_UNIMPLEMENTED() throw std::runtime_error("unimplemented"); diff --git a/spot/misc/fixpool.hh b/spot/misc/fixpool.hh index 9c1fbd288..0779d7171 100644 --- a/spot/misc/fixpool.hh +++ b/spot/misc/fixpool.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2015 Laboratoire de Recherche et Développement -// de l'Epita (LRDE) +// Copyright (C) 2011, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -95,7 +95,7 @@ namespace spot void deallocate (const void* ptr) { - assert(ptr); + SPOT_ASSERT(ptr); block_* b = reinterpret_cast(const_cast(ptr)); b->next = freelist_; freelist_ = b; diff --git a/spot/misc/mspool.hh b/spot/misc/mspool.hh index 8df955b3d..600ed84e4 100644 --- a/spot/misc/mspool.hh +++ b/spot/misc/mspool.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2015 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE) +// Copyright (C) 2011, 2013, 2015, 2016 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -107,7 +107,7 @@ namespace spot void deallocate (const void* ptr, size_t size) { - assert(ptr); + SPOT_ASSERT(ptr); size = fixsize(size); block_* b = reinterpret_cast(const_cast(ptr)); block_*& f = freelist_[size]; diff --git a/spot/misc/timer.hh b/spot/misc/timer.hh index f7c47bc5a..4d512fe26 100644 --- a/spot/misc/timer.hh +++ b/spot/misc/timer.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015 Laboratoire de +// Copyright (C) 2009, 2011, 2012, 2013, 2014, 2015, 2016 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 @@ -91,7 +91,7 @@ namespace spot void start() { - assert(!running); + SPOT_ASSERT(!running); running = true; #ifdef SPOT_HAVE_TIMES struct tms tmp; @@ -115,7 +115,7 @@ namespace spot #else total_.utime += clock() - start_.utime; #endif - assert(running); + SPOT_ASSERT(running); running = false; } @@ -194,8 +194,9 @@ namespace spot cancel(const std::string& name) { tm_type::iterator i = tm.find(name); - assert(i != tm.end()); - assert(0 < i->second.second); + if (SPOT_UNLIKELY(i == tm.end())) + throw std::invalid_argument("timer_map::cancel(): unknown name"); + SPOT_ASSERT(0 < i->second.second); if (0 == --i->second.second) tm.erase(i); } @@ -205,7 +206,8 @@ namespace spot timer(const std::string& name) const { tm_type::const_iterator i = tm.find(name); - assert(i != tm.end()); + if (SPOT_UNLIKELY(i == tm.end())) + throw std::invalid_argument("timer_map::timer(): unknown name"); return i->second.first; } diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index bc0b965b5..f96f45237 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -191,7 +191,9 @@ namespace spot { if (op_ != o) return nullptr; - assert(size_ == 1); + if (SPOT_UNLIKELY(size_ != 1)) + throw std::invalid_argument + ("get_child_of() expecting single-child node"); return nth(0); } @@ -211,14 +213,18 @@ namespace spot /// \see formula::min unsigned min() const { - assert(op_ == op::FStar || op_ == op::Star); + if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star)) + throw std::invalid_argument + ("min() only works on Star and FStar nodes"); return min_; } /// \see formula::max unsigned max() const { - assert(op_ == op::FStar || op_ == op::Star); + if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star)) + throw std::invalid_argument + ("max() only works on Star and FStar nodes"); return max_; } @@ -580,8 +586,8 @@ namespace spot bool operator()(const fnode* left, const fnode* right) const { - assert(left); - assert(right); + SPOT_ASSERT(left); + SPOT_ASSERT(right); if (left == right) return false; diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh index b18f167f4..842a8d7c7 100644 --- a/spot/twa/acc.hh +++ b/spot/twa/acc.hh @@ -58,13 +58,13 @@ namespace spot bool operator==(unsigned o) const { - assert(o == 0U); + SPOT_ASSERT(o == 0U); return id == o; } bool operator!=(unsigned o) const { - assert(o == 0U); + SPOT_ASSERT(o == 0U); return id != o; } @@ -1115,7 +1115,7 @@ namespace spot mark_t mark(unsigned u) const { - assert(u < num_sets()); + SPOT_ASSERT(u < num_sets()); return 1U << u; } diff --git a/spot/twa/taatgba.hh b/spot/twa/taatgba.hh index 46e67c5b1..d9e6d978b 100644 --- a/spot/twa/taatgba.hh +++ b/spot/twa/taatgba.hh @@ -209,7 +209,7 @@ namespace spot virtual std::string format_state(const spot::state* s) const override { const spot::set_state* se = down_cast(s); - assert(se); + SPOT_ASSERT(se); const state_set* ss = se->get_state(); return format_state_set(ss); } @@ -279,7 +279,7 @@ namespace spot if (ss->size() == 1) { i2 = state_name_map_.find(*i1); - assert(i2 != state_name_map_.end()); + SPOT_ASSERT(i2 != state_name_map_.end()); return "{" + label_to_string(i2->second) + "}"; } else @@ -288,7 +288,7 @@ namespace spot while (i1 != ss->end()) { i2 = state_name_map_.find(*i1++); - assert(i2 != state_name_map_.end()); + SPOT_ASSERT(i2 != state_name_map_.end()); res += label_to_string(i2->second); res += ","; } diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index cd73aa8ee..02a3f3a8e 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -129,7 +129,7 @@ namespace spot bool operator()(const state* left, const state* right) const { - assert(left); + SPOT_ASSERT(left); return left->compare(right) < 0; } }; @@ -152,7 +152,7 @@ namespace spot bool operator()(const state* left, const state* right) const { - assert(left); + SPOT_ASSERT(left); return 0 == left->compare(right); } }; @@ -176,7 +176,7 @@ namespace spot size_t operator()(const state* that) const { - assert(that); + SPOT_ASSERT(that); return that->hash(); } }; @@ -280,7 +280,7 @@ namespace spot operator()(shared_state left, shared_state right) const { - assert(left); + SPOT_ASSERT(left); return left->compare(right.get()) < 0; } }; @@ -308,7 +308,7 @@ namespace spot operator()(shared_state left, shared_state right) const { - assert(left); + SPOT_ASSERT(left); return 0 == left->compare(right.get()); } }; @@ -336,7 +336,7 @@ namespace spot size_t operator()(shared_state that) const { - assert(that); + SPOT_ASSERT(that); return that->hash(); } }; diff --git a/spot/twa/twagraph.hh b/spot/twa/twagraph.hh index 865a45ef6..1cf048f14 100644 --- a/spot/twa/twagraph.hh +++ b/spot/twa/twagraph.hh @@ -45,7 +45,7 @@ namespace spot virtual int compare(const spot::state* other) const override { auto o = down_cast(other); - assert(o); + SPOT_ASSERT(o); // Do not simply return "other - this", it might not fit in an int. if (o < this) @@ -145,19 +145,19 @@ namespace spot virtual const twa_graph_state* dst() const override { - assert(!done()); + SPOT_ASSERT(!done()); return &g_->state_data(g_->edge_storage(p_).dst); } virtual bdd cond() const override { - assert(!done()); + SPOT_ASSERT(!done()); return g_->edge_data(p_).cond; } virtual acc_cond::mark_t acc() const override { - assert(!done()); + SPOT_ASSERT(!done()); return g_->edge_data(p_).acc; } @@ -251,7 +251,9 @@ namespace spot void set_init_state(state_num s) { - assert(s < num_states()); + if (SPOT_UNLIKELY(s >= num_states())) + throw std::invalid_argument + ("set_init_state() called with nonexisiting state"); init_number_ = s; } @@ -278,8 +280,8 @@ namespace spot succ_iter(const state* st) const override { auto s = down_cast(st); - assert(s); - assert(!s->succ || g_.is_valid_edge(s->succ)); + SPOT_ASSERT(s); + SPOT_ASSERT(!s->succ || g_.is_valid_edge(s->succ)); if (this->iter_cache_) { @@ -296,7 +298,7 @@ namespace spot state_number(const state* st) const { auto s = down_cast(st); - assert(s); + SPOT_ASSERT(s); return s - &g_.state_storage(0); } @@ -451,7 +453,11 @@ namespace spot acc_cond::mark_t state_acc_sets(unsigned s) const { - assert((bool)prop_state_acc() || num_sets() == 0); + if (SPOT_UNLIKELY(!((bool)prop_state_acc() || num_sets() == 0))) + throw std::runtime_error + ("state_acc_sets() should only be called on " + "automata with state-based acceptance"); + for (auto& t: g_.out(s)) // Stop at the first edge, since the remaining should be // labeled identically. @@ -461,7 +467,10 @@ namespace spot bool state_is_accepting(unsigned s) const { - assert((bool)prop_state_acc() || num_sets() == 0); + if (SPOT_UNLIKELY(!((bool)prop_state_acc() || num_sets() == 0))) + throw std::runtime_error + ("state_is_accepting() should only be called on " + "automata with state-based acceptance"); for (auto& t: g_.out(s)) // Stop at the first edge, since the remaining should be // labeled identically. diff --git a/spot/twaalgos/emptiness_stats.hh b/spot/twaalgos/emptiness_stats.hh index dbc62b1e9..fb8feefc7 100644 --- a/spot/twaalgos/emptiness_stats.hh +++ b/spot/twaalgos/emptiness_stats.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université @@ -43,7 +43,7 @@ namespace spot get(const char* str) const { auto i = stats.find(str); - assert(i != stats.end()); + SPOT_ASSERT(i != stats.end()); return (this->*i->second)(); } @@ -163,7 +163,7 @@ namespace spot void dec_depth(unsigned n = 1) { - assert(depth_ >= n); + SPOT_ASSERT(depth_ >= n); depth_ -= n; } diff --git a/spot/twaalgos/mask.hh b/spot/twaalgos/mask.hh index 32557af9a..048a02152 100644 --- a/spot/twaalgos/mask.hh +++ b/spot/twaalgos/mask.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement +// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -66,7 +66,7 @@ namespace spot todo.pop_back(); unsigned new_src = seen[old_src]; - assert(new_src != -1U); + SPOT_ASSERT(new_src != -1U); for (auto& t: old->out(old_src)) { @@ -112,7 +112,7 @@ namespace spot trans(t.src, cond, acc, t.dst); // Having the same number of states should assure that state ids are // equivilent in old and cpy. - assert(t.src < cpy->num_states() && t.dst < cpy->num_states()); + SPOT_ASSERT(t.src < cpy->num_states() && t.dst < cpy->num_states()); if (cond != bddfalse) cpy->new_edge(t.src, t.dst, cond, acc); } diff --git a/spot/twaalgos/ndfs_result.hxx b/spot/twaalgos/ndfs_result.hxx index 707bedfcb..53c025f7c 100644 --- a/spot/twaalgos/ndfs_result.hxx +++ b/spot/twaalgos/ndfs_result.hxx @@ -109,7 +109,7 @@ namespace spot const stack_type& stb = ms_->get_st_blue(); const stack_type& str = ms_->get_st_red(); - assert(!stb.empty()); + SPOT_ASSERT(!stb.empty()); acc_cond::mark_t covered_acc = 0U; accepting_transitions_list acc_trans; @@ -128,8 +128,8 @@ namespace spot i = stb.begin(); transition t = { i->s->clone(), j->label, j->acc, j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); + SPOT_ASSERT(h_.has_been_visited(t.source)); + SPOT_ASSERT(h_.has_been_visited(t.dest)); acc_trans.push_back(t); } else @@ -148,8 +148,8 @@ namespace spot { transition t = { i->s->clone(), j->label, j->acc, j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); + SPOT_ASSERT(h_.has_been_visited(t.source)); + SPOT_ASSERT(h_.has_been_visited(t.dest)); acc_trans.push_back(t); covered_acc |= j->acc; } @@ -160,8 +160,8 @@ namespace spot { transition t = { i->s->clone(), j->label, j->acc, j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); + SPOT_ASSERT(h_.has_been_visited(t.source)); + SPOT_ASSERT(h_.has_been_visited(t.dest)); acc_trans.push_back(t); covered_acc |= j->acc; } @@ -174,8 +174,8 @@ namespace spot { transition t = { i->s->clone(), j->label, j->acc, j->s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); + SPOT_ASSERT(h_.has_been_visited(t.source)); + SPOT_ASSERT(h_.has_been_visited(t.dest)); acc_trans.push_back(t); covered_acc |= j->acc; } @@ -186,13 +186,13 @@ namespace spot if (!a_->acc().accepting(covered_acc)) { bool b = dfs(start, acc_trans, covered_acc); - assert(b); + SPOT_ASSERT(b); (void) b; } start->destroy(); - assert(!acc_trans.empty()); + SPOT_ASSERT(!acc_trans.empty()); auto run = std::make_shared(automaton()); // construct run->cycle from acc_trans. @@ -254,7 +254,7 @@ namespace spot bool dfs(const state* target, accepting_transitions_list& acc_trans, acc_cond::mark_t& covered_acc) { - assert(h_.has_been_visited(target)); + SPOT_ASSERT(h_.has_been_visited(target)); stack_type st1; state_set seen, dead; @@ -303,8 +303,8 @@ namespace spot { transition t = { f.s->clone(), label, acc, s_prime->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); + SPOT_ASSERT(h_.has_been_visited(t.source)); + SPOT_ASSERT(h_.has_been_visited(t.dest)); acc_trans.push_back(t); covered_acc |= acc; if (a_->acc().accepting(covered_acc)) @@ -345,8 +345,8 @@ namespace spot transition t = { st1.front().s->clone(), f_dest.label, f_dest.acc, f_dest.s->clone() }; - assert(h_.has_been_visited(t.source)); - assert(h_.has_been_visited(t.dest)); + SPOT_ASSERT(h_.has_been_visited(t.source)); + SPOT_ASSERT(h_.has_been_visited(t.dest)); acc_trans.push_back(t); covered_acc |= f_dest.acc; if (a_->acc().accepting(covered_acc)) @@ -446,7 +446,7 @@ namespace spot const state* res = s.search(start->clone(), path); if (res) { - assert(res->compare(target) == 0); + SPOT_ASSERT(res->compare(target) == 0); return true; } else @@ -531,7 +531,7 @@ namespace spot void construct_cycle(twa_run_ptr run, const accepting_transitions_list& acc_trans) { - assert(!acc_trans.empty()); + SPOT_ASSERT(!acc_trans.empty()); transition current = acc_trans.front(); // insert the first accepting transition in the cycle ndfsr_trace << "the initial accepting transition is from " @@ -579,10 +579,10 @@ namespace spot min_path s(this, a_, target, h_); const state* res = s.search(current.dest->clone(), run->cycle); // init current to the corresponding transition. - assert(res); + SPOT_ASSERT(res); ndfsr_trace << a_->format_state(res) << " reached" << std::endl; i = target.find(res); - assert(i != target.end()); + SPOT_ASSERT(i != target.end()); } else { @@ -611,8 +611,8 @@ namespace spot target.emplace(begin, tmp); min_path s(this, a_, target, h_); const state* res = s.search(current.dest->clone(), run->cycle); - assert(res); - assert(res->compare(begin) == 0); + SPOT_ASSERT(res); + SPOT_ASSERT(res->compare(begin) == 0); (void)res; } } @@ -648,7 +648,7 @@ namespace spot // This initial state is outside the cycle. Compute the prefix. min_path s(this, a_, target, h_); cycle_entry_point = s.search(prefix_start, run->prefix); - assert(cycle_entry_point); + SPOT_ASSERT(cycle_entry_point); cycle_entry_point = cycle_entry_point->clone(); } @@ -658,7 +658,7 @@ namespace spot cycle_ep_it != run->cycle.end() && cycle_entry_point->compare(cycle_ep_it->s); ++cycle_ep_it) continue; - assert(cycle_ep_it != run->cycle.end()); + SPOT_ASSERT(cycle_ep_it != run->cycle.end()); cycle_entry_point->destroy(); // Now shift the cycle so it starts on cycle_entry_point. diff --git a/spot/twaalgos/sccinfo.hh b/spot/twaalgos/sccinfo.hh index 991be62df..f75e29a47 100644 --- a/spot/twaalgos/sccinfo.hh +++ b/spot/twaalgos/sccinfo.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -108,7 +108,6 @@ namespace spot const scc_node& node(unsigned scc) const { - assert(scc < node_.size()); return node_[scc]; } @@ -132,7 +131,6 @@ namespace spot unsigned scc_of(unsigned st) const { - assert(st < sccof_.size()); return sccof_[st]; } @@ -162,7 +160,7 @@ namespace spot /// \brief Get number of the SCC containing the initial state. unsigned initial() const { - assert(scc_count() - 1 == scc_of(aut_->get_init_state_number())); + SPOT_ASSERT(scc_count() - 1 == scc_of(aut_->get_init_state_number())); return scc_count() - 1; } diff --git a/spot/twaalgos/translate.hh b/spot/twaalgos/translate.hh index 29143e2d1..9672ad6c0 100644 --- a/spot/twaalgos/translate.hh +++ b/spot/twaalgos/translate.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -50,7 +50,7 @@ namespace spot translator(tl_simplifier* simpl, const option_map* opt = nullptr) : postprocessor(opt), simpl_(simpl), simpl_owned_(nullptr) { - assert(simpl); + SPOT_ASSERT(simpl); setup_opt(opt); } diff --git a/tests/sanity/style.test b/tests/sanity/style.test index 93d0bc5fb..3287929ed 100755 --- a/tests/sanity/style.test +++ b/tests/sanity/style.test @@ -300,8 +300,11 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do */priv/*|*/bin/*);; *) $GREP '#.*include.*priv/' $tmp && - diag 'Do not include private headers in public headers.' + diag 'Do not include private headers in public headers.' + $GREP -v '#' $tmp | $GREP 'assert[ ]*(.*)' && + diag 'Use SPOT_ASSERT() instead of assert() in public headers.' ;; + esac ;; *.cc) @@ -312,8 +315,8 @@ for dir in "$TOP/spot" "$TOP/bin" "$TOP/tests"; do $GREP '^[ ]*class[ ]' $tmp && diag 'Private definitions must be in anonymous namespace.' fi - e$GREP ' ' $tmp && - diag 'Use spaces instead of tabular.' + e$GREP ' ' $tmp && + diag 'Use spaces instead of tabs.' ;; esac case $file in