diff --git a/src/search/utils/system.cc b/src/search/utils/system.cc index f2f54b6f46..001f68542a 100644 --- a/src/search/utils/system.cc +++ b/src/search/utils/system.cc @@ -49,11 +49,9 @@ void exit_with(ExitCode exitcode) { exit(static_cast(exitcode)); } -void exit_after_receiving_signal(ExitCode exitcode) { - /* - In signal handlers, we have to use the "safe function" _Exit() rather - than the unsafe function exit(). - */ +void exit_with_reentrant(ExitCode exitcode) { + /* In signal handlers or when we run out of memory, we have to use the + "safe function" _Exit() rather than the unsafe function exit(). */ report_exit_code_reentrant(exitcode); _Exit(static_cast(exitcode)); } diff --git a/src/search/utils/system.h b/src/search/utils/system.h index a5ec692aef..1f23ef19c7 100644 --- a/src/search/utils/system.h +++ b/src/search/utils/system.h @@ -54,7 +54,7 @@ enum class ExitCode { }; NO_RETURN extern void exit_with(ExitCode returncode); -NO_RETURN extern void exit_after_receiving_signal(ExitCode returncode); +NO_RETURN extern void exit_with_reentrant(ExitCode returncode); int get_peak_memory_in_kb(); const char *get_exit_code_message_reentrant(ExitCode exitcode); diff --git a/src/search/utils/system_unix.cc b/src/search/utils/system_unix.cc index 6752d08b62..9b4709c541 100644 --- a/src/search/utils/system_unix.cc +++ b/src/search/utils/system_unix.cc @@ -164,7 +164,7 @@ static void out_of_memory_handler() { memory for the stack of the signal handler and raising a signal here. */ write_reentrant_str(STDOUT_FILENO, "Failed to allocate memory.\n"); - exit_with(ExitCode::SEARCH_OUT_OF_MEMORY); + exit_with_reentrant(ExitCode::SEARCH_OUT_OF_MEMORY); } static void signal_handler(int signal_number) { @@ -173,7 +173,7 @@ static void signal_handler(int signal_number) { write_reentrant_int(STDOUT_FILENO, signal_number); write_reentrant_str(STDOUT_FILENO, " -- exiting\n"); if (signal_number == SIGXCPU) { - exit_after_receiving_signal(ExitCode::SEARCH_OUT_OF_TIME); + exit_with_reentrant(ExitCode::SEARCH_OUT_OF_TIME); } raise(signal_number); } diff --git a/src/search/utils/system_windows.cc b/src/search/utils/system_windows.cc index f8b4bc1e53..a244b68468 100644 --- a/src/search/utils/system_windows.cc +++ b/src/search/utils/system_windows.cc @@ -15,7 +15,7 @@ using namespace std; namespace utils { void out_of_memory_handler() { cout << "Failed to allocate memory." << endl; - exit_with(ExitCode::SEARCH_OUT_OF_MEMORY); + exit_with_reentrant(ExitCode::SEARCH_OUT_OF_MEMORY); } void signal_handler(int signal_number) {