mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-14 08:15:11 +00:00
Code Activity

Fix specbot test harness for POSIX/Linux compatibility

Browse source 
Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/cd4905c3-da72-4e93-b0f4-b512453d2bf6

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-04-02 16:44:21 +00:00 • committed by GitHub
parent 8e165e14c0
commit a87095f931
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 74 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

49
specbot/test_deeptest_seq.c
View file

@ -20,15 +20,15 @@
#include <string.h>
#include <stdlib.h>
#include <setjmp.h>
#ifdef _WIN32
#include <windows.h>
#include <crtdbg.h>
#include <signal.h>
static jmp_buf jmp_env;
static volatile int in_test = 0;
#ifdef _WIN32
#include <windows.h>
#include <crtdbg.h>
void abort_handler(int sig) {
(void)sig;
if (in_test) {
@ -50,13 +50,6 @@ void suppress_dialogs() {
_set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT);
signal(SIGABRT, abort_handler);
}
#else
void suppress_dialogs() {}
#endif
static int tests_run = 0;
static int tests_passed = 0;
static int tests_crashed = 0;
#define RUN_TEST(name) do { \
fprintf(stderr, "[TEST] Running %s\n", #name); \
@ -79,6 +72,40 @@ static int tests_crashed = 0;
} \
} while(0)
#else
void abort_handler(int sig) {
(void)sig;
if (in_test) {
in_test = 0;
signal(SIGABRT, abort_handler);
longjmp(jmp_env, 1);
}
}
void suppress_dialogs() { signal(SIGABRT, abort_handler); }
#define RUN_TEST(name) do { \
fprintf(stderr, "[TEST] Running %s\n", #name); \
tests_run++; \
in_test = 1; \
if (setjmp(jmp_env) == 0) { \
name(); \
in_test = 0; \
tests_passed++; \
fprintf(stderr, "[TEST] PASS %s\n", #name); \
} else { \
tests_crashed++; \
fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \
} \
} while(0)
#endif
static int tests_run = 0;
static int tests_passed = 0;
static int tests_crashed = 0;
/* ===== Helpers ===== */
static Z3_sort mk_string_sort(Z3_context ctx) { return Z3_mk_string_sort(ctx); }
static Z3_ast mk_str(Z3_context ctx, const char* s) { return Z3_mk_string(ctx, s); }

46
specbot/test_specbot_seq.c
View file

@ -4,15 +4,15 @@
#include <stdlib.h>
#include <setjmp.h>
#ifdef _WIN32
#include <windows.h>
#include <crtdbg.h>
#include <signal.h>
static jmp_buf jmp_env;
static volatile int in_test = 0;
#ifdef _WIN32
#include <windows.h>
#include <crtdbg.h>
void abort_handler(int sig) {
(void)sig;
if (in_test) {
@ -34,12 +34,6 @@ void suppress_dialogs() {
_set_abort_behavior(0, _WRITE_ABORT_MSG | _CALL_REPORTFAULT);
signal(SIGABRT, abort_handler);
}
#else
void suppress_dialogs() {}
#endif
static int tests_run = 0;
static int tests_passed = 0;
#define RUN_TEST(name) do { \
fprintf(stderr, "[TEST] Running %s\n", #name); \
@ -60,6 +54,38 @@ static int tests_passed = 0;
} \
} while(0)
#else
void abort_handler(int sig) {
(void)sig;
if (in_test) {
in_test = 0;
signal(SIGABRT, abort_handler);
longjmp(jmp_env, 1);
}
}
void suppress_dialogs() { signal(SIGABRT, abort_handler); }
#define RUN_TEST(name) do { \
fprintf(stderr, "[TEST] Running %s\n", #name); \
tests_run++; \
in_test = 1; \
if (setjmp(jmp_env) == 0) { \
name(); \
in_test = 0; \
tests_passed++; \
fprintf(stderr, "[TEST] PASS %s\n", #name); \
} else { \
fprintf(stderr, "[TEST] ABORT %s (caught SIGABRT)\n", #name); \
} \
} while(0)
#endif
static int tests_run = 0;
static int tests_passed = 0;
/* Helper to create string sort, variables, constants */
Z3_sort mk_string_sort(Z3_context ctx) { return Z3_mk_string_sort(ctx); }
Z3_ast mk_string_var(Z3_context ctx, const char* name) {