Commit 7f996d1b authored by Etienne Renault's avatar Etienne Renault
Browse files

Use SPOT_ASSERT() instead of assert() in public headers

* spot/mc/ec.hh, spot/mc/intersect.hh,
spot/mc/reachability.hh, spot/mc/utils.hh: here.
parent e5eb397e
......@@ -124,7 +124,7 @@ namespace spot
std::string trace()
{
assert(counterexample_found());
SPOT_ASSERT(counterexample_found());
std::string res = "Prefix:\n";
// Compute the prefix of the accepting run
......
......@@ -62,7 +62,7 @@ namespace spot
twacube_ptr twa):
sys_(sys), twa_(twa)
{
assert(is_a_kripkecube(sys));
SPOT_ASSERT(is_a_kripkecube(sys));
map.reserve(2000000);
todo.reserve(100000);
}
......@@ -178,8 +178,9 @@ namespace spot
/// is slightly different.
void forward_iterators(bool just_pushed)
{
assert(!todo.empty());
assert(!(todo.back().it_prop->done() && todo.back().it_kripke->done()));
SPOT_ASSERT(!todo.empty());
SPOT_ASSERT(!(todo.back().it_prop->done() &&
todo.back().it_kripke->done()));
// Sometimes kripke state may have no successors.
if (todo.back().it_kripke->done())
......@@ -187,7 +188,7 @@ namespace spot
// The state has just been push and the 2 iterators intersect.
// There is no need to move iterators forward.
assert(!(todo.back().it_prop->done()));
SPOT_ASSERT(!(todo.back().it_prop->done()));
if (just_pushed && twa_->get_cubeset()
.intersect(twa_->trans_data(todo.back().it_prop).cube_,
todo.back().it_kripke->condition()))
......
......@@ -35,7 +35,7 @@ namespace spot
seq_reach_kripke(kripkecube<State, SuccIterator>& sys):
sys_(sys)
{
assert(is_a_kripkecube(sys));
SPOT_ASSERT(is_a_kripkecube(sys));
visited.reserve(2000000);
todo.reserve(100000);
}
......
......@@ -67,7 +67,7 @@ namespace spot
{
unsigned st = res_->new_state();
names_->push_back(this->sys_.to_string(s));
assert(st == i);
SPOT_ASSERT(st == i);
}
void edge(unsigned src, unsigned dst)
......@@ -167,7 +167,7 @@ namespace spot
unsigned st = res_->new_state();
names_->push_back(this->sys_.to_string(s.st_kripke) +
('*' + std::to_string(s.st_prop)));
assert(st+1 == i);
SPOT_ASSERT(st+1 == i);
return true;
}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment