X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/83a2c3a9dd2104f4db2f42a483b212f07aa39f6b..b487d5a9259b88670b8cd97e9c16e4b000c11008:/src/mc/mc_safety.c diff --git a/src/mc/mc_safety.c b/src/mc/mc_safety.c index 6f671f2bdf..401c43b772 100644 --- a/src/mc/mc_safety.c +++ b/src/mc/mc_safety.c @@ -5,6 +5,7 @@ * under the terms of the license (GNU LGPL) which comes with this package. */ #include "mc_private.h" +#include "mc_record.h" #include "xbt/mmalloc/mmprivate.h" @@ -117,17 +118,13 @@ void MC_modelcheck_safety(void) if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached && (req = MC_state_get_request(state, &value)) && visited_state == NULL) { - /* Debug information */ - if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) { - req_str = MC_request_to_string(req, value); - XBT_DEBUG("Execute: %s", req_str); - xbt_free(req_str); - } + MC_LOG_REQUEST(mc_safety, req, value); - MC_SET_MC_HEAP; - if (dot_output != NULL) + if (dot_output != NULL) { + MC_SET_MC_HEAP; req_str = MC_request_get_dot_output(req, value); - MC_SET_STD_HEAP; + MC_SET_STD_HEAP; + } MC_state_set_executed_request(state, req, value); mc_stats->executed_transitions++; @@ -141,7 +138,7 @@ void MC_modelcheck_safety(void) } /* Answer the request */ - SIMIX_simcall_pre(req, value); + SIMIX_simcall_handle(req, value); /* Wait for requests (schedules processes) */ MC_wait_for_requests();