X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=a37e00521ea7761608db62b32cec81faadbcf5c4;hb=c7a5091afba87a67423c0797fa001914ce9e2ff4;hp=d9671a30b7b31bac2b182135edf8c7f26bd1e247;hpb=7bba6b355f7b2250aed59de4b9d20f36c89a3eb4;p=c11tester.git

diff --git a/model.cc b/model.cc
index d9671a30..a37e0052 100644
--- a/model.cc
+++ b/model.cc
@@ -26,6 +26,37 @@ void placeholder(void *) {
 	ASSERT(0);
 }
 
+#include <signal.h>
+
+#define SIGSTACKSIZE 65536
+static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
+{
+	model_print("Segmentation fault at %p\n", si->si_addr);
+	model_print("For debugging, place breakpoint at: %s:%d\n",
+							__FILE__, __LINE__);
+	print_trace();	// Trace printing may cause dynamic memory allocation
+	while(1)
+		;
+}
+
+void install_handler() {
+	stack_t ss;
+	ss.ss_sp = model_malloc(SIGSTACKSIZE);
+	ss.ss_size = SIGSTACKSIZE;
+	ss.ss_flags = 0;
+	sigaltstack(&ss, NULL);
+	struct sigaction sa;
+	sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
+	sigemptyset(&sa.sa_mask);
+	sa.sa_sigaction = mprot_handle_pf;
+
+	if (sigaction(SIGSEGV, &sa, NULL) == -1) {
+		perror("sigaction(SIGSEGV)");
+		exit(EXIT_FAILURE);
+	}
+
+}
+
 /** @brief Constructor */
 ModelChecker::ModelChecker() :
 	/* Initialize default scheduler */
@@ -54,8 +85,7 @@ ModelChecker::ModelChecker() :
 	parse_options(&params);
 	initRaceDetector();
 	/* Configure output redirection for the model-checker */
-	redirect_output();
-	install_trace_analyses(get_execution());
+	install_handler();
 }
 
 /** @brief Destructor */
@@ -262,6 +292,7 @@ void ModelChecker::finish_execution(bool more_executions)
 	execution_number ++;
 	if (more_executions)
 		reset_to_initial_state();
+
 	history->set_new_exec_flag();
 }
 
@@ -537,6 +568,9 @@ static void runChecker() {
 void ModelChecker::startChecker() {
 	startExecution(get_system_context(), runChecker);
 	snapshot = take_snapshot();
+
+	install_trace_analyses(get_execution());
+	redirect_output();
 	initMainThread();
 }