model-checker : move function from mc_global in mm_module (compilation error without MC)

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 186335f..97e31b9 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -86,6 +86,8 @@ void _mc_cfg_cb_visited(const char *name, int pos) {
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
+mc_comparison_times_t mc_comp_times = NULL;
+double mc_snapshot_comparison_time;
 
 /* Safety */
 
@@ -120,8 +122,15 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr);
 static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset);
 static size_t data_bss_ignore_size(void *address);
 static void MC_get_global_variables(char *elf_file);
+static void heap_ignore_region_free(mc_heap_ignore_region_t r);
+static void heap_ignore_region_free_voidp(void *r);
 
 void MC_do_the_modelcheck_for_real() {
+
+  MC_SET_RAW_MEM;
+  mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
+  MC_UNSET_RAW_MEM;
+
   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
     if (mc_reduce_kind==e_mc_reduce_unset)
       mc_reduce_kind=e_mc_reduce_dpor;
@@ -183,7 +192,9 @@ void MC_init(){
   get_binary_plt_section();
 
   MC_ignore_data_bss(&end_raw_heap, sizeof(end_raw_heap));
- 
+  MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
+  MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
+
   /* Get global variables */
   MC_get_global_variables(xbt_binary_name);
   MC_get_global_variables(libsimgrid_path);
@@ -735,6 +746,15 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
 /************ MC_ignore ***********/ 
 
+static void heap_ignore_region_free(mc_heap_ignore_region_t r){
+  if(r)
+    xbt_free(r);
+}
+
+static void heap_ignore_region_free_voidp(void *r){
+  heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
+}
+
 void MC_ignore_heap(void *address, size_t size){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -742,25 +762,21 @@ void MC_ignore_heap(void *address, size_t size){
   MC_SET_RAW_MEM;
   
   if(mc_heap_comparison_ignore == NULL)
-    mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), NULL);
+    mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
 
   mc_heap_ignore_region_t region = NULL;
   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
   region->address = address;
   region->size = size;
 
-  if((address >= std_heap) && (address <= (void*)((char *)std_heap + STD_HEAP_SIZE))){
-
-    region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
-    
-    if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
-      region->fragment = -1;
-      ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1;
-    }else{
-      region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
-      ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
-    }
-    
+  region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
+  
+  if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
+    region->fragment = -1;
+    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore = 1;
+  }else{
+    region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
+    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment] = 1;
   }
 
   unsigned int cursor = 0;