X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e6b90556037db15f64d05921eb05de9a4e625f9d..603a2971cfa9ec8a4fd4493b74c5680956828423:/src/mc/ModelChecker.cpp diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index 439e6770ca..8866abb8db 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -163,9 +163,9 @@ static void MC_report_crash(int status) else XBT_INFO("No core dump was generated by the system."); XBT_INFO("Counter-example execution trace:"); - simgrid::mc::dumpRecordPath(); for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) - XBT_INFO("%s", s.c_str()); + XBT_INFO(" %s", s.c_str()); + simgrid::mc::dumpRecordPath(); simgrid::mc::session->logState(); XBT_INFO("Stack trace:"); mc_model_checker->process().dumpStack(); @@ -177,9 +177,9 @@ static void MC_report_assertion_error() XBT_INFO("*** PROPERTY NOT VALID ***"); XBT_INFO("**************************"); XBT_INFO("Counter-example execution trace:"); - simgrid::mc::dumpRecordPath(); for (auto const& s : mc_model_checker->getChecker()->getTextualTrace()) - XBT_INFO("%s", s.c_str()); + XBT_INFO(" %s", s.c_str()); + simgrid::mc::dumpRecordPath(); simgrid::mc::session->logState(); } @@ -265,7 +265,6 @@ bool ModelChecker::handle_message(char* buffer, ssize_t size) case MC_MESSAGE_ASSERTION_FAILED: MC_report_assertion_error(); this->exit(SIMGRID_MC_EXIT_SAFETY); - break; default: xbt_die("Unexpected message from model-checked application");