X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/2b1c48aa8ff28c0d706779f2a69aadc5333e48ab..a0c5f40f68a69e5fd2c22643c98aed7570191e21:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 476c4d452f..461f6c0f20 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -71,6 +71,7 @@ mc_stats_t mc_stats = NULL; mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness = NULL; mc_snapshot_t initial_snapshot_liveness = NULL; +int compare; xbt_automaton_t _mc_property_automaton = NULL; @@ -131,6 +132,7 @@ void MC_init_safety(void) MC_take_snapshot(initial_snapshot); MC_UNSET_RAW_MEM; + if(raw_mem_set) MC_SET_RAW_MEM; else @@ -138,6 +140,10 @@ void MC_init_safety(void) } +void MC_compare(void){ + compare = 1; +} + void MC_modelcheck(void) { @@ -155,6 +161,8 @@ void MC_modelcheck_liveness(){ mc_time = xbt_new0(double, simix_process_maxpid); + compare = 0; + /* Initialize the data structures that must be persistent across every iteration of the model-checker (in RAW memory) */ @@ -599,7 +607,6 @@ void MC_diff(void){ switch(sn->regions[i]->type){ case 0: /* heap */ XBT_INFO("Size of heap : %zu", sn->regions[i]->size); - mmalloc_display_info_heap(sn->regions[i]->data); break; case 1 : /* libsimgrid */ XBT_INFO("Size of libsimgrid : %zu", sn->regions[i]->size);