bin: add support for SPOT_OOM_ABORT
* bin/common_setup.cc: Here. * NEWS, bin/man/spot-x.x: Document it.
This commit is contained in:
parent
b20687630b
commit
42a94c4dbe
3 changed files with 28 additions and 0 deletions
4
NEWS
4
NEWS
|
|
@ -65,6 +65,10 @@ New in spot 2.4.2.dev (not yet released)
|
||||||
by their acceptance name (Buchi, co-Buchi, Streett, etc.) or
|
by their acceptance name (Buchi, co-Buchi, Streett, etc.) or
|
||||||
"other" if no name is known for the acceptance condition.
|
"other" if no name is known for the acceptance condition.
|
||||||
|
|
||||||
|
- All tools learned to check the SPOT_OOM_ABORT environment
|
||||||
|
variable. This is only useful for debuging out-of-memory
|
||||||
|
conditions; see the spot-x(7) man page for detail.
|
||||||
|
|
||||||
Library:
|
Library:
|
||||||
|
|
||||||
- Rename three methods of spot::scc_info. New names are clearer. The
|
- Rename three methods of spot::scc_info. New names are clearer. The
|
||||||
|
|
|
||||||
|
|
@ -79,6 +79,14 @@ static void setup_sig_handler()
|
||||||
# define setup_sig_handler() while (0);
|
# define setup_sig_handler() while (0);
|
||||||
#endif
|
#endif
|
||||||
|
|
||||||
|
|
||||||
|
static void bad_alloc_handler()
|
||||||
|
{
|
||||||
|
std::set_new_handler(nullptr);
|
||||||
|
std::cerr << "not enough memory\n";
|
||||||
|
abort();
|
||||||
|
}
|
||||||
|
|
||||||
void
|
void
|
||||||
setup(char** argv)
|
setup(char** argv)
|
||||||
{
|
{
|
||||||
|
|
@ -91,6 +99,9 @@ setup(char** argv)
|
||||||
|
|
||||||
argp_err_exit_status = 2;
|
argp_err_exit_status = 2;
|
||||||
|
|
||||||
|
if (getenv("SPOT_OOM_ABORT"))
|
||||||
|
std::set_new_handler(bad_alloc_handler);
|
||||||
|
|
||||||
std::ios_base::sync_with_stdio(false);
|
std::ios_base::sync_with_stdio(false);
|
||||||
// Do not flush std::cout every time we read from std::cin, unless
|
// Do not flush std::cout every time we read from std::cin, unless
|
||||||
// we are reading from a terminal. Note that we do flush regularly
|
// we are reading from a terminal. Note that we do flush regularly
|
||||||
|
|
|
||||||
|
|
@ -99,6 +99,19 @@ in third-party tools that output incorrect HOA (e.g., declaring
|
||||||
the automaton with property "univ-branch" when no universal branching
|
the automaton with property "univ-branch" when no universal branching
|
||||||
is actually used)
|
is actually used)
|
||||||
|
|
||||||
|
.TP
|
||||||
|
\fBSPOT_OOM_ABORT\fR
|
||||||
|
If this variable is set, Out-Of-Memory errors will \f(CWabort()\fR the
|
||||||
|
program (potentially generating a coredump) instead of raising an
|
||||||
|
exception. This is useful to debug a program and to obtain a stack
|
||||||
|
trace pointing to the function doing the allocation. When this
|
||||||
|
variable is unset (the default), \f(CWstd::bad_alloc\fR are thrown on
|
||||||
|
memory allocation failures, and the stack is usually unwinded up to
|
||||||
|
top-level, losing the original context of the error. Note that at
|
||||||
|
least \f(CWltlcross\fR has some custom handling of
|
||||||
|
\f(CWstd::bad_alloc\fR to recover from products that are too large (by
|
||||||
|
ignoring them), and setting this variable will interfer with that.
|
||||||
|
|
||||||
.TP
|
.TP
|
||||||
\fBSPOT_PR_CHECK\fR
|
\fBSPOT_PR_CHECK\fR
|
||||||
Select the default algorithm that must be used to check the persistence
|
Select the default algorithm that must be used to check the persistence
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue