* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/ModelChecker.hpp"
-#include "src/mc/Session.hpp"
#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
setup_ignore();
+ errno = 0;
#ifdef __linux__
ptrace(PTRACE_SETOPTIONS, pid, nullptr, PTRACE_O_TRACEEXIT);
ptrace(PTRACE_CONT, pid, 0, 0);
#else
# error "no ptrace equivalent coded for this platform"
#endif
+ xbt_assert(errno == 0,
+ "Ptrace does not seem to be usable in your setup (errno: %d). "
+ "If you run from within a docker, adding `--cap-add SYS_PTRACE` to the docker line may help. "
+ "If it does not help, please report this bug.",
+ errno);
}
static constexpr auto ignored_local_variables = {
XBT_INFO("From exit: %i", WEXITSTATUS(status));
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->get_exploration()->get_textual_trace())
- XBT_INFO(" %s", s.c_str());
- XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str());
- session_singleton->log_state();
- 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->get_remote_process().dump_stack();
+ if (mc_model_checker->get_exploration()) {
+ XBT_INFO("Counter-example execution trace:");
+ for (auto const& s : mc_model_checker->get_exploration()->get_textual_trace())
+ XBT_INFO(" %s", s.c_str());
+ XBT_INFO("Path = %s", mc_model_checker->get_exploration()->get_record_trace().to_string().c_str());
+ Api::get().get_session().log_state();
+ 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->get_remote_process().dump_stack();
+ }
}
}
xbt_assert(size == sizeof(message), "Broken message. Got %d bytes instead of %d.", (int)size, (int)sizeof(message));
memcpy(&message, buffer, sizeof(message));
- get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors, message.dead_actors);
+ get_remote_process().init(message.mmalloc_default_mdp, message.maxpid, message.actors);
break;
}
for (auto const& s : get_exploration()->get_textual_trace())
XBT_INFO(" %s", s.c_str());
XBT_INFO("Path = %s", get_exploration()->get_record_trace().to_string().c_str());
- session_singleton->log_state();
+ Api::get().get_session().log_state();
this->exit(SIMGRID_MC_EXIT_SAFETY);