formula: hide throw statements from inline methods
* spot/tl/formula.hh: Move all throw statements behind some [[noreturn]] report...() methods... * spot/tl/formula.cc: ... defined here. This makes the methods shorter and helps their inlining. Incidentally, this also removes the uninitialized read that weirdly occurs when _GLIBCXX_DEBUG is on, as observed with #184, but I do not know why.
This commit is contained in:
parent
6b96aa4f27
commit
ab42075dce
2 changed files with 64 additions and 17 deletions
|
|
@ -1,5 +1,5 @@
|
||||||
// -*- coding: utf-8 -*-
|
// -*- coding: utf-8 -*-
|
||||||
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
|
// Copyright (C) 2015, 2016, 2017 Laboratoire de Recherche et Développement de
|
||||||
// l'Epita (LRDE).
|
// l'Epita (LRDE).
|
||||||
//
|
//
|
||||||
// This file is part of Spot, a model checking library.
|
// This file is part of Spot, a model checking library.
|
||||||
|
|
@ -161,6 +161,46 @@ namespace spot
|
||||||
delete this;
|
delete this;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
fnode::report_non_existing_child()
|
||||||
|
{
|
||||||
|
throw std::runtime_error("access to non-existing child");
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
fnode::report_too_many_children()
|
||||||
|
{
|
||||||
|
throw std::runtime_error("too many children for formula");
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
fnode::report_get_child_of_expecting_single_child_node()
|
||||||
|
{
|
||||||
|
throw std::invalid_argument
|
||||||
|
("get_child_of() expecting single-child node");
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
fnode::report_min_invalid_arg()
|
||||||
|
{
|
||||||
|
throw std::invalid_argument
|
||||||
|
("min() only works on Star and FStar nodes");
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
fnode::report_max_invalid_arg()
|
||||||
|
{
|
||||||
|
throw std::invalid_argument
|
||||||
|
("min() only works on Star and FStar nodes");
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
formula::report_ap_invalid_arg()
|
||||||
|
{
|
||||||
|
throw std::invalid_argument("atomic propositions cannot be "
|
||||||
|
"constructed from arbitrary formulas");
|
||||||
|
}
|
||||||
|
|
||||||
std::string fnode::kindstr() const
|
std::string fnode::kindstr() const
|
||||||
{
|
{
|
||||||
switch (op_)
|
switch (op_)
|
||||||
|
|
|
||||||
|
|
@ -192,8 +192,7 @@ namespace spot
|
||||||
if (op_ != o)
|
if (op_ != o)
|
||||||
return nullptr;
|
return nullptr;
|
||||||
if (SPOT_UNLIKELY(size_ != 1))
|
if (SPOT_UNLIKELY(size_ != 1))
|
||||||
throw std::invalid_argument
|
report_get_child_of_expecting_single_child_node();
|
||||||
("get_child_of() expecting single-child node");
|
|
||||||
return nth(0);
|
return nth(0);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -214,8 +213,7 @@ namespace spot
|
||||||
unsigned min() const
|
unsigned min() const
|
||||||
{
|
{
|
||||||
if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
|
if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
|
||||||
throw std::invalid_argument
|
report_min_invalid_arg();
|
||||||
("min() only works on Star and FStar nodes");
|
|
||||||
return min_;
|
return min_;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -223,8 +221,7 @@ namespace spot
|
||||||
unsigned max() const
|
unsigned max() const
|
||||||
{
|
{
|
||||||
if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
|
if (SPOT_UNLIKELY(op_ != op::FStar && op_ != op::Star))
|
||||||
throw std::invalid_argument
|
report_max_invalid_arg();
|
||||||
("max() only works on Star and FStar nodes");
|
|
||||||
return max_;
|
return max_;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -255,8 +252,8 @@ namespace spot
|
||||||
/// \see formula::nth
|
/// \see formula::nth
|
||||||
const fnode* nth(unsigned i) const
|
const fnode* nth(unsigned i) const
|
||||||
{
|
{
|
||||||
if (i >= size())
|
if (SPOT_UNLIKELY(i >= size()))
|
||||||
throw std::runtime_error("access to non-existing child");
|
report_non_existing_child();
|
||||||
return children[i];
|
return children[i];
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -480,6 +477,13 @@ namespace spot
|
||||||
void setup_props(op o);
|
void setup_props(op o);
|
||||||
void destroy_aux() const;
|
void destroy_aux() const;
|
||||||
|
|
||||||
|
[[noreturn]] static void report_non_existing_child();
|
||||||
|
[[noreturn]] static void report_too_many_children();
|
||||||
|
[[noreturn]] static void
|
||||||
|
report_get_child_of_expecting_single_child_node();
|
||||||
|
[[noreturn]] static void report_min_invalid_arg();
|
||||||
|
[[noreturn]] static void report_max_invalid_arg();
|
||||||
|
|
||||||
static const fnode* unique(const fnode*);
|
static const fnode* unique(const fnode*);
|
||||||
|
|
||||||
// Destruction may only happen via destroy().
|
// Destruction may only happen via destroy().
|
||||||
|
|
@ -509,8 +513,8 @@ namespace spot
|
||||||
saturated_(0)
|
saturated_(0)
|
||||||
{
|
{
|
||||||
size_t s = std::distance(begin, end);
|
size_t s = std::distance(begin, end);
|
||||||
if (s > (size_t) UINT16_MAX)
|
if (SPOT_UNLIKELY(s > (size_t) UINT16_MAX))
|
||||||
throw std::runtime_error("too many children for formula");
|
report_too_many_children();
|
||||||
size_ = s;
|
size_ = s;
|
||||||
auto pos = children;
|
auto pos = children;
|
||||||
for (auto i = begin; i != end; ++i)
|
for (auto i = begin; i != end; ++i)
|
||||||
|
|
@ -825,11 +829,9 @@ namespace spot
|
||||||
/// atomic propositions.
|
/// atomic propositions.
|
||||||
static formula ap(const formula& a)
|
static formula ap(const formula& a)
|
||||||
{
|
{
|
||||||
if (a.kind() == op::ap)
|
if (SPOT_UNLIKELY(a.kind() != op::ap))
|
||||||
return a;
|
report_ap_invalid_arg();
|
||||||
else
|
return a;
|
||||||
throw std::invalid_argument("atomic propositions cannot be "
|
|
||||||
"constructed from arbitrary formulas");
|
|
||||||
}
|
}
|
||||||
|
|
||||||
/// \brief Build a unary operator.
|
/// \brief Build a unary operator.
|
||||||
|
|
@ -1293,7 +1295,7 @@ namespace spot
|
||||||
class SPOT_API formula_child_iterator final
|
class SPOT_API formula_child_iterator final
|
||||||
{
|
{
|
||||||
const fnode*const* ptr_;
|
const fnode*const* ptr_;
|
||||||
public:
|
public:
|
||||||
formula_child_iterator()
|
formula_child_iterator()
|
||||||
: ptr_(nullptr)
|
: ptr_(nullptr)
|
||||||
{
|
{
|
||||||
|
|
@ -1651,6 +1653,11 @@ namespace spot
|
||||||
for (auto f: *this)
|
for (auto f: *this)
|
||||||
f.traverse(func);
|
f.traverse(func);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
private:
|
||||||
|
#ifndef SWIG
|
||||||
|
[[noreturn]] static void report_ap_invalid_arg();
|
||||||
|
#endif
|
||||||
};
|
};
|
||||||
|
|
||||||
/// Print the properties of formula \a f on stream \a out.
|
/// Print the properties of formula \a f on stream \a out.
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue