-/* 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. */
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())
- MC_init_dot_output();
+ 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);
}
+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", "*"),
XBT_INFO("Counter-example execution trace:");
for (auto const& s : explorer->get_textual_trace())
XBT_INFO(" %s", s.c_str());
- XBT_INFO("Path = %s", explorer->get_record_trace().to_string().c_str());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ explorer->get_record_trace().to_string().c_str());
explorer->log_state();
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
XBT_INFO("Counter-example execution trace:");
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());
+ XBT_INFO("You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with "
+ "--cfg=model-check/replay:'%s'",
+ get_exploration()->get_record_trace().to_string().c_str());
exploration_->log_state();
this->exit(SIMGRID_MC_EXIT_SAFETY);
// 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();
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;
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");