Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Hide system-dependent message.
[simgrid.git] / src / mc / ModelChecker.cpp
index 7bc9774..338c107 100644 (file)
@@ -38,7 +38,6 @@ ModelChecker::ModelChecker(std::unique_ptr<RemoteClient> process)
     , signal_event_(nullptr)
     , page_store_(500)
     , process_(std::move(process))
-    , parent_snapshot_(nullptr)
 {
 
 }
@@ -54,17 +53,12 @@ ModelChecker::~ModelChecker() {
 
 void ModelChecker::start()
 {
-  const pid_t pid = process_->pid();
-
   base_ = event_base_new();
   event_callback_fn event_callback = [](evutil_socket_t fd, short events, void *arg)
   {
     ((ModelChecker *)arg)->handle_events(fd, events);
   };
-  socket_event_ = event_new(base_,
-                            process_->getChannel().getSocket(),
-                            EV_READ|EV_PERSIST,
-                            event_callback, this);
+  socket_event_ = event_new(base_, process_->get_channel().get_socket(), EV_READ | EV_PERSIST, event_callback, this);
   event_add(socket_event_, NULL);
   signal_event_ = event_new(base_,
                             SIGCHLD,
@@ -76,6 +70,8 @@ void ModelChecker::start()
   int status;
 
   // The model-checked process SIGSTOP itself to signal it's ready:
+  const pid_t pid = process_->pid();
+
   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");
@@ -130,7 +126,7 @@ void ModelChecker::shutdown()
 
 void ModelChecker::resume(simgrid::mc::RemoteClient& process)
 {
-  int res = process.getChannel().send(MC_MESSAGE_CONTINUE);
+  int res = process.get_channel().send(MC_MESSAGE_CONTINUE);
   if (res)
     throw simgrid::xbt::errno_error();
   process.clear_cache();
@@ -145,17 +141,19 @@ static void MC_report_crash(int status)
     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().dumpStack();
+  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()
@@ -273,7 +271,7 @@ void ModelChecker::handle_events(int fd, short events)
 {
   if (events == EV_READ) {
     char buffer[MC_MESSAGE_LENGTH];
-    ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false);
+    ssize_t size = process_->get_channel().receive(buffer, sizeof(buffer), false);
     if (size == -1 && errno != EAGAIN)
       throw simgrid::xbt::errno_error();
     if (not handle_message(buffer, size)) {
@@ -368,7 +366,7 @@ void ModelChecker::handle_simcall(Transition const& transition)
   m.type  = MC_MESSAGE_SIMCALL_HANDLE;
   m.pid   = transition.pid;
   m.value = transition.argument;
-  this->process_->getChannel().send(m);
+  this->process_->get_channel().send(m);
   this->process_->clear_cache();
   if (this->process_->running())
     event_base_dispatch(base_);
@@ -377,10 +375,10 @@ void ModelChecker::handle_simcall(Transition const& transition)
 bool ModelChecker::checkDeadlock()
 {
   int res;
-  if ((res = this->process().getChannel().send(MC_MESSAGE_DEADLOCK_CHECK)))
+  if ((res = this->process().get_channel().send(MC_MESSAGE_DEADLOCK_CHECK)))
     xbt_die("Could not check deadlock state");
   s_mc_message_int_t message;
-  ssize_t s = mc_model_checker->process().getChannel().receive(message);
+  ssize_t s = mc_model_checker->process().get_channel().receive(message);
   if (s == -1)
     xbt_die("Could not receive message");
   if (s != sizeof(message) || message.type != MC_MESSAGE_DEADLOCK_CHECK_REPLY)