Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : update state equality detection
[simgrid.git] / src / mc / mc_global.c
index 461e0b5..43d5097 100644 (file)
@@ -1,4 +1,4 @@
-/* Copyright (c) 2008-2012 Da SimGrid Team. All rights reserved.            */
+/* Copyright (c) 2008-2013 Da SimGrid Team. All rights reserved.            */
 
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
@@ -30,6 +30,7 @@ char* _sg_mc_property_file=NULL;
 int _sg_mc_timeout=0;
 int _sg_mc_max_depth=1000;
 int _sg_mc_visited=0;
+char *_sg_mc_dot_output_file = NULL;
 
 extern int _sg_init_status;
 void _mc_cfg_cb_reduce(const char *name, int pos) {
@@ -80,6 +81,12 @@ void _mc_cfg_cb_visited(const char *name, int pos) {
   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
 }
 
+void _mc_cfg_cb_dot_output(const char *name, int pos) {
+  if (_sg_init_status && !_sg_do_model_check) {
+    xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+  }
+  _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
+}
 
 /* MC global data structures */
 
@@ -88,16 +95,15 @@ char mc_replay_mode = FALSE;
 double *mc_time = NULL;
 mc_comparison_times_t mc_comp_times = NULL;
 double mc_snapshot_comparison_time;
+mc_stats_t mc_stats = NULL;
 
 /* Safety */
 
 xbt_fifo_t mc_stack_safety = NULL;
-mc_stats_t mc_stats = NULL;
 mc_global_t initial_state_safety = NULL;
 
 /* Liveness */
 
-mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_global_t initial_state_liveness = NULL;
 int compare;
@@ -113,6 +119,9 @@ xbt_dynar_t mc_data_bss_comparison_ignore;
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
+FILE *dot_output = NULL;
+const char* colors[10];
+
 xbt_automaton_t _mc_property_automaton = NULL;
 
 /* Static functions */
@@ -122,14 +131,18 @@ 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_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+    MC_SET_RAW_MEM;
+    MC_init_dot_output();
+    MC_UNSET_RAW_MEM;
+  }
 
   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
     if (mc_reduce_kind==e_mc_reduce_unset)
@@ -158,13 +171,6 @@ void MC_init(){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
   
-  mc_time = xbt_new0(double, simix_process_maxpid);
-
-  /* mc_time refers to clock for each process -> ignore it for heap comparison */
-  int i;
-  for(i = 0; i<simix_process_maxpid; i++)
-    MC_ignore_heap(&(mc_time[i]), sizeof(double));
-  
   compare = 0;
 
   /* Initialize the data structures that must be persistent across every
@@ -191,10 +197,6 @@ void MC_init(){
   get_libsimgrid_plt_section();
   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);
@@ -214,11 +216,40 @@ void MC_init(){
   MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
   MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
 
+  /* Ignore local variable about time used for tracing */
+  MC_ignore_stack("start_time", "*"); 
+
+  MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
+  MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
+  MC_ignore_data_bss(&mc_time, sizeof(mc_time));
+
   if(raw_mem_set)
     MC_SET_RAW_MEM;
 
 }
 
