mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

debug : Add support for selecting LLDB via invoke on macOS (#7726)

Browse source
This commit is contained in:
LeeYoungJoon 2025-07-12 16:02:09 +09:00 • committed by GitHub
parent 0995928f6e
commit e575919657
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 24 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/util/debug.cpp
View file

@ -117,7 +117,7 @@ void set_default_debug_action(debug_action a) {
} }
debug_action ask_debug_action(std::istream& in) { debug_action ask_debug_action(std::istream& in) {
std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB\n"; std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB, Invoke (L)LDB\n";
char result; char result;
bool ok = bool(in >> result); bool ok = bool(in >> result);
if (!ok) if (!ok)
@ -137,7 +137,10 @@ debug_action ask_debug_action(std::istream& in) {
return debug_action::throw_exception; return debug_action::throw_exception;
case 'G': case 'G':
case 'g': case 'g':
return debug_action::invoke_debugger; return debug_action::invoke_gdb;
case 'L':
case 'l':
return debug_action::invoke_lldb;
default: default:
std::cerr << "INVALID COMMAND\n"; std::cerr << "INVALID COMMAND\n";
return debug_action::ask; return debug_action::ask;
@ -145,7 +148,7 @@ debug_action ask_debug_action(std::istream& in) {
} }
#if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER) #if !defined(_WINDOWS) && !defined(NO_Z3_DEBUGGER)
void invoke_gdb() { void invoke_debugger() {
std::string buffer; std::string buffer;
int *x = nullptr; int *x = nullptr;
debug_action a = get_default_debug_action(); debug_action a = get_default_debug_action();
@ -161,7 +164,7 @@ void invoke_gdb() {
return; return;
case debug_action::throw_exception: case debug_action::throw_exception:
throw default_exception("assertion violation"); throw default_exception("assertion violation");
case debug_action::invoke_debugger: case debug_action::invoke_gdb:
buffer = "gdb -nw /proc/" + std::to_string(getpid()) + "/exe " + std::to_string(getpid()); buffer = "gdb -nw /proc/" + std::to_string(getpid()) + "/exe " + std::to_string(getpid());
std::cerr << "invoking GDB...\n"; std::cerr << "invoking GDB...\n";
if (system(buffer.c_str()) == 0) { if (system(buffer.c_str()) == 0) {
@ -174,6 +177,19 @@ void invoke_gdb() {
*x = 0; *x = 0;
} }
return; return;
case debug_action::invoke_lldb:
buffer = "lldb -p " + std::to_string(getpid());
std::cerr << "invoking LLDB...\n";
if (system(buffer.c_str()) == 0) {
std::cerr << "continuing the execution...\n";
}
else {
std::cerr << "error starting LLDB...\n";
// forcing seg fault.
int *x = nullptr;
*x = 0;
}
return;
case debug_action::ask: case debug_action::ask:
default: default:
a = ask_debug_action(std::cin); a = ask_debug_action(std::cin);

7
src/util/debug.h
View file

@ -30,7 +30,8 @@ enum class debug_action {
abort, abort,
stop, stop,
throw_exception, throw_exception,
invoke_debugger, invoke_gdb,
invoke_lldb
}; };
debug_action get_default_debug_action(); debug_action get_default_debug_action();
void set_default_debug_action(debug_action a); void set_default_debug_action(debug_action a);
@ -69,8 +70,8 @@ void invoke_exit_action(unsigned int code);
#ifdef _WINDOWS #ifdef _WINDOWS
#define INVOKE_DEBUGGER() __debugbreak() #define INVOKE_DEBUGGER() __debugbreak()
#else #else
void invoke_gdb(); void invoke_debugger();
#define INVOKE_DEBUGGER() invoke_gdb() #define INVOKE_DEBUGGER() invoke_debugger()
#endif #endif
#endif #endif