#include "xbt/automaton.hpp"
#include "xbt/system_error.hpp"
+#include <sys/ptrace.h>
#include <sys/wait.h>
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
// The model-checked process SIGSTOP itself to signal it's ready:
const pid_t pid = process_->pid();
- pid_t res = waitpid(pid, &status, WUNTRACED | WAITPID_CHECKED_FLAGS);
+ pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS);
if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP)
xbt_die("Could not wait model-checked process");
setup_ignore();
- if (kill(pid, SIGCONT) != 0)
- throw simgrid::xbt::errno_error("Could not wake up the model-checked process");
+#ifdef __linux__
+ ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
+ ptrace(PTRACE_CONT, pid, 0, 0);
+#elif defined BSD
+ ptrace(PT_CONTINUE, pid, (caddr_t)1, 0);
+#else
+# error "no ptrace equivalent coded for this platform"
+#endif
}
static const std::pair<const char*, const char*> ignored_local_variables[] = {
XBT_INFO("From signal: %s", strsignal(WTERMSIG(status)));
else if (WIFEXITED(status))
XBT_INFO("From exit: %i", WEXITSTATUS(status));
- if (WCOREDUMP(status))
- XBT_INFO("A core dump was generated by the system.");
- else
- XBT_INFO("No core dump was generated by the system.");
+ if (not xbt_log_no_loc)
+ XBT_INFO("%s core dump was generated by the system.", WCOREDUMP(status) ? "A" : "No");
XBT_INFO("Counter-example execution trace:");
for (auto const& s : mc_model_checker->getChecker()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
simgrid::mc::dumpRecordPath();
simgrid::mc::session->log_state();
- XBT_INFO("Stack trace:");
- mc_model_checker->process().dump_stack();
+ if (xbt_log_no_loc) {
+ XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
+ } else {
+ XBT_INFO("Stack trace:");
+ mc_model_checker->process().dump_stack();
+ }
}
static void MC_report_assertion_error()
}
if (pid == this->process().pid()) {
- xbt_assert(WIFEXITED(status) || WIFSIGNALED(status));
- XBT_DEBUG("Child process is over");
- this->process().terminate();
+
+ // From PTRACE_O_TRACEEXIT:
+#ifdef __linux__
+ if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
+ if (ptrace(PTRACE_GETEVENTMSG, this->process().pid(), 0, &status) == -1)
+ xbt_die("Could not get exit status");
+ if (WIFSIGNALED(status)) {
+ MC_report_crash(status);
+ mc_model_checker->exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
+ }
+ }
+#endif
+
+ // We don't care about signals, just reinject them:
+ if (WIFSTOPPED(status)) {
+ XBT_DEBUG("Stopped with signal %i", (int) WSTOPSIG(status));
+ errno = 0;
+#ifdef __linux__
+ ptrace(PTRACE_CONT, this->process().pid(), 0, WSTOPSIG(status));
+#elif defined BSD
+ ptrace(PT_CONTINUE, this->process().pid(), (caddr_t)1, WSTOPSIG(status));
+#endif
+ if (errno != 0)
+ xbt_die("Could not PTRACE_CONT");
+ }
+
+ else if (WIFEXITED(status) || WIFSIGNALED(status)) {
+ XBT_DEBUG("Child process is over");
+ this->process().terminate();
+ }
}
}
}