+void MC_init_dot_output(){
+
+  colors[0] = "blue";
+  colors[1] = "red";
+  colors[2] = "green";
+  colors[3] = "pink";
+  colors[4] = "brown";
+  colors[5] = "purple";
+  colors[6] = "yellow";
+  colors[7] = "orange";
+  
+  dot_output = fopen(_sg_mc_dot_output_file, "w");
+  
+  if(dot_output == NULL){
+    perror("Error open dot output file");
+    xbt_abort();
+  }
+
+  fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.20; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+
+}
+
 void MC_modelcheck_safety(void)
 {
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -229,6 +260,9 @@ void MC_modelcheck_safety(void)
 
   mc_time = xbt_new0(double, simix_process_maxpid);
 
+  /* mc_time refers to clock for each process -> ignore it for heap comparison */  
+  MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+
   /* Initialize the data structures that must be persistent across every
      iteration of the model-checker (in RAW memory) */
   
@@ -274,15 +308,22 @@ void MC_modelcheck_liveness(){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_init();
+
+  mc_time = xbt_new0(double, simix_process_maxpid);
+
+  /* mc_time refers to clock for each process -> ignore it for heap comparison */  
+  MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
  
   MC_SET_RAW_MEM;
-  
   /* Initialize statistics */
-  mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  mc_stats->state_size = 1;
 
   /* Create exploration stack */
   mc_stack_liveness = xbt_fifo_new();
 
+  /* Create the initial state */
   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 
   MC_UNSET_RAW_MEM;
@@ -290,7 +331,7 @@ void MC_modelcheck_liveness(){
   MC_ddfs_init();
 
   /* We're done */
-  MC_print_statistics_pairs(mc_stats_pair);
+  MC_print_statistics(mc_stats);
   xbt_free(mc_time);
 
   if(raw_mem_set)
@@ -301,16 +342,28 @@ void MC_modelcheck_liveness(){
 
 void MC_exit(void)
 {
+  MC_SET_RAW_MEM;
+  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+    fprintf(dot_output, "}\n");
+    fclose(dot_output);
+  }
+  MC_UNSET_RAW_MEM;
+
   xbt_free(mc_time);
   MC_memory_exit();
   xbt_abort();
 }
 
+int SIMIX_pre_mc_random(smx_simcall_t simcall){
+
+  return simcall->mc_value;
+}
+
 
-int MC_random(int min, int max)
+int MC_random(void)
 {
   /*FIXME: return mc_current_state->executed_transition->random.value;*/
-  return 0;
+  return simcall_mc_random();
 }
 
 /**
@@ -359,11 +412,12 @@ void MC_replay(xbt_fifo_t stack, int start)
 {
   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 
-  int value, i = 1;
+  int value, i = 1, count = 1;
   char *req_str;
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item, start_item;
   mc_state_t state;
+  smx_process_t process = NULL;
 
   XBT_DEBUG("**** Begin Replay ****");
 
@@ -383,6 +437,19 @@ void MC_replay(xbt_fifo_t stack, int start)
     }
   }
 
+  MC_SET_RAW_MEM;
+  xbt_dict_reset(first_enabled_state);
+  xbt_swag_foreach(process, simix_global->process_list){
+    if(MC_process_is_enabled(process)){
+      char *key = bprintf("%lu", process->pid);
+      char *data = bprintf("%d", count);
+      xbt_dict_set(first_enabled_state, key, data, NULL);
+      xbt_free(key);
+    }
+  }
+  MC_UNSET_RAW_MEM;
+  
+
   /* Traverse the stack from the state at position start and re-execute the transitions */
   for (item = start_item;
        item != xbt_fifo_get_first_item(stack);
@@ -391,6 +458,12 @@ void MC_replay(xbt_fifo_t stack, int start)
     state = (mc_state_t) xbt_fifo_get_item_content(item);
     saved_req = MC_state_get_executed_request(state, &value);
    
+    MC_SET_RAW_MEM;
+    char *key = bprintf("%lu", saved_req->issuer->pid);
+    xbt_dict_remove(first_enabled_state, key); 
+    xbt_free(key);
+    MC_UNSET_RAW_MEM;
+   
     if(saved_req){
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */
@@ -403,14 +476,32 @@ void MC_replay(xbt_fifo_t stack, int start)
         xbt_free(req_str);
       }
     }
-         
+    
     SIMIX_simcall_pre(req, value);
     MC_wait_for_requests();
+
+    count++;
+
+    MC_SET_RAW_MEM;
+    /* Insert in dict all enabled processes */
+    xbt_swag_foreach(process, simix_global->process_list){
+      if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
+        char *key = bprintf("%lu", process->pid);
+        if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
+          char *data = bprintf("%d", count);
+          xbt_dict_set(first_enabled_state, key, data, NULL);
+        }
+        xbt_free(key);
+      }
+    }
+    MC_UNSET_RAW_MEM;
          
     /* Update statistics */
     mc_stats->visited_states++;
     mc_stats->executed_transitions++;
+
   }
+
   XBT_DEBUG("**** End Replay ****");
 
   if(raw_mem)
@@ -431,7 +522,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
   smx_simcall_t req = NULL, saved_req = NULL;
   xbt_fifo_item_t item;
   mc_state_t state;
-  mc_pair_stateless_t pair;
+  mc_pair_t pair;
   int depth = 1;
 
   XBT_DEBUG("**** Begin Replay ****");
@@ -450,7 +541,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
 
     while(depth <= xbt_fifo_size(stack)){
 
-      pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){
@@ -480,7 +571,8 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
-      mc_stats_pair->visited_pairs++;
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
 
       item = xbt_fifo_get_prev_item(item);
     }
