+ MC_init_memory_map_info();
+ MC_init_debug_info(); /* FIXME : get debug information only if liveness verification or visited state reduction */
+
+ if ((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0] != '\0'))
+ MC_init_dot_output();
+
+ /* Init parmap */
+ //parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
+
+ MC_SET_STD_HEAP;
+
+ if (_sg_mc_visited > 0 || _sg_mc_liveness) {
+ /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
+ MC_ignore_local_variable("e", "*");
+ MC_ignore_local_variable("__ex_cleanup", "*");
+ MC_ignore_local_variable("__ex_mctx_en", "*");
+ MC_ignore_local_variable("__ex_mctx_me", "*");
+ MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
+ MC_ignore_local_variable("_log_ev", "*");
+ MC_ignore_local_variable("_throw_ctx", "*");
+ MC_ignore_local_variable("ctx", "*");
+
+ MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot");
+ MC_ignore_local_variable("next_cont"
+ "ext", "smx_ctx_sysv_suspend_serial");
+ MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
+
+ /* Ignore local variable about time used for tracing */
+ MC_ignore_local_variable("start_time", "*");
+
+ MC_ignore_global_variable("mc_model_checker");
+
+ // Mot of those things could be moved into mc_model_checker:
+ MC_ignore_global_variable("compared_pointers");
+ MC_ignore_global_variable("mc_comp_times");
+ MC_ignore_global_variable("mc_snapshot_comparison_time");
+ MC_ignore_global_variable("mc_time");
+ MC_ignore_global_variable("smpi_current_rank");
+ MC_ignore_global_variable("counter"); /* Static variable used for tracing */
+ MC_ignore_global_variable("maestro_stack_start");
+ MC_ignore_global_variable("maestro_stack_end");
+ MC_ignore_global_variable("smx_total_comms");
+
+ if (MC_is_active()) {
+ MC_ignore_global_variable("mc_diff_info");
+ }
+
+ MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+
+ smx_process_t process;
+ xbt_swag_foreach(process, simix_global->process_list) {
+ MC_ignore_heap(&(process->process_hookup),
+ sizeof(process->process_hookup));
+ }
+ }
+
+ if (raw_mem_set)
+ MC_SET_MC_HEAP;
+
+}
+
+/******************************* Core of MC *******************************/
+/**************************************************************************/
+
+static void MC_modelcheck_comm_determinism_init(void)
+{
+
+ int mc_mem_set = (mmalloc_get_current_heap() == mc_heap);
+
+ MC_init();
+
+ if (!mc_mem_set)
+ MC_SET_MC_HEAP;
+