* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/Session.hpp"
-#include "src/mc/checker/Checker.hpp"
-#include "src/mc/mc_config.hpp"
#include "src/internal_config.h" // HAVE_SMPI
+#include "src/mc/explo/Exploration.hpp"
+#include "src/mc/mc_config.hpp"
#if HAVE_SMPI
#include "smpi/smpi.h"
#include "src/smpi/include/private.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_Session, mc, "Model-checker session");
XBT_LOG_EXTERNAL_CATEGORY(mc_global);
-namespace simgrid {
-namespace mc {
+namespace simgrid::mc {
template <class Code> void run_child_process(int socket, Code code)
{
xbt_assert(fdflags != -1 && fcntl(socket, F_SETFD, fdflags & ~FD_CLOEXEC) != -1,
"Could not remove CLOEXEC for socket");
- // Disable lazy relocation in the model-checked process to prevent the application from
- // modifying its .got.plt during snapshot.
- setenv("LC_BIND_NOW", "1", 1);
-
setenv(MC_ENV_SOCKET_FD, std::to_string(socket).c_str(), 1);
code();
void Session::log_state() const
{
- model_checker_->getChecker()->log_state();
+ model_checker_->get_exploration()->log_state();
if (not _sg_mc_dot_output_file.get().empty()) {
fprintf(dot_output, "}\n");
return ((s_mc_message_int_t*)buff.data())->value;
}
-void Session::check_deadlock()
+void Session::check_deadlock() const
{
xbt_assert(model_checker_->channel().send(MessageType::DEADLOCK_CHECK) == 0, "Could not check deadlock state");
s_mc_message_int_t message;
XBT_CINFO(mc_global, "*** DEADLOCK DETECTED ***");
XBT_CINFO(mc_global, "**************************");
XBT_CINFO(mc_global, "Counter-example execution trace:");
- for (auto const& s : model_checker_->getChecker()->get_textual_trace())
- XBT_CINFO(mc_global, " %s", s.c_str());
- XBT_CINFO(mc_global, "Path = %s", model_checker_->getChecker()->get_record_trace().to_string().c_str());
+ for (auto const& frame : model_checker_->get_exploration()->get_textual_trace())
+ XBT_CINFO(mc_global, " %s", frame.c_str());
+ XBT_CINFO(mc_global, "Path = %s", model_checker_->get_exploration()->get_record_trace().to_string().c_str());
log_state();
throw DeadlockError();
}
}
-
-simgrid::mc::Session* session_singleton;
-}
-}
+} // namespace simgrid::mc