From 42a94c4dbe1d73db2d5177db5f6c2d782fcb5afa Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 15 Nov 2017 14:38:07 +0100 Subject: [PATCH] bin: add support for SPOT_OOM_ABORT * bin/common_setup.cc: Here. * NEWS, bin/man/spot-x.x: Document it. --- NEWS | 4 ++++ bin/common_setup.cc | 11 +++++++++++ bin/man/spot-x.x | 13 +++++++++++++ 3 files changed, 28 insertions(+) diff --git a/NEWS b/NEWS index 946055794..4f537fd58 100644 --- a/NEWS +++ b/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 "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: - Rename three methods of spot::scc_info. New names are clearer. The diff --git a/bin/common_setup.cc b/bin/common_setup.cc index 4d7c518e8..faed4ed8a 100644 --- a/bin/common_setup.cc +++ b/bin/common_setup.cc @@ -79,6 +79,14 @@ static void setup_sig_handler() # define setup_sig_handler() while (0); #endif + +static void bad_alloc_handler() +{ + std::set_new_handler(nullptr); + std::cerr << "not enough memory\n"; + abort(); +} + void setup(char** argv) { @@ -91,6 +99,9 @@ setup(char** argv) argp_err_exit_status = 2; + if (getenv("SPOT_OOM_ABORT")) + std::set_new_handler(bad_alloc_handler); + std::ios_base::sync_with_stdio(false); // 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 diff --git a/bin/man/spot-x.x b/bin/man/spot-x.x index c86b44376..9f374815b 100644 --- a/bin/man/spot-x.x +++ b/bin/man/spot-x.x @@ -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 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 \fBSPOT_PR_CHECK\fR Select the default algorithm that must be used to check the persistence