Merge branch 'udpor-phase4' into 'master'

[simgrid.git] / src / mc / ModelChecker.cpp

diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp
index eac05cd7d4f6e56d9110802ea5b3683c22235328..e4024eabafc2453681ef5756b6a8b9bbd3e39f38 100644 (file)
--- a/src/mc/ModelChecker.cpp
+++ b/src/mc/ModelChecker.cpp
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2022. The SimGrid Team. All rights reserved.          */
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved.          */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -67,14 +67,6 @@ void ModelChecker::start()
   xbt_assert(waitpid(pid, &status, WAITPID_CHECKED_FLAGS) == pid && WIFSTOPPED(status) && WSTOPSIG(status) == SIGSTOP,
              "Could not wait model-checked process");
 
-  if (not _sg_mc_dot_output_file.get().empty()) {
-    dot_output_ = fopen(_sg_mc_dot_output_file.get().c_str(), "w");
-    xbt_assert(dot_output_ != nullptr, "Error open dot output file: %s", strerror(errno));
-
-    fprintf(dot_output_, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node "
-                         "[fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
-  }
-
   setup_ignore();
 
   errno = 0;
@@ -93,16 +85,6 @@ void ModelChecker::start()
              errno);
 }
 
-void ModelChecker::dot_output(const char* fmt, ...)
-{
-  if (dot_output_ != nullptr) {
-    va_list ap;
-    va_start(ap, fmt);
-    vfprintf(dot_output_, fmt, ap);
-    va_end(ap);
-  }
-}
-
 static constexpr auto ignored_local_variables = {
     std::make_pair("e", "*"),
     std::make_pair("_log_ev", "*"),
@@ -284,7 +266,9 @@ void ModelChecker::handle_waitpid()
       // From PTRACE_O_TRACEEXIT:
 #ifdef __linux__
       if (status>>8 == (SIGTRAP | (PTRACE_EVENT_EXIT<<8))) {
-        xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &status) != -1, "Could not get exit status");
+        unsigned long eventmsg;
+        xbt_assert(ptrace(PTRACE_GETEVENTMSG, remote_process_->pid(), 0, &eventmsg) != -1, "Could not get exit status");
+        status = static_cast<int>(eventmsg);
         if (WIFSIGNALED(status)) {
           MC_report_crash(exploration_, status);
           this->get_remote_process().terminate();
@@ -326,8 +310,7 @@ void ModelChecker::wait_for_requests()
 
 Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool new_transition)
 {
-  s_mc_message_simcall_execute_t m;
-  memset(&m, 0, sizeof(m));
+  s_mc_message_simcall_execute_t m = {};
   m.type              = MessageType::SIMCALL_EXECUTE;
   m.aid_              = aid;
   m.times_considered_ = times_considered;
@@ -355,8 +338,7 @@ Transition* ModelChecker::handle_simcall(aid_t aid, int times_considered, bool n
 
 void ModelChecker::finalize_app(bool terminate_asap)
 {
-  s_mc_message_int_t m;
-  memset(&m, 0, sizeof m);
+  s_mc_message_int_t m = {};
   m.type  = MessageType::FINALIZE;
   m.value = terminate_asap;
   xbt_assert(checker_side_.get_channel().send(m) == 0, "Could not ask the app to finalize on need");