#include "src/mc/mc_private.h"
#include "src/mc/mc_ignore.h"
#include "src/mc/mc_exit.h"
+#include "src/mc/mc_record.h"
#include "src/mc/Transition.hpp"
+#include "src/mc/Checker.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker");
process_->init();
- /* Initialize statistics */
- mc_stats = xbt_new0(s_mc_stats_t, 1);
-
if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0'))
MC_init_dot_output();
throw simgrid::xbt::errno_error(errno);
}
+static void MC_report_crash(int status)
+{
+ XBT_INFO("**************************");
+ XBT_INFO("** CRASH IN THE PROGRAM **");
+ XBT_INFO("**************************");
+ if (WIFSIGNALED(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.");
+ XBT_INFO("Counter-example execution trace:");
+ simgrid::mc::dumpRecordPath();
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
+ simgrid::mc::session->logState();
+ XBT_INFO("Stack trace:");
+ mc_model_checker->process().dumpStack();
+}
+
+static void MC_report_assertion_error(void)
+{
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ XBT_INFO("Counter-example execution trace:");
+ simgrid::mc::dumpRecordPath();
+ for (auto& s : mc_model_checker->getChecker()->getTextualTrace())
+ XBT_INFO("%s", s.c_str());
+ simgrid::mc::session->logState();
+}
+
bool ModelChecker::handle_message(char* buffer, ssize_t size)
{
s_mc_message_t base_message;