@@ -492,7 +584,7 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
          item != xbt_fifo_get_first_item(stack);
          item = xbt_fifo_get_prev_item(item)) {
 
-      pair = (mc_pair_stateless_t) xbt_fifo_get_item_content(item);
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
       state = (mc_state_t) pair->graph_state;
 
       if(pair->requests > 0){
@@ -522,7 +614,8 @@ void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
       depth++;
     
       /* Update statistics */
-      mc_stats_pair->visited_pairs++;
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
     }
   }  
 
@@ -603,13 +696,13 @@ void MC_show_deadlock(smx_simcall_t req)
 
 void MC_show_stack_liveness(xbt_fifo_t stack){
   int value;
-  mc_pair_stateless_t pair;
+  mc_pair_t pair;
   xbt_fifo_item_t item;
   smx_simcall_t req;
   char *req_str = NULL;
   
   for (item = xbt_fifo_get_last_item(stack);
-       (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
+       (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
     req = MC_state_get_executed_request(pair->graph_state, &value);
     if(req){
@@ -628,11 +721,11 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  mc_pair_stateless_t pair;
+  mc_pair_t pair;
 
   MC_SET_RAW_MEM;
-  while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
-    pair_stateless_free(pair);
+  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
+    MC_pair_delete(pair);
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
@@ -643,26 +736,14 @@ void MC_dump_stack_liveness(xbt_fifo_t stack){
 
 void MC_print_statistics(mc_stats_t stats)
 {
-  //XBT_INFO("State space size ~= %lu", stats->state_size);
-  XBT_INFO("Expanded states = %lu", stats->expanded_states);
-  XBT_INFO("Visited states = %lu", stats->visited_states);
+  if(stats->expanded_pairs == 0){
+    XBT_INFO("Expanded states = %lu", stats->expanded_states);
+    XBT_INFO("Visited states = %lu", stats->visited_states);
+  }else{
+    XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
+    XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
+  }
   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
-  XBT_INFO("Expanded / Visited = %lf",
-           (double) stats->visited_states / stats->expanded_states);
-  /*XBT_INFO("Exploration coverage = %lf",
-    (double)stats->expanded_states / stats->state_size); */
-}
-
-void MC_print_statistics_pairs(mc_stats_pair_t stats)
-{
-  XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
-  XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
-  //XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
-  XBT_INFO("Expanded / Visited = %lf",
-           (double) stats->visited_pairs / stats->expanded_pairs);
-
-  if(mmalloc_get_current_heap() == raw_heap)
-    MC_UNSET_RAW_MEM;
 }
 
 void MC_assert(int prop)
@@ -674,6 +755,12 @@ void MC_assert(int prop)
     XBT_INFO("Counter-example execution trace:");
     MC_dump_stack_safety(mc_stack_safety);
     MC_print_statistics(mc_stats);
+    MC_SET_RAW_MEM;
+    if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
+      fprintf(dot_output, "}\n");
+      fclose(dot_output);
+    }
+    MC_UNSET_RAW_MEM;
     xbt_abort();
   }
 }
@@ -686,7 +773,7 @@ static void MC_assert_pair(int prop){
     //XBT_INFO("Counter-example execution trace:");
     MC_show_stack_liveness(mc_stack_liveness);
     //MC_dump_snapshot_stack(mc_snapshot_stack);
-    MC_print_statistics_pairs(mc_stats_pair);
+    MC_print_statistics(mc_stats);
     xbt_abort();
   }
 }
@@ -735,7 +822,7 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
   if (_mc_property_automaton == NULL)
     _mc_property_automaton = xbt_automaton_new();
 
-  xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
+  xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
 
   MC_UNSET_RAW_MEM;
 
@@ -746,12 +833,11 @@ 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);
+void heap_ignore_region_free(mc_heap_ignore_region_t r){
+  xbt_free(r);
 }
 
-static void heap_ignore_region_free_voidp(void *r){
+void heap_ignore_region_free_voidp(void *r){
   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
 }
 
@@ -760,33 +846,54 @@ void MC_ignore_heap(void *address, size_t size){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
-  
-  if(mc_heap_comparison_ignore == 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;
-
+  
   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;
+    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
   }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;
+    ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
+  }
+  
+  if(mc_heap_comparison_ignore == NULL){
+    mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
+    xbt_dynar_push(mc_heap_comparison_ignore, &region);
+    if(!raw_mem_set)
+      MC_UNSET_RAW_MEM;
+    return;
   }
 
   unsigned int cursor = 0;
-  mc_heap_ignore_region_t current_region;
-  xbt_dynar_foreach(mc_heap_comparison_ignore, cursor, current_region){
+  mc_heap_ignore_region_t current_region = NULL;
+  int start = 0;
+  int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
+  
+  while(start <= end){
+    cursor = (start + end) / 2;
+    current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
+    if(current_region->address == address){
+      heap_ignore_region_free(region);
+      if(!raw_mem_set)
+        MC_UNSET_RAW_MEM;
+      return;
+    }
+    if(current_region->address < address)
+      start = cursor + 1;
     if(current_region->address > address)
-      break;
+      end = cursor - 1;   
   }
 
-  xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
+  if(current_region->address < address)
+    xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
+  else
+    xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
 
   MC_UNSET_RAW_MEM;
 
@@ -799,7 +906,7 @@ void MC_remove_ignore_heap(void *address, size_t size){
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
-  
+
   unsigned int cursor = 0;
   int start = 0;
   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
@@ -845,12 +952,12 @@ void MC_ignore_data_bss(void *address, size_t size){
   if(mc_data_bss_comparison_ignore == NULL)
     mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), NULL);
 
-  if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
+  mc_data_bss_ignore_variable_t var = NULL;
+  var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+  var->address = address;
+  var->size = size;
 
-    mc_data_bss_ignore_variable_t var = NULL;
-    var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
-    var->address = address;
-    var->size = size;
+  if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
 
     xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
 
@@ -875,11 +982,6 @@ void MC_ignore_data_bss(void *address, size_t size){
       if(current_var->address > address)
         end = cursor - 1;
     }
-    mc_data_bss_ignore_variable_t var = NULL;
-    var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
-    var->address = address;
-    var->size = size;
 
     if(current_var->address < address)
       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
@@ -888,6 +990,34 @@ void MC_ignore_data_bss(void *address, size_t size){
 
   }
 
+  /* Remove variable from mc_global_variables */
+
+  if(mc_global_variables != NULL){
+
+    unsigned int cursor = 0;
+    int start = 0;
+    int end = xbt_dynar_length(mc_global_variables) - 1;
+    global_variable_t current_var;
+    int var_found;
+
+    while(start <= end){
+      cursor = (start + end) / 2;
+      current_var = (global_variable_t)xbt_dynar_get_as(mc_global_variables, cursor, global_variable_t);
+      if(current_var->address == var->address){
+        var_found = 1;
+        break;
+      }
+      if(current_var->address < address)
+        start = cursor + 1;
+      if(current_var->address > address)
+        end = cursor - 1;
+    }
+
+    if(var_found)
+      xbt_dynar_remove_at(mc_global_variables, cursor, NULL);
+    
+  }
+
   MC_UNSET_RAW_MEM;
 
   if(raw_mem_set)
@@ -920,7 +1050,7 @@ static size_t data_bss_ignore_size(void *address){
 
 
 
-void MC_ignore_stack(const char *var_name, const char *frame){
+void MC_ignore_stack(const char *var_name, const char *frame_name){
   
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
@@ -934,7 +1064,7 @@ void MC_ignore_stack(const char *var_name, const char *frame){
     mc_stack_ignore_variable_t var = NULL;
     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
     var->var_name = strdup(var_name);
-    var->frame = strdup(frame);
+    var->frame = strdup(frame_name);
 
     xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
 
@@ -948,7 +1078,7 @@ void MC_ignore_stack(const char *var_name, const char *frame){
     while(start <= end){
       cursor = (start + end) / 2;
       current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
-      if(strcmp(current_var->frame, frame) == 0){
+      if(strcmp(current_var->frame, frame_name) == 0){
         if(strcmp(current_var->var_name, var_name) == 0){
           MC_UNSET_RAW_MEM;
           if(raw_mem_set)
@@ -960,24 +1090,36 @@ void MC_ignore_stack(const char *var_name, const char *frame){
         if(strcmp(current_var->var_name, var_name) > 0)
           end = cursor - 1;
       }
-      if(strcmp(current_var->frame, frame) < 0)
+      if(strcmp(current_var->frame, frame_name) < 0)
         start = cursor + 1;
-      if(strcmp(current_var->frame, frame) > 0)
+      if(strcmp(current_var->frame, frame_name) > 0)
         end = cursor - 1;
     }
 
     mc_stack_ignore_variable_t var = NULL;
     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
     var->var_name = strdup(var_name);
-    var->frame = strdup(frame);
+    var->frame = strdup(frame_name);
 
-    if(strcmp(current_var->frame, frame) < 0)
+    if(strcmp(current_var->frame, frame_name) < 0)
       xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
     else
       xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
 
   }
 
+ /* Remove variable from mc_local_variables */
+
+  if(mc_local_variables != NULL){
+
+    if(strcmp(frame_name, "*") != 0){
+      dw_frame_t frame = xbt_dict_get_or_null(mc_local_variables, frame_name);
+      if(frame != NULL)
+        xbt_dict_remove(frame->variables, var_name);
+    }
+
+  }
+
   MC_UNSET_RAW_MEM;
   
   if(raw_mem_set)
@@ -999,6 +1141,7 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
   region->process_name = strdup(name);
   region->context = context;
   region->size = size;
+  region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
   xbt_dynar_push(stacks_areas, &region);
   
   MC_UNSET_RAW_MEM;
@@ -1029,7 +1172,7 @@ xbt_dict_t MC_get_location_list(const char *elf_file){
   int cursor_remove;
   xbt_dynar_t split = NULL;
 
-  while ((read = getline(&line, &n, fp)) != -1) {
+  while ((read = xbt_getline(&line, &n, fp)) != -1) {
 
     /* Wipeout the new line character */
     line[read - 1] = '\0';
@@ -1088,7 +1231,7 @@ xbt_dict_t MC_get_location_list(const char *elf_file){
       xbt_dynar_free(&split);
       free(loc_expr);
 
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
       if(read != -1){
         line[read - 1] = '\0';
         xbt_str_strip_spaces(line);
@@ -1153,12 +1296,12 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
   int new_frame = 0, new_variable = 0;
   dw_frame_t variable_frame, subroutine_frame = NULL;
 
-  read = getline(&line, &n, fp);
+  read = xbt_getline(&line, &n, fp);
 
   while (read != -1) {
 
     if(n == 0){
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
       continue;
     }
  
@@ -1166,7 +1309,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
     line[read - 1] = '\0';
    
     if(strlen(line) == 0){
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
       continue;
     }
 
@@ -1174,7 +1317,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
     xbt_str_strip_spaces(line);
     
     if(line[0] != '<'){
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
       continue;
     }
     
@@ -1192,12 +1335,12 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
       subprogram_start = strdup(strtok(NULL, "<"));
       xbt_str_rtrim(subprogram_start, ">:");
 
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
    
       while(read != -1){
 
         if(n == 0){
-          read = getline(&line, &n, fp);
+          read = xbt_getline(&line, &n, fp);
           continue;
         }
 
@@ -1205,7 +1348,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
         line[read - 1] = '\0';
         
         if(strlen(line) == 0){
-          read = getline(&line, &n, fp);
+          read = xbt_getline(&line, &n, fp);
           continue;
         }
       
@@ -1288,7 +1431,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
 
         }
 
-        read = getline(&line, &n, fp);
+        read = xbt_getline(&line, &n, fp);
 
       }
  
@@ -1300,10 +1443,8 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
       }
 
       xbt_free(subprogram_start);
-      if(subprogram_end != NULL){
-        xbt_free(subprogram_end);
-        subprogram_end = NULL;
-      }
+      xbt_free(subprogram_end);
+      subprogram_end = NULL;
         
 
     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
@@ -1314,12 +1455,12 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
       origin = strdup(strtok(NULL, "<"));
       xbt_str_rtrim(origin, ">:");
       
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
       
       while(read != -1){
 
         if(n == 0){
-          read = getline(&line, &n, fp);
+          read = xbt_getline(&line, &n, fp);
           continue;
         }
 
@@ -1327,7 +1468,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
         line[read - 1] = '\0'; 
 
         if(strlen(line) == 0){
-          read = getline(&line, &n, fp);
+          read = xbt_getline(&line, &n, fp);
           continue;
         }
        
@@ -1393,7 +1534,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
         
         }
 
-        read = getline(&line, &n, fp);
+        read = xbt_getline(&line, &n, fp);
  
       }
 
@@ -1412,7 +1553,7 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
       origin = strdup(strtok(NULL, "<"));
       xbt_str_rtrim(origin, ">:");
 
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
 
       while(read != -1){
 
@@ -1420,12 +1561,12 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
         line[read - 1] = '\0'; 
 
         if(n == 0){
-          read = getline(&line, &n, fp);
+          read = xbt_getline(&line, &n, fp);
           continue;
         }
 
         if(strlen(line) == 0){
-          read = getline(&line, &n, fp);
+          read = xbt_getline(&line, &n, fp);
           continue;
         }
 
@@ -1457,13 +1598,13 @@ void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_
           subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
         }
 
-        read = getline(&line, &n, fp);
+        read = xbt_getline(&line, &n, fp);
       
       }
 
     }else{
 
-      read = getline(&line, &n, fp);
+      read = xbt_getline(&line, &n, fp);
 
     }
 
@@ -1515,13 +1656,13 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_fbregister_op;
-        new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_bregister_op;
         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
-        new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
@@ -1531,7 +1672,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_piece;
-        new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         /*if(strlen(xbt_dynar_get_as(tokens2, 1, char*)) > 1)
           new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, 1, char*));
         else
@@ -1540,7 +1681,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_plus_uconst;
-        new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, 1, char *));
+        new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strcmp(tok, "DW_OP_abs") == 0 || 
                strcmp(tok, "DW_OP_and") == 0 ||
@@ -1560,7 +1701,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_deref;
-        new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
           new_element->location.deref_size = atoi(xbt_dynar_get_as(tokens, cursor, char*));
         else
@@ -1575,7 +1716,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_uconstant;
         new_element->location.uconstant.bytes = 1;
-        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
           new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens, cursor, char*)));
         else
@@ -1585,7 +1726,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_sconstant;
         new_element->location.sconstant.bytes = 1;
-        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
                strcmp(tok2, "DW_OP_const2u:") == 0 ||
@@ -1594,7 +1735,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_uconstant;
         new_element->location.uconstant.bytes = tok2[11] - '0';
-        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
           new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
         else
@@ -1607,7 +1748,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_sconstant;
         new_element->location.sconstant.bytes = tok2[11] - '0';
-        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else{
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
@@ -1780,7 +1921,7 @@ static void MC_get_global_variables(char *elf_file){
 
   int type = strcmp(elf_file, xbt_binary_name); /* 0 = binary, other = libsimgrid */
 
-  while ((read = getline(&line, &n, fp)) != -1){
+  while ((read = xbt_getline(&line, &n, fp)) != -1){
 
     if(n == 0)
       continue;
@@ -1801,7 +1942,6 @@ static void MC_get_global_variables(char *elf_file){
        || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".data") == 0)
        || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".bss") == 0)
        || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "stderr", 6) == 0)
-       || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "counter", 7) == 0)
        || ((size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16) == 0))
       continue;
 
@@ -1817,10 +1957,34 @@ static void MC_get_global_variables(char *elf_file){
     var->size = (size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16);
     var->name = strdup(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*));
 
-    if(data_bss_ignore_size(var->address) > 0)
+    if(data_bss_ignore_size(var->address) > 0){
       global_variable_free(var);
-    else
-      xbt_dynar_push(mc_global_variables, &var);
+    }else{
+      if(xbt_dynar_is_empty(mc_global_variables)){
+        xbt_dynar_push(mc_global_variables, &var);
+      }else{
+        unsigned int cursor = 0;
+        int start = 0;
+        int end = xbt_dynar_length(mc_global_variables) - 1;
+        global_variable_t current_var = NULL;
+      
+        while(start <= end){
+          cursor = (start + end) / 2;
+          current_var = (global_variable_t)xbt_dynar_get_as(mc_global_variables, cursor, global_variable_t);
+          if(current_var->address == var->address)
+            break;
+          if(current_var->address < var->address)
+            start = cursor + 1;
+          if(current_var->address > var->address)
+            end = cursor - 1;
+        }
+        if(current_var->address < var->address)
+          xbt_dynar_insert_at(mc_global_variables, cursor + 1, &var);
+        else
+          xbt_dynar_insert_at(mc_global_variables, cursor, &var);
+      }
+    }
 
     xbt_dynar_free(&line_tokens);