+void MC_modelcheck_safety(void)
+{
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ /* Check if MC is already initialized */
+ if (initial_state_safety)
+ return;
+
+ mc_time = xbt_new0(double, simix_process_maxpid);
+
+ /* Initialize the data structures that must be persistent across every
+ iteration of the model-checker (in RAW memory) */
+
+ MC_SET_RAW_MEM;
+
+ /* Initialize statistics */
+ mc_stats = xbt_new0(s_mc_stats_t, 1);
+ mc_stats->state_size = 1;
+
+ /* Create exploration stack */
+ mc_stack_safety = xbt_fifo_new();
+
+ MC_UNSET_RAW_MEM;
+
+ if(_surf_mc_stateful > 0){
+ MC_init();
+ }else{
+ MC_init_memory_map_info();
+ get_libsimgrid_plt_section();
+ get_binary_plt_section();
+ }
+
+ MC_dpor_init();
+
+ MC_SET_RAW_MEM;
+ /* Save the initial state */
+ initial_state_safety = xbt_new0(s_mc_global_t, 1);
+ initial_state_safety->snapshot = MC_take_snapshot();
+ //MC_take_snapshot(initial_snapshot);
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ MC_dpor();
+
+ MC_exit();
+}
+