Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : snapshot comparison with the types of variables and cleanup
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 5 Aug 2013 12:48:31 +0000 (14:48 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 5 Aug 2013 12:55:04 +0000 (14:55 +0200)
14 files changed:
include/xbt/mmalloc.h
src/include/mc/datatypes.h
src/include/mc/mc.h
src/mc/mc_checkpoint.c
src/mc/mc_compare.c
src/mc/mc_global.c
src/mc/mc_private.h
src/mc/memory_map.c
src/msg/instr_msg_process.c
src/msg/instr_msg_task.c
src/simix/smx_network.c
src/smpi/instr_smpi.c
src/surf/instr_routing.c
src/xbt/mmalloc/mm_diff.c

index 5e254ea..df40f03 100644 (file)
@@ -19,6 +19,7 @@
 #endif
 
 #include "xbt/dynar.h"
+#include "xbt/dict.h"
 
 /* Datatype representing a separate heap. The whole point of the mmalloc module
  * is to allow several such heaps in the process. It thus works by redefining
@@ -58,15 +59,9 @@ xbt_mheap_t mmalloc_get_current_heap(void);
 int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
 int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2);
 void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t to_ignore1, xbt_dynar_t to_ignore2);
-void match_equals(xbt_dynar_t list);
-int compare_area(void *area1, void* area2, xbt_dynar_t previous);
+int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t all_types, xbt_dict_t other_types, char *type, int pointer_level);
 void reset_heap_information(void);
-
-void mmalloc_backtrace_block_display(void* heapinfo, int block);
-void mmalloc_backtrace_fragment_display(void* heapinfo, int block, int frag);
-void mmalloc_backtrace_display(void *addr);
-
-int is_free_area(void *area, xbt_mheap_t heap);
+int get_pointed_area_size(void *area, int heap);
 
 size_t mmalloc_get_bytes_used(xbt_mheap_t);
 
index 656541b..9be94cc 100644 (file)
@@ -25,16 +25,6 @@ typedef struct s_mc_heap_ignore_region{
   size_t size;
 }s_mc_heap_ignore_region_t, *mc_heap_ignore_region_t;
 
-typedef struct s_mc_stack_ignore_variable{
-  char *var_name;
-  char *frame;
-}s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
-
-typedef struct s_mc_data_bss_ignore_variable{
-  void *address;
-  size_t size;
-}s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
-
 typedef struct s_stack_region{
   void *address;
   char *process_name;
@@ -43,20 +33,39 @@ typedef struct s_stack_region{
   int block;
 }s_stack_region_t, *stack_region_t;
 
-typedef struct s_heap_equality{
-  void *address1;
-  void *address2;
-}s_heap_equality_t, *heap_equality_t;
-
-void heap_equality_free_voidp(void *e);
 void stack_region_free_voidp(void *s);
 
 void heap_ignore_region_free(mc_heap_ignore_region_t r);
 void heap_ignore_region_free_voidp(void *r);
-void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v);
-void data_bss_ignore_variable_free_voidp(void *v);
-void stack_ignore_variable_free(mc_stack_ignore_variable_t v);
-void stack_ignore_variable_free_voidp(void *v);
+
+/************ DWARF structures *************/
+
+typedef enum{
+  e_dw_base_type = 0,
+  e_dw_enumeration_type,
+  e_dw_enumerator,
+  e_dw_typedef,
+  e_dw_const_type,
+  e_dw_array_type,
+  e_dw_pointer_type,
+  e_dw_structure_type,
+  e_dw_union_type,
+  e_dw_subroutine_type,
+  e_dw_volatile_type
+}e_dw_type_type;
+
+typedef struct s_dw_type{
+  e_dw_type_type type;
+  void *id;
+  char *name;
+  int size;
+  char *dw_type_id;
+  xbt_dynar_t members; /* if DW_TAG_structure_type */
+  int is_pointer_type;
+  int offset;
+}s_dw_type_t, *dw_type_t;
+
+char* get_type_description(xbt_dict_t types, char *type_name);
 
 SG_END_DECL()
 #endif                          /* _MC_MC_H */
index 65c8212..6432098 100644 (file)
@@ -56,17 +56,14 @@ void MC_automaton_load(const char *file);
 /****************************** MC ignore **********************************/
 XBT_PUBLIC(void) MC_ignore_heap(void *address, size_t size);
 XBT_PUBLIC(void) MC_remove_ignore_heap(void *address, size_t size);
-XBT_PUBLIC(void) MC_ignore_stack(const char *var_name, const char *frame);
-XBT_PUBLIC(void) MC_ignore_data_bss(void *address, size_t size);
+XBT_PUBLIC(void) MC_ignore_local_variable(const char *var_name, const char *frame, ...);
+XBT_PUBLIC(void) MC_ignore_global_variable(const char *var_name, ...);
 void MC_new_stack_area(void *stack, char *name, void *context, size_t size);
 
 /********************************* Memory *************************************/
 XBT_PUBLIC(void) MC_memory_init(void);  /* Initialize the memory subsystem */
 XBT_PUBLIC(void) MC_memory_exit(void);
 
-/* Trigger for state equality detection (check potential cycle in application) */
-void MC_compare(void);
-
 SG_END_DECL()
 
 #endif                          /* _MC_MC_H */
index 340b1b0..1ad751d 100644 (file)
@@ -24,23 +24,33 @@ void *start_data_libsimgrid, *start_bss_libsimgrid;
 void *start_data_binary, *start_bss_binary;
 void *start_text_binary;
 
-static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size);
-static void MC_region_restore(mc_mem_region_t reg);
-static void MC_region_destroy(mc_mem_region_t reg);
+/* Free functions */
 
-static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start_addr, size_t size);
+static void MC_snapshot_stack_free(mc_snapshot_stack_t s){
+  if(s){
+    xbt_free(s->local_variables->data);
+    xbt_free(s->local_variables);
+    xbt_free(s);
+  }
+}
 
-static void add_value(xbt_dynar_t *list, const char *type, unsigned long int val);
-static xbt_dynar_t take_snapshot_stacks(mc_snapshot_t *s, void *heap);
-static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap);
-static void print_local_variables_values(xbt_dynar_t all_variables);
-static void *get_stack_pointer(void *stack_context, void *heap);
+static void MC_snapshot_stack_free_voidp(void *s){
+  MC_snapshot_stack_free((mc_snapshot_stack_t) * (void **) s);
+}
 
-static void snapshot_stack_free(mc_snapshot_stack_t s);
-static xbt_dynar_t take_snapshot_ignore(void);
+static void local_variable_free(local_variable_t v){
+  xbt_free(v->frame);
+  xbt_free(v->name);
+  xbt_free(v->type);
+  xbt_free(v);
+}
+
+static void local_variable_free_voidp(void *v){
+  local_variable_free((local_variable_t) * (void **) v);
+}
 
-static void get_hash_global(char *snapshot_hash, void *data1, void *data2);
-static void get_hash_local(char *snapshot_hash, xbt_dynar_t stacks);
+
+/* Snapshot regions */
 
 static mc_mem_region_t MC_region_new(int type, void *start_addr, size_t size)
 {
@@ -78,7 +88,7 @@ static void MC_snapshot_add_region(mc_snapshot_t snapshot, int type, void *start
   return;
 } 
 
-static void get_memory_regions(mc_snapshot_t snapshot){
+static void MC_get_memory_regions(mc_snapshot_t snapshot){
 
   FILE *fp;
   char *line = NULL;
@@ -188,7 +198,7 @@ void MC_init_memory_map_info(){
  
   unsigned int i = 0;
   s_map_region_t reg;
-  memory_map_t maps = get_memory_map();
+  memory_map_t maps = MC_get_memory_map();
 
   while (i < maps->mapsize) {
     reg = maps->regions[i];
@@ -227,63 +237,11 @@ void MC_init_memory_map_info(){
     i++;
   }
    
-  free_memory_map(maps);
-
-}
-
-mc_snapshot_t MC_take_snapshot()
-{
-
-  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
-  
-  MC_SET_RAW_MEM;
-
-  mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
-  snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
-
-  /* Save the std heap and the writable mapped pages of libsimgrid and binary */
-  get_memory_regions(snapshot);
-
-  snapshot->to_ignore = take_snapshot_ignore();
-
-  if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")){
-    snapshot->stacks = take_snapshot_stacks(&snapshot, snapshot->regions[0]->data);
-    get_hash_global(snapshot->hash_global, snapshot->regions[1]->data, snapshot->regions[2]->data);
-    get_hash_local(snapshot->hash_local, snapshot->stacks);
-  }
-
-  MC_UNSET_RAW_MEM;
-
-  if(raw_mem)
-    MC_SET_RAW_MEM;
-
-  return snapshot;
-
-}
-
-void MC_restore_snapshot(mc_snapshot_t snapshot)
-{
-  unsigned int i;
-  for(i=0; i < NB_REGIONS; i++){
-    MC_region_restore(snapshot->regions[i]);
-  }
+  MC_free_memory_map(maps);
 
 }
 
-void MC_free_snapshot(mc_snapshot_t snapshot)
-{
-  unsigned int i;
-  for(i=0; i < NB_REGIONS; i++)
-    MC_region_destroy(snapshot->regions[i]);
-
-  xbt_free(snapshot->stack_sizes);
-  xbt_dynar_free(&(snapshot->stacks));
-  xbt_dynar_free(&(snapshot->to_ignore));
-  xbt_free(snapshot);
-}
-
-
-void get_libsimgrid_plt_section(){
+void MC_get_libsimgrid_plt_section(){
 
   FILE *fp;
   char *line = NULL;            /* Temporal storage for each line that is readed */
@@ -348,7 +306,7 @@ void get_libsimgrid_plt_section(){
 
 }
 
-void get_binary_plt_section(){
+void MC_get_binary_plt_section(){
 
   FILE *fp;
   char *line = NULL;            /* Temporal storage for each line that is readed */
@@ -411,56 +369,103 @@ void get_binary_plt_section(){
 
 }
 
-static void add_value(xbt_dynar_t *list, const char *type, unsigned long int val){
-  variable_value_t value = xbt_new0(s_variable_value_t, 1);
-  value->type = strdup(type);
-  if(strcmp(type, "value") == 0){
-    value->value.res = val;
-  }else{
-    value->value.address = (void *)val;
-  }
-  xbt_dynar_push(*list, &value);
-}
-
-static xbt_dynar_t take_snapshot_stacks(mc_snapshot_t *snapshot, void *heap){
-
-  xbt_dynar_t res = xbt_dynar_new(sizeof(s_mc_snapshot_stack_t), snapshot_stack_free_voidp);
+/* Snapshot */
 
-  unsigned int cursor = 0;
-  stack_region_t current_stack;
+static void MC_get_hash_global(char *snapshot_hash, void *data1, void *data2){
   
-  xbt_dynar_foreach(stacks_areas, cursor, current_stack){
-    mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1);
-    st->local_variables = get_local_variables_values(current_stack->context, heap);
-    st->stack_pointer = get_stack_pointer(current_stack->context, heap);
-    xbt_dynar_push(res, &st);
-    (*snapshot)->stack_sizes = xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
-    (*snapshot)->stack_sizes[cursor] = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap)));
-  }
+  /* unsigned int cursor = 0; */
+  /* size_t offset;  */
+  /* global_variable_t current_var;  */
+  /* void *addr_pointed = NULL; */
+  /* void *res = NULL; */
 
-  return res;
+  /* xbt_strbuff_t clear = xbt_strbuff_new(); */
+  
+  /* xbt_dynar_foreach(mc_global_variables, cursor, current_var){ */
+  /*   if(current_var->address < start_data_libsimgrid){ /\* binary *\/ */
+  /*     offset = (char *)current_var->address - (char *)start_data_binary; */
+  /*     addr_pointed = *((void **)((char *)data2 + offset)); */
+  /*     if(((addr_pointed >= start_plt_binary && addr_pointed <= end_plt_binary)) || ((addr_pointed >= std_heap && (char *)addr_pointed <= (char *)std_heap + STD_HEAP_SIZE ))) */
+  /*       continue; */
+  /*     res = xbt_malloc0(current_var->size + 1); */
+  /*     memset(res, 0, current_var->size + 1); */
+  /*     memcpy(res, (char*)data2 + offset, current_var->size); */
+  /*   }else{ /\* libsimgrid *\/ */
+  /*     offset = (char *)current_var->address - (char *)start_data_libsimgrid; */
+  /*     addr_pointed = *((void **)((char *)data1 + offset)); */
+  /*     if((addr_pointed >= start_plt_libsimgrid && addr_pointed <= end_plt_libsimgrid) || (addr_pointed >= std_heap && (char *)addr_pointed <= (char *)std_heap + STD_HEAP_SIZE )) */
+  /*       continue; */
+  /*     res = xbt_malloc0(current_var->size + 1); */
+  /*     memset(res, 0, current_var->size + 1); */
+  /*     memcpy(res, (char*)data1 + offset, current_var->size); */
+  /*   } */
+  /*   if(res != NULL){ */
+  /*     xbt_strbuff_append(clear, (const char*)res); */
+  /*     xbt_free(res); */
+  /*     res = NULL; */
+  /*   } */
+  /* } */
+
+  /* xbt_sha(clear->data, snapshot_hash); */
+
+  /* xbt_strbuff_free(clear); */
 
 }
 
-static void *get_stack_pointer(void *stack_context, void *heap){
-
-  unw_cursor_t c;
-  int ret;
-  unw_word_t sp;
-
-  ret = unw_init_local(&c, (unw_context_t *)stack_context);
-  if(ret < 0){
-    XBT_INFO("unw_init_local failed");
-    xbt_abort();
-  }
-
-  unw_get_reg(&c, UNW_REG_SP, &sp);
-
-  return ((char *)heap + (size_t)(((char *)((long)sp) - (char*)std_heap)));
+static void MC_get_hash_local(char *snapshot_hash, xbt_dynar_t stacks){
+
+  /* xbt_dynar_t tokens = NULL, s_tokens = NULL; */
+  /* unsigned int cursor1 = 0, cursor2 = 0; */
+  /* mc_snapshot_stack_t current_stack; */
+  /* char *frame_name = NULL; */
+  /* void *addr; */
+
+  /* xbt_strbuff_t clear = xbt_strbuff_new(); */
+
+  /* while(cursor1 < xbt_dynar_length(stacks)){ */
+  /*   current_stack = xbt_dynar_get_as(stacks, cursor1, mc_snapshot_stack_t); */
+  /*   tokens = xbt_str_split(current_stack->local_variables->data, NULL); */
+  /*   cursor2 = 0; */
+  /*   while(cursor2 < xbt_dynar_length(tokens)){ */
+  /*     s_tokens = xbt_str_split(xbt_dynar_get_as(tokens, cursor2, char *), "="); */
+  /*     if(xbt_dynar_length(s_tokens) > 1){ */
+  /*       if(strcmp(xbt_dynar_get_as(s_tokens, 0, char *), "frame_name") == 0){ */
+  /*         xbt_free(frame_name); */
+  /*         frame_name = xbt_strdup(xbt_dynar_get_as(s_tokens, 1, char *)); */
+  /*         xbt_strbuff_append(clear, (const char*)xbt_dynar_get_as(tokens, cursor2, char *)); */
+  /*         cursor2++; */
+  /*         xbt_dynar_free(&s_tokens); */
+  /*         continue; */
+  /*       } */
+  /*       addr = (void *) strtoul(xbt_dynar_get_as(s_tokens, 1, char *), NULL, 16); */
+  /*       if(addr > std_heap && (char *)addr <= (char *)std_heap + STD_HEAP_SIZE){ */
+  /*         cursor2++; */
+  /*         xbt_dynar_free(&s_tokens); */
+  /*         continue; */
+  /*       } */
+  /*       if(is_stack_ignore_variable(frame_name, xbt_dynar_get_as(s_tokens, 0, char *))){ */
+  /*         cursor2++; */
+  /*         xbt_dynar_free(&s_tokens); */
+  /*         continue; */
+  /*       } */
+  /*       xbt_strbuff_append(clear, (const char *)xbt_dynar_get_as(tokens, cursor2, char *)); */
+  /*     } */
+  /*     xbt_dynar_free(&s_tokens); */
+  /*     cursor2++; */
+  /*   } */
+  /*   xbt_dynar_free(&tokens); */
+  /*   cursor1++; */
+  /* } */
+
+  /* xbt_free(frame_name); */
+
+  /* xbt_sha(clear->data, snapshot_hash); */
+
+  /* xbt_strbuff_free(clear); */
 
 }
 
-static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap){
+static xbt_dynar_t MC_get_local_variables_values(void *stack_context){
   
   unw_cursor_t c;
   int ret;
@@ -475,21 +480,17 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
 
   unw_word_t ip, sp, off;
   dw_frame_t frame;
-  xbt_dynar_t compose = xbt_dynar_new(sizeof(variable_value_t), variable_value_free_voidp);
 
-  xbt_strbuff_t variables = xbt_strbuff_new();
-  xbt_dict_cursor_t dict_cursor;
-  char *variable_name;
-  dw_local_variable_t current_variable;
-  unsigned int cursor = 0, cursor2 = 0;
+  unsigned int cursor = 0;
+  dw_variable_t current_variable;
   dw_location_entry_t entry = NULL;
   dw_location_t location_entry = NULL;
   unw_word_t res;
-  int frame_found = 0;
+  int frame_found = 0, region_type;
   void *frame_pointer_address = NULL;
-  long true_ip;
-  char *to_append;
+  long true_ip, value;
+
+  xbt_dynar_t variables = xbt_dynar_new(sizeof(local_variable_t), local_variable_free_voidp);
 
   while(ret >= 0){
 
@@ -498,59 +499,50 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
 
     unw_get_proc_name(&c, frame_name, sizeof (frame_name), &off);
 
-    frame = xbt_dict_get_or_null(mc_local_variables, frame_name);
+    if((long)ip > (long)start_text_libsimgrid)
+      frame = xbt_dict_get_or_null(mc_local_variables_libsimgrid, frame_name);
+    else
+      frame = xbt_dict_get_or_null(mc_local_variables_binary, frame_name);
 
     if(frame == NULL){
-      xbt_dynar_free(&compose);
-      xbt_dict_cursor_free(&dict_cursor);
-      return variables;
+      ret = unw_step(&c);
+      continue;
     }
-
-    to_append = bprintf("frame_name=%s\n", frame_name);
-    xbt_strbuff_append(variables, to_append);
-    xbt_free(to_append);
-    to_append = bprintf("ip=%lx\n", (unsigned long)ip);
-    xbt_strbuff_append(variables, to_append);
-    xbt_free(to_append);
     
     true_ip = (long)frame->low_pc + (long)off;
+    frame_pointer_address = NULL;
 
     /* Get frame pointer */
     switch(frame->frame_base->type){
     case e_dw_loclist:
-      while((cursor < xbt_dynar_length(frame->frame_base->location.loclist)) && frame_found == 0){
+      cursor = 0;
+      while(cursor < xbt_dynar_length(frame->frame_base->location.loclist) && !frame_found){
         entry = xbt_dynar_get_as(frame->frame_base->location.loclist, cursor, dw_location_entry_t);
         if((true_ip >= entry->lowpc) && (true_ip < entry->highpc)){
           frame_found = 1;
           switch(entry->location->type){
           case e_dw_compose:
-            xbt_dynar_reset(compose);
-            cursor2 = 0;
-            while(cursor2 < xbt_dynar_length(entry->location->location.compose)){
-              location_entry = xbt_dynar_get_as(entry->location->location.compose, cursor2, dw_location_t);
+            if(xbt_dynar_length(entry->location->location.compose) > 1){
+              frame_pointer_address = NULL; /* TODO : location list with optimizations enabled */
+            }else{
+              location_entry = xbt_dynar_get_as(entry->location->location.compose, 0, dw_location_t);
               switch(location_entry->type){
               case e_dw_register:
                 unw_get_reg(&c, location_entry->location.reg, &res);
-                add_value(&compose, "address", (long)res);
+                frame_pointer_address = (void*)(long)res;
                 break;
               case e_dw_bregister_op:
                 unw_get_reg(&c, location_entry->location.breg_op.reg, &res);
-                add_value(&compose, "address", (long)res + location_entry->location.breg_op.offset);
+                frame_pointer_address = (void*)((long)res + location_entry->location.breg_op.offset);
                 break;
               default:
-                xbt_dynar_reset(compose);
+                frame_pointer_address = NULL; /* FIXME : implement other cases (with optimizations enabled) */
                 break;
               }
-              cursor2++;
-            }
-
-            if(!xbt_dynar_is_empty(compose)){
-              frame_pointer_address = xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1, variable_value_t)->value.address ; 
-              xbt_dynar_reset(compose);
             }
             break;
-          default :
-            frame_pointer_address = NULL;
+          default:
+            frame_pointer_address = NULL; /* FIXME : implement other cases (with optimizations enabled) */
             break;
           }
         }
@@ -558,229 +550,119 @@ static xbt_strbuff_t get_local_variables_values(void *stack_context, void *heap)
       }
       break;
     default :
-      frame_pointer_address = NULL;
+      frame_pointer_address = NULL; /* FIXME : implement other cases (with optimizations enabled)*/
       break;
     }
 
     frame_found = 0;
     cursor = 0;
 
-    xbt_dict_foreach(frame->variables, dict_cursor, variable_name, current_variable){
-      if(current_variable->location != NULL){
-        switch(current_variable->location->type){
+    xbt_dynar_foreach(frame->variables, cursor, current_variable){
+      
+      if((long)ip > (long)start_text_libsimgrid)
+        region_type = 1;
+      else
+        region_type = 2;
+
+      local_variable_t new_var = xbt_new0(s_local_variable_t, 1);
+      new_var->frame = xbt_strdup(frame_name);
+      new_var->ip = (unsigned long)ip;
+      new_var->name = xbt_strdup(current_variable->name);
+      new_var->type = strdup(current_variable->type_origin);
+      new_var->region= region_type;
+      
+      if(current_variable->address.location != NULL){
+        switch(current_variable->address.location->type){
         case e_dw_compose:
-          xbt_dynar_reset(compose);
-          cursor = 0;
-          while(cursor < xbt_dynar_length(current_variable->location->location.compose)){
-            location_entry = xbt_dynar_get_as(current_variable->location->location.compose, cursor, dw_location_t);
+          if(xbt_dynar_length(current_variable->address.location->location.compose) > 1){
+            /* TODO : location list with optimizations enabled */
+          }else{
+            location_entry = xbt_dynar_get_as(current_variable->address.location->location.compose, 0, dw_location_t);
+            
             switch(location_entry->type){
             case e_dw_register:
               unw_get_reg(&c, location_entry->location.reg, &res);
-              add_value(&compose, "value", (long)res);
+              value = (long)res;
               break;
             case e_dw_bregister_op:
               unw_get_reg(&c, location_entry->location.breg_op.reg, &res);
-              add_value(&compose, "address", (long)res + location_entry->location.breg_op.offset);
+              value = (long)res + location_entry->location.breg_op.offset;
               break;
             case e_dw_fbregister_op:
               if(frame_pointer_address != NULL)
-                add_value(&compose, "address", (long)((char *)frame_pointer_address + location_entry->location.fbreg_op));
+                value = (long)((char *)frame_pointer_address + location_entry->location.fbreg_op);
+              else
+                value = 0;
               break;
             default:
-              xbt_dynar_reset(compose);
+              value = 0; /* FIXME : implement other cases (with optimizations enabled)*/
               break;
             }
-            cursor++;
-          }
-          
-          if(!xbt_dynar_is_empty(compose)){
-            if(strcmp(xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1, variable_value_t)->type, "value") == 0){
-              to_append = bprintf("%s=%lx\n", current_variable->name, xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1, variable_value_t)->value.res);
-              xbt_strbuff_append(variables, to_append);
-              xbt_free(to_append);
-            }else{
-              if((long)xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1,variable_value_t)->value.address < 0 || *((void**)xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1,variable_value_t)->value.address) == NULL){
-                to_append = bprintf("%s=NULL\n", current_variable->name);
-                xbt_strbuff_append(variables, to_append);
-                xbt_free(to_append);
-              }else if(((long)*((void**)xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1,variable_value_t)->value.address) > 0xffffffff) || ((long)*((void**)xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1,variable_value_t)->value.address) < (long)start_text_binary)){
-                to_append = bprintf("%s=%u\n", current_variable->name, (unsigned int)(long)*((void**)xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1, variable_value_t)->value.address));
-                xbt_strbuff_append(variables, to_append);
-                xbt_free(to_append);
-              }else{ 
-                to_append = bprintf("%s=%p\n", current_variable->name, *((void**)xbt_dynar_get_as(compose, xbt_dynar_length(compose) - 1, variable_value_t)->value.address));
-                xbt_strbuff_append(variables, to_append);
-                xbt_free(to_append);
-              }
-            }
-            xbt_dynar_reset(compose);
-          }else{
-            to_append = bprintf("%s=undefined\n", current_variable->name);
-            xbt_strbuff_append(variables, to_append);
-            xbt_free(to_append);
+
+            if(value)
+              new_var->address = (void *)value;
+            else
+              new_var->address = NULL;
           }
           break;
         default :
           break;
         }
-      }else{
-        to_append = bprintf("%s=undefined\n", current_variable->name);
-        xbt_strbuff_append(variables, to_append);
-        xbt_free(to_append);
       }
-    }    
+
+      xbt_dynar_push(variables, &new_var);
+
+    }
+
     ret = unw_step(&c);
      
   }
 
-  xbt_dynar_free(&compose);
-  xbt_dict_cursor_free(&dict_cursor);
-
   return variables;
 
 }
 
-static void print_local_variables_values(xbt_dynar_t all_variables){
-
-  unsigned cursor = 0;
-  mc_snapshot_stack_t stack;
 
-  xbt_dynar_foreach(all_variables, cursor, stack){
-    XBT_INFO("%s", stack->local_variables->data);
-  }
-}
+static void *MC_get_stack_pointer(void *stack_context, void *heap){
 
+  unw_cursor_t c;
+  int ret;
+  unw_word_t sp;
 
-static void snapshot_stack_free(mc_snapshot_stack_t s){
-  if(s){
-    xbt_free(s->local_variables->data);
-    xbt_free(s->local_variables);
-    xbt_free(s);
+  ret = unw_init_local(&c, (unw_context_t *)stack_context);
+  if(ret < 0){
+    XBT_INFO("unw_init_local failed");
+    xbt_abort();
   }
-}
 
-void snapshot_stack_free_voidp(void *s){
-  snapshot_stack_free((mc_snapshot_stack_t) * (void **) s);
-}
-
-mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall){
-  return MC_take_snapshot();
-}
+  unw_get_reg(&c, UNW_REG_SP, &sp);
 
-void *MC_snapshot(void){
+  return ((char *)heap + (size_t)(((char *)((long)sp) - (char*)std_heap)));
 
-  return simcall_mc_snapshot();
-  
 }
 
-void variable_value_free(variable_value_t v){
-  if(v){
-    xbt_free(v->type);
-    xbt_free(v);
-  }
-}
+static xbt_dynar_t MC_take_snapshot_stacks(mc_snapshot_t *snapshot, void *heap){
 
-void variable_value_free_voidp(void* v){
-  variable_value_free((variable_value_t) * (void **)v);
-}
+  xbt_dynar_t res = xbt_dynar_new(sizeof(s_mc_snapshot_stack_t), MC_snapshot_stack_free_voidp);
 
-static void get_hash_global(char *snapshot_hash, void *data1, void *data2){
-  
   unsigned int cursor = 0;
-  size_t offset; 
-  global_variable_t current_var; 
-  void *addr_pointed = NULL;
-  void *res = NULL;
-
-  xbt_strbuff_t clear = xbt_strbuff_new();
+  stack_region_t current_stack;
   
-  xbt_dynar_foreach(mc_global_variables, cursor, current_var){
-    if(current_var->address < start_data_libsimgrid){ /* binary */
-      offset = (char *)current_var->address - (char *)start_data_binary;
-      addr_pointed = *((void **)((char *)data2 + offset));
-      if(((addr_pointed >= start_plt_binary && addr_pointed <= end_plt_binary)) || ((addr_pointed >= std_heap && (char *)addr_pointed <= (char *)std_heap + STD_HEAP_SIZE )))
-        continue;
-      res = xbt_malloc0(current_var->size + 1);
-      memset(res, 0, current_var->size + 1);
-      memcpy(res, (char*)data2 + offset, current_var->size);
-    }else{ /* libsimgrid */
-      offset = (char *)current_var->address - (char *)start_data_libsimgrid;
-      addr_pointed = *((void **)((char *)data1 + offset));
-      if((addr_pointed >= start_plt_libsimgrid && addr_pointed <= end_plt_libsimgrid) || (addr_pointed >= std_heap && (char *)addr_pointed <= (char *)std_heap + STD_HEAP_SIZE ))
-        continue;
-      res = xbt_malloc0(current_var->size + 1);
-      memset(res, 0, current_var->size + 1);
-      memcpy(res, (char*)data1 + offset, current_var->size);
-    }
-    if(res != NULL){
-      xbt_strbuff_append(clear, (const char*)res);
-      xbt_free(res);
-      res = NULL;
-    }
-  }
-
-  xbt_sha(clear->data, snapshot_hash);
-
-  xbt_strbuff_free(clear);
-
-}
-
-static void get_hash_local(char *snapshot_hash, xbt_dynar_t stacks){
-
-  xbt_dynar_t tokens = NULL, s_tokens = NULL;
-  unsigned int cursor1 = 0, cursor2 = 0;
-  mc_snapshot_stack_t current_stack;
-  char *frame_name = NULL;
-  void *addr;
-
-  xbt_strbuff_t clear = xbt_strbuff_new();
-
-  while(cursor1 < xbt_dynar_length(stacks)){
-    current_stack = xbt_dynar_get_as(stacks, cursor1, mc_snapshot_stack_t);
-    tokens = xbt_str_split(current_stack->local_variables->data, NULL);
-    cursor2 = 0;
-    while(cursor2 < xbt_dynar_length(tokens)){
-      s_tokens = xbt_str_split(xbt_dynar_get_as(tokens, cursor2, char *), "=");
-      if(xbt_dynar_length(s_tokens) > 1){
-        if(strcmp(xbt_dynar_get_as(s_tokens, 0, char *), "frame_name") == 0){
-          xbt_free(frame_name);
-          frame_name = xbt_strdup(xbt_dynar_get_as(s_tokens, 1, char *));
-          xbt_strbuff_append(clear, (const char*)xbt_dynar_get_as(tokens, cursor2, char *));
-          cursor2++;
-          xbt_dynar_free(&s_tokens);
-          continue;
-        }
-        addr = (void *) strtoul(xbt_dynar_get_as(s_tokens, 1, char *), NULL, 16);
-        if(addr > std_heap && (char *)addr <= (char *)std_heap + STD_HEAP_SIZE){
-          cursor2++;
-          xbt_dynar_free(&s_tokens);
-          continue;
-        }
-        if(is_stack_ignore_variable(frame_name, xbt_dynar_get_as(s_tokens, 0, char *))){
-          cursor2++;
-          xbt_dynar_free(&s_tokens);
-          continue;
-        }
-        xbt_strbuff_append(clear, (const char *)xbt_dynar_get_as(tokens, cursor2, char *));
-      }
-      xbt_dynar_free(&s_tokens);
-      cursor2++;
-    }
-    xbt_dynar_free(&tokens);
-    cursor1++;
+  xbt_dynar_foreach(stacks_areas, cursor, current_stack){
+    mc_snapshot_stack_t st = xbt_new(s_mc_snapshot_stack_t, 1);
+    st->local_variables = MC_get_local_variables_values(current_stack->context);
+    st->stack_pointer = MC_get_stack_pointer(current_stack->context, heap);
+    st->real_address = current_stack->address;
+    xbt_dynar_push(res, &st);
+    (*snapshot)->stack_sizes = xbt_realloc((*snapshot)->stack_sizes, (cursor + 1) * sizeof(size_t));
+    (*snapshot)->stack_sizes[cursor] = current_stack->size - ((char *)st->stack_pointer - (char *)((char *)heap + ((char *)current_stack->address - (char *)std_heap)));
   }
 
-  xbt_free(frame_name);
-
-  xbt_sha(clear->data, snapshot_hash);
-
-  xbt_strbuff_free(clear);
+  return res;
 
 }
 
-
-static xbt_dynar_t take_snapshot_ignore(){
+static xbt_dynar_t MC_take_snapshot_ignore(){
   
   if(mc_heap_comparison_ignore == NULL)
     return NULL;
@@ -803,3 +685,60 @@ static xbt_dynar_t take_snapshot_ignore(){
   return cpy;
 
 }
+
+
+mc_snapshot_t MC_take_snapshot(){
+
+  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
+  
+  MC_SET_RAW_MEM;
+
+  mc_snapshot_t snapshot = xbt_new0(s_mc_snapshot_t, 1);
+  snapshot->nb_processes = xbt_swag_size(simix_global->process_list);
+
+  /* Save the std heap and the writable mapped pages of libsimgrid and binary */
+  MC_get_memory_regions(snapshot);
+
+  snapshot->to_ignore = MC_take_snapshot_ignore();
+
+  if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")){
+    snapshot->stacks = MC_take_snapshot_stacks(&snapshot, snapshot->regions[0]->data);
+    //MC_get_hash_global(snapshot->hash_global, snapshot->regions[1]->data, snapshot->regions[2]->data);
+    //MC_get_hash_local(snapshot->hash_local, snapshot->stacks);
+  }
+
+  MC_UNSET_RAW_MEM;
+
+  if(raw_mem)
+    MC_SET_RAW_MEM;
+
+  return snapshot;
+
+}
+
+void MC_restore_snapshot(mc_snapshot_t snapshot){
+  unsigned int i;
+  for(i=0; i < NB_REGIONS; i++){
+    MC_region_restore(snapshot->regions[i]);
+  }
+
+}
+
+void MC_free_snapshot(mc_snapshot_t snapshot){
+  unsigned int i;
+  for(i=0; i < NB_REGIONS; i++)
+    MC_region_destroy(snapshot->regions[i]);
+
+  xbt_free(snapshot->stack_sizes);
+  xbt_dynar_free(&(snapshot->stacks));
+  xbt_dynar_free(&(snapshot->to_ignore));
+  xbt_free(snapshot);
+}
+
+mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall){
+  return MC_take_snapshot();
+}
+
+void *MC_snapshot(void){
+  return simcall_mc_snapshot();
+}
index 6f379cf..5d8ac72 100644 (file)
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_compare, mc,
                                 "Logging specific to mc_compare");
 
-static int heap_region_compare(void *d1, void *d2, size_t size);
+typedef struct s_pointers_pair{
+  void *p1;
+  void *p2;
+}s_pointers_pair_t, *pointers_pair_t;
+
+xbt_dynar_t compared_pointers;
 
-static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
-static size_t heap_ignore_size(void *address);
+static int heap_region_compare(void *d1, void *d2, size_t size);
 
 static void stack_region_free(stack_region_t s);
-static void heap_equality_free(heap_equality_t e);
 
-static int compare_local_variables(char *s1, char *s2);
-static int compare_global_variables(int region_type, void *d1, void *d2);
+static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack_t stack2, void *heap1, void *heap2);
+static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_region_t r2);
+static int compare_pointer(char *pointer_type, void *addr_pointed1, void *addr_pointed2, int region_size, int region_type);
+static int compare_areas_with_type(void *area1, void *area2, xbt_dict_t types, xbt_dict_t other_types, char *type_id, int region_size, int region_type, void *start_data, int pointer_level);
+
+static int already_compared_pointers(void *p1, void *p2){
+
+  if(xbt_dynar_is_empty(compared_pointers))
+    return -1;
 
-static size_t heap_ignore_size(void *address){
   unsigned int cursor = 0;
   int start = 0;
-  int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
-  mc_heap_ignore_region_t region;
+  int end = xbt_dynar_length(compared_pointers) - 1;
+  pointers_pair_t pair;
 
   while(start <= end){
     cursor = (start + end) / 2;
-    region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
-    if(region->address == address)
-      return region->size;
-    if(region->address < address)
+    pair = (pointers_pair_t)xbt_dynar_get_as(compared_pointers, cursor, pointers_pair_t);
+    if(pair->p1 == p1){
+      if(pair->p2 == p2)
+        return 0;
+      else if(pair->p2 < p2)
+        start = cursor + 1;
+      else
+        end = cursor - 1;
+    }else if(pair->p1 < p1){
       start = cursor + 1;
-    if(region->address > address)
-      end = cursor - 1;   
+    }else{
+      end = cursor - 1 ;
+    }
   }
 
-  return 0;
+  return -1;
+
 }
 
-static int compare_global_variables(int region_type, void *d1, void *d2){ /* region_type = 1 -> libsimgrid, region_type = 2 -> binary */
+static void add_compared_pointers(void *p1, void *p2){
+
+  pointers_pair_t new_pair = xbt_new0(s_pointers_pair_t, 1);
+  new_pair->p1 = p1;
+  new_pair->p2 = p2;
+  
+  if(xbt_dynar_is_empty(compared_pointers)){
+    xbt_dynar_push(compared_pointers, &new_pair);
+    return;
+  }
 
   unsigned int cursor = 0;
-  size_t offset; 
-  int i = 0;
-  global_variable_t current_var; 
-  int pointer_align; 
-  void *addr_pointed1 = NULL, *addr_pointed2 = NULL;
-  int res_compare = 0;
-  void *plt_start, *plt_end;
+  int start = 0;
+  int end = xbt_dynar_length(compared_pointers) - 1;
+  pointers_pair_t pair = NULL;
 
-  if(region_type == 2){
-    plt_start = start_plt_binary;
-    plt_end = end_plt_binary;
+  while(start <= end){
+    cursor = (start + end) / 2;
+    pair = (pointers_pair_t)xbt_dynar_get_as(compared_pointers, cursor, pointers_pair_t);
+    if(pair->p1 == p1){
+      if(pair->p2 == p2)
+        return;
+      else if(pair->p2 < p2)
+        start = cursor + 1;
+      else
+        end = cursor - 1;
+    }else if(pair->p1 < p1){
+      start = cursor + 1;
+    }else{
+      end = cursor - 1 ;
+    }
+  }
+
+  if(pair->p1 == p1){
+    if(pair->p2 < p2)
+      xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
+    else
+      xbt_dynar_insert_at(compared_pointers, cursor, &new_pair); 
   }else{
-    plt_start = start_plt_libsimgrid;
-    plt_end = end_plt_libsimgrid;
+    if(pair->p1 < p1)
+      xbt_dynar_insert_at(compared_pointers, cursor + 1, &new_pair);
+    else
+      xbt_dynar_insert_at(compared_pointers, cursor, &new_pair);   
   }
 
-  xbt_dynar_foreach(mc_global_variables, cursor, current_var){
-    if(current_var->address < start_data_libsimgrid){ /* binary global variable */
-      if(region_type == 1)
-        continue;
-      offset = (char *)current_var->address - (char *)start_data_binary;
-    }else{ /* libsimgrid global variable */
-      if(region_type == 2)
-        break;
-      offset = (char *)current_var->address - (char *)start_data_libsimgrid;
+}
+
+static int compare_areas_with_type(void *area1, void *area2, xbt_dict_t types, xbt_dict_t other_types, char *type_id, int region_size, int region_type, void *start_data, int pointer_level){
+
+  dw_type_t type = xbt_dict_get_or_null(types, type_id);;
+  unsigned int cursor = 0;
+  dw_type_t member, subtype, subsubtype;
+  int elm_size, i, res, switch_types = 0;
+  void *addr_pointed1, *addr_pointed2;
+  int pointed_area_size1, pointed_area_size2;
+
+  switch(type->type){
+  case e_dw_base_type:
+  case e_dw_enumeration_type:
+  case e_dw_union_type:
+    return (memcmp(area1, area2, type->size) != 0);
+    break;
+  case e_dw_typedef:
+  case e_dw_volatile_type:
+    return compare_areas_with_type(area1, area2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
+    break;
+  case e_dw_const_type: /* Const variable cannot be modified */
+    return -1;
+    break;
+  case e_dw_array_type:
+    subtype = xbt_dict_get_or_null(types, type->dw_type_id);
+    switch(subtype->type){
+    case e_dw_base_type:
+    case e_dw_enumeration_type:
+    case e_dw_pointer_type:
+    case e_dw_structure_type:
+    case e_dw_union_type:
+      if(subtype->size == 0){ /*declaration of the type, need the complete description */
+        subtype = xbt_dict_get_or_null(types, get_type_description(types, subtype->name));
+        if(subtype == NULL){
+          subtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subtype->name));
+          switch_types = 1;
+        }
+      }
+      elm_size = subtype->size;
+      break;
+    case e_dw_typedef:
+    case e_dw_volatile_type:
+      subsubtype = xbt_dict_get_or_null(types, subtype->dw_type_id);
+      if(subsubtype->size == 0){ /*declaration of the type, need the complete description */
+        subsubtype = xbt_dict_get_or_null(types, get_type_description(types, subsubtype->name));
+        if(subsubtype == NULL){
+          subsubtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subsubtype->name));
+          switch_types = 1;
+        }
+      }
+      elm_size = subsubtype->size;
+      break;
+    default : 
+      return 0;
+      break;
+    }
+    for(i=0; i<type->size; i++){
+      if(switch_types)
+        res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), other_types, types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
+      else
+        res = compare_areas_with_type((char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level);
+      if(res != 0)
+        return res;
     }
-    i = 0;
-    while(i < current_var->size){
-      if(memcmp((char *)d1 + offset + i, (char *)d2 + offset + i, 1) != 0){ 
-        pointer_align = (i / sizeof(void*)) * sizeof(void*); 
-        addr_pointed1 = *((void **)((char *)d1 + offset + pointer_align));
-        addr_pointed2 = *((void **)((char *)d2 + offset + pointer_align));
-        if((addr_pointed1 > plt_start && addr_pointed1 < plt_end) || (addr_pointed2 > plt_start && addr_pointed2 < plt_end)){
-          i = pointer_align + sizeof(void*);
-          continue;
-        }else if((addr_pointed1 > std_heap) && ((char *)addr_pointed1 < (char *)std_heap + STD_HEAP_SIZE) 
-                && (addr_pointed2 > std_heap) && ((char *)addr_pointed2 < (char *)std_heap + STD_HEAP_SIZE)){
-          res_compare = compare_area(addr_pointed1, addr_pointed2, NULL);
-          if(res_compare == 1){
-            #ifdef MC_VERBOSE
-              if(region_type == 2)
-                XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-              else
-                XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-            #endif
-            #ifdef MC_DEBUG
-              if(region_type == 2)
-                XBT_DEBUG("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-              else
-                XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-            #endif
-            return 1;
-          }
-          i = pointer_align + sizeof(void*);
-          continue;
-        }else{
-          #ifdef MC_VERBOSE
-            if(region_type == 2)
-              XBT_VERB("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-            else
-              XBT_VERB("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-          #endif
-          #ifdef MC_DEBUG
-            if(region_type == 2)
-              XBT_DEBUG("Different global variable in binary : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-            else
-              XBT_DEBUG("Different global variable in libsimgrid : %s at addresses %p - %p (size = %zu)", current_var->name, (char *)d1+offset, (char *)d2+offset, current_var->size);
-          #endif
-          return 1;
-        }              
+    break;
+  case e_dw_pointer_type: 
+    if(type->dw_type_id && ((dw_type_t)xbt_dict_get_or_null(types, type->dw_type_id))->type == e_dw_subroutine_type){
+      addr_pointed1 = *((void **)(area1)); 
+      addr_pointed2 = *((void **)(area2));
+      return (addr_pointed1 != addr_pointed2);
+    }else{
+      addr_pointed1 = *((void **)(area1)); 
+      addr_pointed2 = *((void **)(area2));
+      
+      if((addr_pointed1 == addr_pointed2) && ((pointed_area_size1 = get_pointed_area_size(addr_pointed1, 1)) != (pointed_area_size2 = get_pointed_area_size(addr_pointed2, 2))))
+        return -1;
+      if(addr_pointed1 == NULL && addr_pointed2 == NULL)
+        return 0;
+      if(already_compared_pointers(addr_pointed1, addr_pointed2) != -1)
+        return 0;
+      add_compared_pointers(addr_pointed1, addr_pointed2);
+
+      pointer_level++;
+      
+      if(addr_pointed1 > std_heap && (char *)addr_pointed1 < (char*) std_heap + STD_HEAP_SIZE && addr_pointed2 > std_heap && (char *)addr_pointed2 < (char*) std_heap + STD_HEAP_SIZE){
+        return compare_heap_area(addr_pointed1, addr_pointed2, NULL, types, other_types, type->dw_type_id, pointer_level); 
+      }else if(addr_pointed1 > start_data && (char*)addr_pointed1 <= (char *)start_data + region_size && addr_pointed2 > start_data && (char*)addr_pointed2 <= (char *)start_data + region_size){
+        if(type->dw_type_id == NULL)
+          return  (addr_pointed1 != addr_pointed2);
+        else
+          return compare_areas_with_type(addr_pointed1, addr_pointed2, types, other_types, type->dw_type_id, region_size, region_type, start_data, pointer_level); 
+      }else{
+        return  (addr_pointed1 != addr_pointed2);
       }
-      i++;
     }
+    break;
+  case e_dw_structure_type:
+    xbt_dynar_foreach(type->members, cursor, member){
+      res = compare_areas_with_type((char *)area1 + member->offset, (char *)area2 + member->offset, types, other_types, member->dw_type_id, region_size, region_type, start_data, pointer_level);
+      if(res == 1)
+        return res;
+    }
+    break;
+  case e_dw_subroutine_type:
+    return -1;
+    break;
+  default:
+    XBT_VERB("Unknown case : %d", type->type);
+    break;
+  }
+  
+  return 0;
+}
+
+static int compare_global_variables(int region_type, mc_mem_region_t r1, mc_mem_region_t r2){
+
+  if(!compared_pointers){
+    compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), NULL);
+    MC_ignore_global_variable("compared_pointers", 1);
+  }else{
+    xbt_dynar_reset(compared_pointers);
   }
 
+  xbt_dynar_t variables;
+  xbt_dict_t types, other_types;
+  int res;
+  unsigned int cursor = 0;
+  dw_variable_t current_var;
+  size_t offset;
+  void *start_data;
+
+  if(region_type == 2){
+    variables = mc_global_variables_binary;
+    types = mc_variables_type_binary;
+    other_types = mc_variables_type_libsimgrid;
+    start_data = start_data_binary;
+  }else{
+    variables = mc_global_variables_libsimgrid;
+    types = mc_variables_type_libsimgrid;
+    other_types = mc_variables_type_binary;
+    start_data = start_data_libsimgrid;
+  }
+
+  xbt_dynar_foreach(variables, cursor, current_var){
+
+    if(region_type == 2)
+      offset = (char *)current_var->address.address - (char *)start_data_binary;
+    else
+      offset = (char *)current_var->address.address - (char *)start_data_libsimgrid;
+
+    res = compare_areas_with_type((char *)r1->data + offset, (char *)r2->data + offset, types, other_types, current_var->type_origin, r1->size, region_type, start_data, 0);
+    if(res == -1){
+      xbt_dynar_cursor_rm(variables, &cursor);
+    }else if(res == 1){
+      XBT_VERB("Global variable %s is different between snapshots", current_var->name);
+      return 1;
+    }
+
+  }
   return 0;
+
+}
+
+static int compare_local_variables(mc_snapshot_stack_t stack1, mc_snapshot_stack_t stack2, void *heap1, void *heap2){
+
+  if(!compared_pointers){
+    compared_pointers = xbt_dynar_new(sizeof(pointers_pair_t), NULL);
+    MC_ignore_global_variable("compared_pointers", 1);
+  }else{
+    xbt_dynar_reset(compared_pointers);
+  }
+
+  if(xbt_dynar_length(stack1->local_variables) != xbt_dynar_length(stack2->local_variables)){
+    XBT_VERB("Different number of local variables");
+    return 1;
+  }else{
+    unsigned int cursor = 0;
+    local_variable_t current_var1, current_var2;
+    int offset1, offset2, res;
+    while(cursor < xbt_dynar_length(stack1->local_variables)){
+      current_var1 = (local_variable_t)xbt_dynar_get_as(stack1->local_variables, cursor, local_variable_t);
+      current_var2 = (local_variable_t)xbt_dynar_get_as(stack2->local_variables, cursor, local_variable_t);
+      if(strcmp(current_var1->name, current_var2->name) != 0 || strcmp(current_var1->frame, current_var2->frame) != 0 || current_var1->ip != current_var2->ip)
+        return 1;
+      offset1 = (char *)current_var1->address - (char *)std_heap;
+      offset2 = (char *)current_var2->address - (char *)std_heap;
+      if(current_var1->region == 1)
+        res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_variables_type_libsimgrid, mc_variables_type_binary, current_var1->type, 0, 1, start_data_libsimgrid, 0l);
+      else
+        res = compare_areas_with_type( (char *)heap1 + offset1, (char *)heap2 + offset2, mc_variables_type_binary, mc_variables_type_libsimgrid, current_var1->type, 0, 2, start_data_binary, 0l);
+      if(res != 0){
+        XBT_VERB("Local variable %s in frame %s  is different between snapshots", current_var1->name, current_var1->frame);
+        return res;
+      }
+      cursor++;
+    }
+    return 0;
+  }
 }
 
+
 static int heap_region_compare(void *d1, void *d2, size_t size){
   
   size_t i = 0;
@@ -149,14 +331,6 @@ void stack_region_free_voidp(void *s){
   stack_region_free((stack_region_t) * (void **) s);
 }
 
-static void heap_equality_free(heap_equality_t e){
-  xbt_free(e);
-}
-
-void heap_equality_free_voidp(void *e){
-  heap_equality_free((heap_equality_t) * (void **) e);
-}
-
 int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall,
                                    mc_snapshot_t s1, mc_snapshot_t s2){
   return snapshot_compare(s1, s2);
@@ -283,17 +457,63 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   /* Init heap information used in heap comparison algorithm */
   init_heap_information((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data, s1->to_ignore, s2->to_ignore);
 
+  /* Stacks comparison */
+  unsigned int  cursor = 0;
+  int diff_local = 0;
+  is_diff = 0;
+  mc_snapshot_stack_t stack1, stack2;
+    
+  while(cursor < xbt_dynar_length(s1->stacks)){
+    stack1 = (mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t);
+    stack2 = (mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t);
+    diff_local = compare_local_variables(stack1, stack2, s1->regions[0]->data, s2->regions[0]->data);
+    if(diff_local > 0){
+      #ifdef MC_DEBUG
+        if(is_diff == 0){
+          xbt_os_walltimer_stop(timer);
+          mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer);
+        }
+        XBT_DEBUG("Different local variables between stacks %d", cursor + 1);
+        errors++;
+        is_diff = 1;
+      #else
+        
+        #ifdef MC_VERBOSE
+          XBT_VERB("Different local variables between stacks %d", cursor + 1);
+        #endif
+          
+        reset_heap_information();
+        xbt_os_timer_free(timer);
+        xbt_os_walltimer_stop(global_timer);
+        mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
+        xbt_os_timer_free(global_timer);
+        
+        if(!raw_mem)
+          MC_UNSET_RAW_MEM;
+        
+        return 1;
+      #endif
+    }
+    cursor++;
+  }
+
+  #ifdef MC_DEBUG
+    if(is_diff == 0)
+      xbt_os_walltimer_stop(timer);
+    xbt_os_walltimer_start(timer);
+  #endif
+
   /* Compare binary global variables */
-  is_diff = compare_global_variables(2, s1->regions[2]->data, s2->regions[2]->data);
+  is_diff = compare_global_variables(2, s1->regions[2], s2->regions[2]);
   if(is_diff != 0){
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
       mc_comp_times->binary_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
-      XBT_DEBUG("Different global variables in binary"); 
-      errors++; 
+      XBT_DEBUG("Different global variables in binary");
+      errors++;
     #else
       #ifdef MC_VERBOSE
-        XBT_VERB("Different global variables in binary"); 
+        XBT_VERB("Different global variables in binary");
       #endif
 
       reset_heap_information();
@@ -316,16 +536,16 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   #endif
 
   /* Compare libsimgrid global variables */
-  is_diff = compare_global_variables(1, s1->regions[1]->data, s2->regions[1]->data);
+  is_diff = compare_global_variables(1, s1->regions[1], s2->regions[1]);
   if(is_diff != 0){
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
-      mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer); 
-      XBT_DEBUG("Different global variables in libsimgrid"); 
-      errors++; 
+      mc_comp_times->libsimgrid_global_variables_comparison_time = xbt_os_timer_elapsed(timer);
+      XBT_DEBUG("Different global variables in libsimgrid");
+      errors++;
     #else
       #ifdef MC_VERBOSE
-        XBT_VERB("Different global variables in libsimgrid"); 
+        XBT_VERB("Different global variables in libsimgrid");
       #endif
         
       reset_heap_information();
@@ -339,49 +559,6 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
 
       return 1;
     #endif
-  }  
-
-  #ifdef MC_DEBUG
-    if(is_diff == 0)
-      xbt_os_walltimer_stop(timer);
-    xbt_os_walltimer_start(timer);
-  #endif
-
-  /* Stacks comparison */
-  unsigned int  cursor = 0;
-  int diff_local = 0;
-  is_diff = 0;
-    
-  while(cursor < xbt_dynar_length(s1->stacks)){
-    diff_local = compare_local_variables(((mc_snapshot_stack_t)xbt_dynar_get_as(s1->stacks, cursor, mc_snapshot_stack_t))->local_variables->data, ((mc_snapshot_stack_t)xbt_dynar_get_as(s2->stacks, cursor, mc_snapshot_stack_t))->local_variables->data);
-    if(diff_local > 0){
-      #ifdef MC_DEBUG
-        if(is_diff == 0){
-          xbt_os_walltimer_stop(timer);
-          mc_comp_times->stacks_comparison_time = xbt_os_timer_elapsed(timer); 
-        }
-        XBT_DEBUG("Different local variables between stacks %d", cursor + 1);
-        errors++;
-        is_diff = 1;
-      #else
-        
-        #ifdef MC_VERBOSE
-          XBT_VERB("Different local variables between stacks %d", cursor + 1);
-        #endif
-          
-        reset_heap_information();
-        xbt_os_timer_free(timer);
-        xbt_os_walltimer_stop(global_timer);
-        mc_snapshot_comparison_time = xbt_os_timer_elapsed(global_timer);
-        xbt_os_timer_free(global_timer);
-        
-        if(!raw_mem)
-          MC_UNSET_RAW_MEM;
-        
-        return 1;
-      #endif
-    }
-    cursor++;
   }
     
   #ifdef MC_DEBUG
@@ -389,7 +566,7 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   #endif
 
   /* Compare heap */
-  if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data)){
+  if(mmalloc_compare_heap((xbt_mheap_t)s1->regions[0]->data, (xbt_mheap_t)s2->regions[0]->data) > 0){
 
     #ifdef MC_DEBUG
       xbt_os_walltimer_stop(timer);
@@ -442,158 +619,9 @@ int snapshot_compare(mc_snapshot_t s1, mc_snapshot_t s2){
   
 }
 
-int is_stack_ignore_variable(char *frame, char *var_name){
-
-  unsigned int cursor = 0;
-  int start = 0;
-  int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
-  mc_stack_ignore_variable_t current_var;
-
-  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 || strcmp(current_var->frame, "*") == 0){
-      if(strcmp(current_var->var_name, var_name) == 0)
-        return 1;
-      if(strcmp(current_var->var_name, var_name) < 0)
-        start = cursor + 1;
-      if(strcmp(current_var->var_name, var_name) > 0)
-        end = cursor - 1;
-    }else if(strcmp(current_var->frame, frame) < 0){
-      start = cursor + 1;
-    }else if(strcmp(current_var->frame, frame) > 0){
-      end = cursor - 1; 
-    }
-  }
-
-  return 0;
-}
-
-static int compare_local_variables(char *s1, char *s2){
-  
-  xbt_dynar_t tokens1 = xbt_str_split(s1, NULL);
-  xbt_dynar_t tokens2 = xbt_str_split(s2, NULL);
-
-  xbt_dynar_t s_tokens1, s_tokens2;
-  unsigned int cursor = 0;
-  void *addr1, *addr2;
-  char *frame_name1 = NULL, *frame_name2 = NULL;
-  int res_compare = 0;
-
-  #if defined MC_VERBOSE || defined MC_DEBUG
-    char *var_name;
-  #endif
-
-  while(cursor < xbt_dynar_length(tokens1)){
-    s_tokens1 = xbt_str_split(xbt_dynar_get_as(tokens1, cursor, char *), "=");
-    s_tokens2 = xbt_str_split(xbt_dynar_get_as(tokens2, cursor, char *), "=");
-    if(xbt_dynar_length(s_tokens1) > 1 && xbt_dynar_length(s_tokens2) > 1){
-      #if defined MC_VERBOSE || defined MC_DEBUG
-        var_name = xbt_dynar_get_as(s_tokens1, 0, char *);
-      #endif
-      if((strcmp(xbt_dynar_get_as(s_tokens1, 0, char *), "frame_name") == 0) && (strcmp(xbt_dynar_get_as(s_tokens2, 0, char *), "frame_name") == 0)){
-        xbt_free(frame_name1);
-        xbt_free(frame_name2);
-        frame_name1 = strdup(xbt_dynar_get_as(s_tokens1, 1, char *));
-        frame_name2 = strdup(xbt_dynar_get_as(s_tokens2, 1, char *));
-      }
-      addr1 = (void *) strtoul(xbt_dynar_get_as(s_tokens1, 1, char *), NULL, 16);
-      addr2 = (void *) strtoul(xbt_dynar_get_as(s_tokens2, 1, char *), NULL, 16);
-      if(addr1 > std_heap && (char *)addr1 <= (char *)std_heap + STD_HEAP_SIZE && addr2 > std_heap && (char *)addr2 <= (char *)std_heap + STD_HEAP_SIZE){
-        res_compare = compare_area(addr1, addr2, NULL);
-        if(res_compare == 1){
-          if(is_stack_ignore_variable(frame_name1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(frame_name2, xbt_dynar_get_as(s_tokens2, 0, char *))){
-            xbt_dynar_free(&s_tokens1);
-            xbt_dynar_free(&s_tokens2);
-            cursor++;
-            continue;
-          }else {
-            #ifdef MC_VERBOSE
-              XBT_VERB("Different local variable : %s at addresses %p - %p in frame %s", var_name, addr1, addr2, frame_name1);
-            #endif
-            #ifdef MC_DEBUG
-              XBT_DEBUG("Different local variable : %s at addresses %p - %p", var_name, addr1, addr2);
-            #endif
-            xbt_dynar_free(&s_tokens1);
-            xbt_dynar_free(&s_tokens2);
-            xbt_dynar_free(&tokens1);
-            xbt_dynar_free(&tokens2);
-            xbt_free(frame_name1);
-            xbt_free(frame_name2);
-            return 1;
-          }
-        }
-      }else{
-        if(strcmp(xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *)) != 0){
-          if(is_stack_ignore_variable(frame_name1, xbt_dynar_get_as(s_tokens1, 0, char *)) && is_stack_ignore_variable(frame_name2, xbt_dynar_get_as(s_tokens2, 0, char *))){
-            xbt_dynar_free(&s_tokens1);
-            xbt_dynar_free(&s_tokens2);
-            cursor++;
-            continue;
-          }else {
-            #ifdef MC_VERBOSE
-              XBT_VERB("Different local variable : %s (%s - %s) in frame %s", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *), frame_name1);
-            #endif
-            #ifdef MC_DEBUG
-              XBT_DEBUG("Different local variable : %s (%s - %s)", var_name, xbt_dynar_get_as(s_tokens1, 1, char *), xbt_dynar_get_as(s_tokens2, 1, char *));
-            #endif
-
-            xbt_dynar_free(&s_tokens1);
-            xbt_dynar_free(&s_tokens2);
-            xbt_dynar_free(&tokens1);
-            xbt_dynar_free(&tokens2);
-            xbt_free(frame_name1);
-            xbt_free(frame_name2);
-            return 1;
-          }
-        }
-      }
-    }
-    xbt_dynar_free(&s_tokens1);
-    xbt_dynar_free(&s_tokens2);
-         
-    cursor++;
-  }
-
-  xbt_free(frame_name1);
-  xbt_free(frame_name2);
-  xbt_dynar_free(&tokens1);
-  xbt_dynar_free(&tokens2);
-  return 0;
-  
-}
-
-static int is_heap_equality(xbt_dynar_t equals, void *a1, void *a2){
-
-  unsigned int cursor = 0;
-  int start = 0;
-  int end = xbt_dynar_length(equals) - 1;
-  heap_equality_t current_equality;
-
-  while(start <= end){
-    cursor = (start + end) / 2;
-    current_equality = (heap_equality_t)xbt_dynar_get_as(equals, cursor, heap_equality_t);
-    if(current_equality->address1 == a1){
-      if(current_equality->address2 == a2)
-        return 1;
-      if(current_equality->address2 < a2)
-        start = cursor + 1;
-      if(current_equality->address2 > a2)
-        end = cursor - 1;
-    }
-    if(current_equality->address1 < a1)
-      start = cursor + 1;
-    if(current_equality->address1 > a1)
-      end = cursor - 1; 
-  }
-
-  return 0;
-
-}
-
 int MC_compare_snapshots(void *s1, void *s2){
   
-  MC_ignore_stack("self", "simcall_BODY_mc_snapshot");
+  MC_ignore_local_variable("self", "simcall_BODY_mc_snapshot", 1);
  
   return simcall_mc_compare_snapshots(s1, s2);
 
index 7469068..ab6b9bc 100644 (file)
@@ -89,7 +89,6 @@ void _mc_cfg_cb_dot_output(const char *name, int pos) {
 }
 
 /* MC global data structures */
-
 mc_state_t mc_current_state = NULL;
 char mc_replay_mode = FALSE;
 double *mc_time = NULL;
@@ -98,20 +97,23 @@ double mc_snapshot_comparison_time;
 mc_stats_t mc_stats = NULL;
 
 /* Safety */
-
 xbt_fifo_t mc_stack_safety = NULL;
 mc_global_t initial_state_safety = NULL;
 
 /* Liveness */
-
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_global_t initial_state_liveness = NULL;
 int compare;
 
-/* Local */
-xbt_dict_t mc_local_variables = NULL;
-/* Global */
-xbt_dynar_t mc_global_variables = NULL;
+xbt_automaton_t _mc_property_automaton = NULL;
+
+/* Variables */
+xbt_dict_t mc_local_variables_libsimgrid = NULL;
+xbt_dict_t mc_local_variables_binary = NULL;
+xbt_dynar_t mc_global_variables_libsimgrid = NULL;
+xbt_dynar_t mc_global_variables_binary = NULL;
+xbt_dict_t mc_variables_type_libsimgrid = NULL;
+xbt_dict_t mc_variables_type_binary = NULL;
 
 /* Ignore mechanism */
 xbt_dynar_t mc_stack_comparison_ignore;
@@ -119,763 +121,1174 @@ xbt_dynar_t mc_data_bss_comparison_ignore;
 extern xbt_dynar_t mc_heap_comparison_ignore;
 extern xbt_dynar_t stacks_areas;
 
+/* Dot output */
 FILE *dot_output = NULL;
 const char* colors[13];
 
-xbt_automaton_t _mc_property_automaton = NULL;
-
-/* Static functions */
 
-static void MC_assert_pair(int prop);
-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);
+/*******************************  DWARF Information *******************************/
+/**********************************************************************************/
 
-void MC_do_the_modelcheck_for_real() {
+/************************** Free functions *************************/
 
-  MC_SET_RAW_MEM;
-  mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
-  MC_UNSET_RAW_MEM;
+static void dw_location_free(dw_location_t l){
+  if(l){
+    if(l->type == e_dw_loclist)
+      xbt_dynar_free(&(l->location.loclist));
+    else if(l->type == e_dw_compose)
+      xbt_dynar_free(&(l->location.compose));
+    else if(l->type == e_dw_arithmetic)
+      xbt_free(l->location.arithmetic);
   
-  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;
+    xbt_free(l);
+  }
+}
 
-    XBT_INFO("Check a safety property");
-    MC_modelcheck_safety();
+static void dw_location_entry_free(dw_location_entry_t e){
+  dw_location_free(e->location);
+  xbt_free(e);
+}
 
-  } else  {
+static void dw_type_free(dw_type_t t){
+  xbt_free(t->name);
+  xbt_free(t->dw_type_id);
+  xbt_dynar_free(&(t->members));
+  xbt_free(t);
+}
 
-    if (mc_reduce_kind==e_mc_reduce_unset)
-      mc_reduce_kind=e_mc_reduce_none;
+static void dw_type_free_voidp(void *t){
+  dw_type_free((dw_type_t) * (void **) t);
+}
 
-    XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
-    MC_automaton_load(_sg_mc_property_file);
-    MC_modelcheck_liveness();
+static void dw_variable_free(dw_variable_t v){
+  if(v){
+    xbt_free(v->name);
+    xbt_free(v->type_origin);
+    if(!v->global)
+      dw_location_free(v->address.location);
+    xbt_free(v);
   }
 }
 
-
-void MC_compare(void){
-  compare = 1;
+static void dw_variable_free_voidp(void *t){
+  dw_variable_free((dw_variable_t) * (void **) t);
 }
 
-void MC_init(){
-
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
-  
-  compare = 0;
-
-  /* Initialize the data structures that must be persistent across every
-     iteration of the model-checker (in RAW memory) */
+/*************************************************************************/
 
-  MC_SET_RAW_MEM;
+static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
 
-  MC_init_memory_map_info();
-  
-  mc_local_variables = xbt_dict_new_homogeneous(NULL);
+  dw_location_t loc = xbt_new0(s_dw_location_t, 1);
 
-  /* Get local variables in binary for state equality detection */
-  xbt_dict_t binary_location_list = MC_get_location_list(xbt_binary_name);
-  MC_get_local_variables(xbt_binary_name, binary_location_list, &mc_local_variables);
+  if(location_list != NULL){
+    
+    char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
+    loc->type = e_dw_loclist;
+    loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
+    if(loc->location.loclist == NULL)
+      XBT_INFO("Key not found in loclist");
+    xbt_free(key);
+    return loc;
 
-  /* Get local variables in libsimgrid for state equality detection */
-  xbt_dict_t libsimgrid_location_list = MC_get_location_list(libsimgrid_path);
-  MC_get_local_variables(libsimgrid_path, libsimgrid_location_list, &mc_local_variables);
+  }else{
 
-  xbt_dict_free(&libsimgrid_location_list);
-  xbt_dict_free(&binary_location_list);
-  
-  /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
-  get_libsimgrid_plt_section();
-  get_binary_plt_section();
+    int cursor = 0;
+    char *tok = NULL, *tok2 = NULL; 
+    
+    xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
+    xbt_dynar_t tokens2;
 
-  /* Get global variables */
-  MC_get_global_variables(xbt_binary_name);
-  MC_get_global_variables(libsimgrid_path);
+    loc->type = e_dw_compose;
+    loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
 
-  MC_UNSET_RAW_MEM;
+    while(cursor < xbt_dynar_length(tokens1)){
 
-   /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
-  MC_ignore_stack("e", "*");
-  MC_ignore_stack("__ex_cleanup", "*");
-  MC_ignore_stack("__ex_mctx_en", "*");
-  MC_ignore_stack("__ex_mctx_me", "*");
-  MC_ignore_stack("__xbt_ex_ctx_ptr", "*");
-  MC_ignore_stack("_log_ev", "*");
-  MC_ignore_stack("_throw_ctx", "*");
-  MC_ignore_stack("ctx", "*");
-
-  MC_ignore_stack("next_context", "smx_ctx_sysv_suspend_serial");
-  MC_ignore_stack("i", "smx_ctx_sysv_suspend_serial");
+      tok = xbt_dynar_get_as(tokens1, cursor, char*);
+      tokens2 = xbt_str_split(tok, " ");
+      tok2 = xbt_dynar_get_as(tokens2, 0, char*);
+      
+      if(strncmp(tok2, "DW_OP_reg", 9) == 0){
+        dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
+        new_element->type = e_dw_register;
+        new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
+        xbt_dynar_push(loc->location.compose, &new_element);     
+      }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, 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, 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);
+        new_element->type = e_dw_lit;
+        new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }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, xbt_dynar_length(tokens2) - 1, char*));
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }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, 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 ||
+               strcmp(tok, "DW_OP_div") == 0 ||
+               strcmp(tok, "DW_OP_minus") == 0 ||
+               strcmp(tok, "DW_OP_mod") == 0 ||
+               strcmp(tok, "DW_OP_mul") == 0 ||
+               strcmp(tok, "DW_OP_neg") == 0 ||
+               strcmp(tok, "DW_OP_not") == 0 ||
+               strcmp(tok, "DW_OP_or") == 0 ||
+               strcmp(tok, "DW_OP_plus") == 0){               
+        dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
+        new_element->type = e_dw_arithmetic;
+        new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }else if(strcmp(tok, "DW_OP_stack_value") == 0){
+      }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, xbt_dynar_length(tokens2) - 1, char*));
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }else if(strcmp(tok, "DW_OP_deref") == 0){
+        dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
+        new_element->type = e_dw_deref;
+        new_element->location.deref_size = sizeof(void *);
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }else if(strcmp(tok2, "DW_OP_constu:") == 0){
+        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, xbt_dynar_length(tokens2) - 1, char*)));
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }else if(strcmp(tok2, "DW_OP_consts:") == 0){
+        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, 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 ||
+               strcmp(tok2, "DW_OP_const4u:") == 0 ||
+               strcmp(tok2, "DW_OP_const8u:") == 0){
+        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, xbt_dynar_length(tokens2) - 1, char*)));
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
+               strcmp(tok, "DW_OP_const2s") == 0 ||
+               strcmp(tok, "DW_OP_const4s") == 0 ||
+               strcmp(tok, "DW_OP_const8s") == 0){
+        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, 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);
+        new_element->type = e_dw_unsupported;
+        xbt_dynar_push(loc->location.compose, &new_element);
+      }
 
-  /* Ignore local variable about time used for tracing */
-  MC_ignore_stack("start_time", "*"); 
+      cursor++;
+      xbt_dynar_free(&tokens2);
 
-  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));
+    }
+    
+    xbt_dynar_free(&tokens1);
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+    return loc;
+    
+  }
 
 }
 
-void MC_init_dot_output(){ /* FIXME : more colors */
+static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
 
-  colors[0] = "blue";
-  colors[1] = "red";
-  colors[2] = "green3";
-  colors[3] = "goldenrod";
-  colors[4] = "brown";
-  colors[5] = "purple";
-  colors[6] = "magenta";
-  colors[7] = "turquoise4";
-  colors[8] = "gray25";
-  colors[9] = "forestgreen";
-  colors[10] = "hotpink";
-  colors[11] = "lightblue";
-  colors[12] = "tan";
+  char *command = bprintf("objdump -Wo %s", elf_file);
 
-  dot_output = fopen(_sg_mc_dot_output_file, "w");
-  
-  if(dot_output == NULL){
-    perror("Error open dot output file");
+  FILE *fp = popen(command, "r");
+
+  if(fp == NULL){
+    perror("popen for objdump failed");
     xbt_abort();
   }
 
-  fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
+  int debug = 0; /*Detect if the program has been compiled with -g */
 
-}
+  xbt_dict_t location_list = xbt_dict_new_homogeneous(NULL);
+  char *line = NULL, *loc_expr = NULL;
+  ssize_t read;
+  size_t n = 0;
+  int cursor_remove;
+  xbt_dynar_t split = NULL;
 
-void MC_modelcheck_safety(void)
-{
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  while ((read = xbt_getline(&line, &n, fp)) != -1) {
 
-  /* Check if MC is already initialized */
-  if (initial_state_safety)
-    return;
+    /* Wipeout the new line character */
+    line[read - 1] = '\0';
 
-  mc_time = xbt_new0(double, simix_process_maxpid);
+    xbt_str_trim(line, NULL);
+    
+    if(n == 0)
+      continue;
 
-  /* mc_time refers to clock for each process -> ignore it for heap comparison */  
-  MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
+    if(strlen(line) == 0)
+      continue;
 
-  /* Initialize the data structures that must be persistent across every
-     iteration of the model-checker (in RAW memory) */
-  
-  MC_SET_RAW_MEM;
+    if(debug == 0){
 
-  /* Initialize statistics */
-  mc_stats = xbt_new0(s_mc_stats_t, 1);
-  mc_stats->state_size = 1;
+      if(strncmp(line, elf_file, strlen(elf_file)) == 0)
+        continue;
+      
+      if(strncmp(line, "Contents", 8) == 0)
+        continue;
 
-  /* Create exploration stack */
-  mc_stack_safety = xbt_fifo_new();
+      if(strncmp(line, "Offset", 6) == 0){
+        debug = 1;
+        continue;
+      }
+    }
 
-  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
-    MC_init_dot_output();
+    if(debug == 0){
+      XBT_INFO("Your program must be compiled with -g");
+      xbt_abort();
+    }
 
-  MC_UNSET_RAW_MEM;
+    xbt_dynar_t loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
 
-  if(_sg_mc_visited > 0){
-    MC_init();
-  }else{
-    MC_SET_RAW_MEM;
-    MC_init_memory_map_info();
-    get_libsimgrid_plt_section();
-    get_binary_plt_section();
-    MC_UNSET_RAW_MEM;
-  }
-
-  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_UNSET_RAW_MEM;
+    xbt_str_strip_spaces(line);
+    split = xbt_str_split(line, " ");
 
-  MC_dpor();
+    while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
+      
+      dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
+      new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
+      new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
+      
+      cursor_remove =0;
+      while(cursor_remove < 3){
+        xbt_dynar_remove_at(split, 0, NULL);
+        cursor_remove++;
+      }
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+      loc_expr = xbt_str_join(split, " ");
+      xbt_str_ltrim(loc_expr, "(");
+      xbt_str_rtrim(loc_expr, ")");
+      new_entry->location = MC_dwarf_get_location(NULL, loc_expr);
 
-  MC_exit();
-}
+      xbt_dynar_push(loclist, &new_entry);
 
-void MC_modelcheck_liveness(){
+      xbt_dynar_free(&split);
+      free(loc_expr);
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+      read = xbt_getline(&line, &n, fp);
+      if(read != -1){
+        line[read - 1] = '\0';
+        xbt_str_strip_spaces(line);
+        split = xbt_str_split(line, " ");
+      }
 
-  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 = xbt_new0(s_mc_stats_t, 1);
-  mc_stats->state_size = 1;
+    char *key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
+    xbt_dict_set(location_list, key, loclist, NULL);
+    xbt_free(key);
+    
+    xbt_dynar_free(&split);
 
-  /* Create exploration stack */
-  mc_stack_liveness = xbt_fifo_new();
+  }
 
-  /* Create the initial state */
-  initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+  xbt_free(line);
+  xbt_free(command);
+  pclose(fp);
 
-  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
-    MC_init_dot_output();
-  
-  MC_UNSET_RAW_MEM;
+  return location_list;
+}
 
-  MC_ddfs_init();
+static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
 
-  /* We're done */
-  MC_print_statistics(mc_stats);
-  xbt_free(mc_time);
+  xbt_dict_cursor_t cursor = NULL;
+  char *name;
+  dw_frame_t res;
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+  xbt_dict_foreach(all_variables, cursor, name, res) {
+    if(offset >= res->start && offset < res->end){
+      xbt_dict_cursor_free(&cursor);
+      return res;
+    }
+  }
 
+  xbt_dict_cursor_free(&cursor);
+  return NULL;
+  
 }
 
+static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
 
-void MC_exit(void)
-{
-  xbt_free(mc_time);
-  MC_memory_exit();
-  xbt_abort();
-}
+  unsigned int cursor = 0;
+  dw_variable_t current_var;
 
-int SIMIX_pre_mc_random(smx_simcall_t simcall){
+  xbt_dynar_foreach(frame->variables, cursor, current_var){
+    if(strcmp(var, current_var->name) == 0)
+      return current_var;
+  }
 
-  return simcall->mc_value;
+  return NULL;
 }
 
+static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
 
-int MC_random(void)
-{
-  /*FIXME: return mc_current_state->executed_transition->random.value;*/
-  return simcall_mc_random();
-}
-
-/**
- * \brief Schedules all the process that are ready to run
- */
-void MC_wait_for_requests(void)
-{
-  smx_process_t process;
-  smx_simcall_t req;
-  unsigned int iter;
+  if(xbt_dynar_is_empty(variables))
+    return 0;
 
-  while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
-    SIMIX_process_runall();
-    xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
-      req = &process->simcall;
-      if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
-        SIMIX_simcall_pre(req, 0);
-    }
-  }
-}
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(variables) - 1;
+  dw_variable_t var_test = NULL;
 
-int MC_deadlock_check()
-{
-  int deadlock = FALSE;
-  smx_process_t process;
-  if(xbt_swag_size(simix_global->process_list)){
-    deadlock = TRUE;
-    xbt_swag_foreach(process, simix_global->process_list){
-      if(process->simcall.call != SIMCALL_NONE
-         && MC_request_is_enabled(&process->simcall)){
-        deadlock = FALSE;
-        break;
+  while(start <= end){
+    cursor = (start + end) / 2;
+    var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
+    if(strcmp(var_test->name, var) < 0){
+      start = cursor + 1;
+    }else if(strcmp(var_test->name, var) > 0){
+      end = cursor - 1;
+    }else{
+      if(address){ /* global variable */
+        if(var_test->address.address == address)
+          return -1;
+        if(var_test->address.address > address)
+          end = cursor - 1;
+        else
+          start = cursor + 1;
+      }else{ /* local variable */
+        return -1;
       }
     }
   }
-  return deadlock;
-}
 
-/**
- * \brief Re-executes from the state at position start all the transitions indicated by
- *        a given model-checker stack.
- * \param stack The stack with the transitions to execute.
- * \param start Start index to begin the re-execution.
- */
-void MC_replay(xbt_fifo_t stack, int start)
-{
-  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
-
-  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;
+  if(strcmp(var_test->name, var) == 0){
+    if(address && var_test->address.address < address)
+      return cursor+1;
+    else
+      return cursor;
+  }else if(strcmp(var_test->name, var) < 0)
+    return cursor+1;
+  else
+    return cursor;
 
-  XBT_DEBUG("**** Begin Replay ****");
+}
 
-  if(start == -1){
-    /* Restore the initial state */
-    MC_restore_snapshot(initial_state_safety->snapshot);
-    /* At the moment of taking the snapshot the raw heap was set, so restoring
-     * it will set it back again, we have to unset it to continue  */
-    MC_UNSET_RAW_MEM;
-  }
 
-  start_item = xbt_fifo_get_last_item(stack);
-  if(start != -1){
-    while (i != start){
-      start_item = xbt_fifo_get_prev_item(start_item);
-      i++;
-    }
-  }
+static void MC_dwarf_get_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *local_variables, xbt_dynar_t *global_variables, xbt_dict_t *types){
 
-  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;
+  char *command = bprintf("objdump -Wi %s", elf_file);
   
+  FILE *fp = popen(command, "r");
 
-  /* 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);
-       item = xbt_fifo_get_prev_item(item)) {
-
-    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 */
-      req = &saved_req->issuer->simcall;
+  if(fp == NULL)
+    perror("popen for objdump failed");
 
-      /* Debug information */
-      if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
-        req_str = MC_request_to_string(req, value);
-        XBT_DEBUG("Replay: %s (%p)", req_str, state);
-        xbt_free(req_str);
-      }
-    }
-    
-    SIMIX_simcall_pre(req, value);
-    MC_wait_for_requests();
+  char *line = NULL, *origin, *abstract_origin, *current_frame = NULL, 
+    *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
+    *node_type = NULL, *location_type = NULL, *variable_name = NULL, 
+    *loc_expr = NULL, *name = NULL, *end =NULL, *type_origin = NULL, *global_address = NULL, 
+    *parent_value = NULL;
 
-    count++;
+  ssize_t read =0;
+  size_t n = 0;
+  int global_variable = 0, parent = 0, new_frame = 0, new_variable = 1, size = 0, 
+    is_pointer = 0, struct_decl = 0, member_end = 0,
+    enumeration_size = 0, subrange = 0, union_decl = 0, offset = 0, index = 0;
+  
+  xbt_dynar_t split = NULL, split2 = NULL;
 
-    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_dict_t variables_origin = xbt_dict_new_homogeneous(xbt_free);
+  xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(xbt_free);
 
-  }
+  dw_frame_t variable_frame, subroutine_frame = NULL;
 
-  XBT_DEBUG("**** End Replay ****");
+  e_dw_type_type type_type = -1;
 
-  if(raw_mem)
-    MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
-  
+  read = xbt_getline(&line, &n, fp);
 
-}
+  while (read != -1) {
 
-void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
-{
+    /* Wipeout the new line character */
+    line[read - 1] = '\0';
+  
+    if(n == 0 || strlen(line) == 0){
+      read = xbt_getline(&line, &n, fp);
+      continue;
+    }
 
-  initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+    xbt_str_ltrim(line, NULL);
+    xbt_str_strip_spaces(line);
+    
+    if(line[0] != '<'){
+      read = xbt_getline(&line, &n, fp);
+      continue;
+    }
+    
+    xbt_dynar_free(&split);
+    split = xbt_str_split(line, " ");
 
-  int value;
-  char *req_str;
-  smx_simcall_t req = NULL, saved_req = NULL;
-  xbt_fifo_item_t item;
-  mc_state_t state;
-  mc_pair_t pair;
-  int depth = 1;
+    /* Get node type */
+    node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 
-  XBT_DEBUG("**** Begin Replay ****");
+    if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
 
-  /* Restore the initial state */
-  MC_restore_snapshot(initial_state_liveness->snapshot);
+      dw_frame_t frame = NULL;
 
-  /* At the moment of taking the snapshot the raw heap was set, so restoring
-   * it will set it back again, we have to unset it to continue  */
-  if(!initial_state_liveness->raw_mem_set)
-    MC_UNSET_RAW_MEM;
+      strtok(xbt_dynar_get_as(split, 0, char *), "<");
+      subprogram_start = xbt_strdup(strtok(NULL, "<"));
+      xbt_str_rtrim(subprogram_start, ">:");
 
-  if(all_stack){
+      read = xbt_getline(&line, &n, fp);
+   
+      while(read != -1){
 
-    item = xbt_fifo_get_last_item(stack);
+        /* Wipeout the new line character */
+        line[read - 1] = '\0';
 
-    while(depth <= xbt_fifo_size(stack)){
+        if(n == 0 || strlen(line) == 0){
+          read = xbt_getline(&line, &n, fp);
+          continue;
+        }
+        
+        xbt_dynar_free(&split);
+        xbt_str_rtrim(line, NULL);
+        xbt_str_strip_spaces(line);
+        split = xbt_str_split(line, " ");
+          
+        node_type = xbt_dynar_get_as(split, 1, char *);
 
-      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
-      state = (mc_state_t) pair->graph_state;
+        if(strncmp(node_type, "DW_AT_", 6) != 0)
+          break;
 
-      if(pair->requests > 0){
-   
-        saved_req = MC_state_get_executed_request(state, &value);
-        //XBT_DEBUG("SavedReq->call %u", saved_req->call);
-      
-        if(saved_req != NULL){
-          /* 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 */
-          req = &saved_req->issuer->simcall;
-          //XBT_DEBUG("Req->call %u", req->call);
-  
-          /* Debug information */
-          if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
-            req_str = MC_request_to_string(req, value);
-            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-            xbt_free(req_str);
-          }
-  
-        }
-        SIMIX_simcall_pre(req, value);
-        MC_wait_for_requests();
-      }
+        if(strcmp(node_type, "DW_AT_sibling") == 0){
 
-      depth++;
-    
-      /* Update statistics */
-      mc_stats->visited_pairs++;
-      mc_stats->executed_transitions++;
+          subprogram_end = xbt_strdup(xbt_dynar_get_as(split, 3, char*));
+          xbt_str_ltrim(subprogram_end, "<0x");
+          xbt_str_rtrim(subprogram_end, ">");
+          
+        }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
+          
+          new_frame = 0;
+          abstract_origin = xbt_strdup(xbt_dynar_get_as(split, 2, char*));
+          xbt_str_ltrim(abstract_origin, "<0x");
+          xbt_str_rtrim(abstract_origin, ">");
+          subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
+          frame = xbt_dict_get_or_null(*local_variables, subprogram_name); 
+          xbt_free(abstract_origin);
 
-      item = xbt_fifo_get_prev_item(item);
-    }
+        }else if(strcmp(node_type, "DW_AT_name") == 0){
 
-  }else{
+          new_frame = 1;
+          xbt_free(current_frame);
+          frame = xbt_new0(s_dw_frame_t, 1);
+          frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *)); 
+          frame->variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
+          frame->frame_base = xbt_new0(s_dw_location_t, 1); 
+          current_frame = strdup(frame->name);
 
-    /* Traverse the stack from the initial state and re-execute the transitions */
-    for (item = xbt_fifo_get_last_item(stack);
-         item != xbt_fifo_get_first_item(stack);
-         item = xbt_fifo_get_prev_item(item)) {
+          xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
+        
+        }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
 
-      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
-      state = (mc_state_t) pair->graph_state;
+          location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
+
+          if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
+
+            frame->frame_base = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
+             
+          }else{
+                
+            xbt_str_strip_spaces(line);
+            split2 = xbt_str_split(line, "(");
+            xbt_dynar_remove_at(split2, 0, NULL);
+            loc_expr = xbt_str_join(split2, " ");
+            xbt_str_rtrim(loc_expr, ")");
+            frame->frame_base = MC_dwarf_get_location(NULL, loc_expr);
+            xbt_dynar_free(&split2);
+            xbt_free(loc_expr);
 
-      if(pair->requests > 0){
-   
-        saved_req = MC_state_get_executed_request(state, &value);
-        //XBT_DEBUG("SavedReq->call %u", saved_req->call);
-      
-        if(saved_req != NULL){
-          /* 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 */
-          req = &saved_req->issuer->simcall;
-          //XBT_DEBUG("Req->call %u", req->call);
-  
-          /* Debug information */
-          if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
-            req_str = MC_request_to_string(req, value);
-            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
-            xbt_free(req_str);
           }
-  
-        }
  
-        SIMIX_simcall_pre(req, value);
-        MC_wait_for_requests();
-      }
+        }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
+          
+          if(frame != NULL)
+            frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 
-      depth++;
-    
-      /* Update statistics */
-      mc_stats->visited_pairs++;
-      mc_stats->executed_transitions++;
-    }
-  }  
+        }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 
-  XBT_DEBUG("**** End Replay ****");
+          if(frame != NULL)
+            frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 
-  if(initial_state_liveness->raw_mem_set)
-    MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
-  
-}
+        }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
 
-/**
- * \brief Dumps the contents of a model-checker's stack and shows the actual
- *        execution trace
- * \param stack The stack to dump
- */
-void MC_dump_stack_safety(xbt_fifo_t stack)
-{
-  
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+          xbt_free(frame->name);
+          xbt_free(current_frame);
+          frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));   
+          current_frame = strdup(frame->name);
+          xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 
-  MC_show_stack_safety(stack);
+        }
 
-  if(!_sg_mc_checkpoint){
+        read = xbt_getline(&line, &n, fp);
 
-    mc_state_t state;
+      }
+      if(new_frame == 1){
+        frame->start = strtoul(subprogram_start, NULL, 16);
+        if(subprogram_end != NULL)
+          frame->end = strtoul(subprogram_end, NULL, 16);
+        xbt_dict_set(*local_variables, frame->name, frame, NULL);
+      }
 
-    MC_SET_RAW_MEM;
-    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
-      MC_state_delete(state);
-    MC_UNSET_RAW_MEM;
+      xbt_free(subprogram_start);
+      xbt_free(subprogram_end);
+      subprogram_end = NULL;
+        
 
-  }
+    }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-  else
-    MC_UNSET_RAW_MEM;
+      dw_variable_t var = NULL;
+      
+      parent_value = strdup(xbt_dynar_get_as(split, 0, char *));
+      parent_value = strtok(parent_value,"<");
+      xbt_str_rtrim(parent_value, ">");
+      parent = atoi(parent_value);
+      xbt_free(parent_value);
+
+      if(parent == 1)
+        global_variable = 1;
+    
+      strtok(xbt_dynar_get_as(split, 0, char *), "<");
+      origin = xbt_strdup(strtok(NULL, "<"));
+      xbt_str_rtrim(origin, ">:");
+      
+      read = xbt_getline(&line, &n, fp);
+      
+      while(read != -1){
+
+        /* Wipeout the new line character */
+        line[read - 1] = '\0'; 
+
+        if(n == 0 || strlen(line) == 0){
+          read = xbt_getline(&line, &n, fp);
+          continue;
+        }
+    
+        xbt_dynar_free(&split);
+        xbt_str_rtrim(line, NULL);
+        xbt_str_strip_spaces(line);
+        split = xbt_str_split(line, " ");
   
-}
+        node_type = xbt_dynar_get_as(split, 1, char *);
 
+        if(strncmp(node_type, "DW_AT_", 6) != 0)
+          break;
 
-void MC_show_stack_safety(xbt_fifo_t stack)
-{
+        if(strcmp(node_type, "DW_AT_name") == 0){
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+          var = xbt_new0(s_dw_variable_t, 1);
+          var->name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
+          xbt_dict_set(variables_origin, origin, xbt_strdup(var->name), NULL);
+         
+        }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 
-  MC_SET_RAW_MEM;
+          new_variable = 0;
 
-  int value;
-  mc_state_t state;
-  xbt_fifo_item_t item;
-  smx_simcall_t req;
-  char *req_str = NULL;
-  
-  for (item = xbt_fifo_get_last_item(stack);
-       (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
-        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
-    req = MC_state_get_executed_request(state, &value);
-    if(req){
-      req_str = MC_request_to_string(req, value);
-      XBT_INFO("%s", req_str);
-      xbt_free(req_str);
-    }
-  }
+          abstract_origin = xbt_dynar_get_as(split, 2, char *);
+          xbt_str_ltrim(abstract_origin, "<0x");
+          xbt_str_rtrim(abstract_origin, ">");
+          
+          variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
+          variable_frame = MC_dwarf_get_frame_by_offset(*local_variables, strtoul(abstract_origin, NULL, 16));
+          var = MC_dwarf_get_variable_by_name(variable_frame, variable_name); 
 
-  if(!raw_mem_set)
-    MC_UNSET_RAW_MEM;
-}
+        }else if(strcmp(node_type, "DW_AT_location") == 0){
 
-void MC_show_deadlock(smx_simcall_t req)
-{
-  /*char *req_str = NULL;*/
-  XBT_INFO("**************************");
-  XBT_INFO("*** DEAD-LOCK DETECTED ***");
-  XBT_INFO("**************************");
-  XBT_INFO("Locked request:");
-  /*req_str = MC_request_to_string(req);
-    XBT_INFO("%s", req_str);
-    xbt_free(req_str);*/
-  XBT_INFO("Counter-example execution trace:");
-  MC_dump_stack_safety(mc_stack_safety);
-  MC_print_statistics(mc_stats);
-}
+          if(var != NULL){
+
+            if(!global_variable){
+
+              location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
+
+              if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
+                var->address.location = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
+              }else{
+                xbt_str_strip_spaces(line);
+                split2 = xbt_str_split(line, "(");
+                xbt_dynar_remove_at(split2, 0, NULL);
+                loc_expr = xbt_str_join(split2, " ");
+                xbt_str_rtrim(loc_expr, ")");
+                if(strncmp("DW_OP_addr", loc_expr, 10) == 0){
+                  global_variable = 1;
+                  xbt_dynar_free(&split2);
+                  split2 = xbt_str_split(loc_expr, " ");
+                  if(strcmp(elf_file, xbt_binary_name) != 0)
+                    var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
+                  else
+                    var->address.address = (void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16);
+                }else{
+                  var->address.location = MC_dwarf_get_location(NULL, loc_expr);
+                }
+                xbt_dynar_free(&split2);
+                xbt_free(loc_expr);
+              }
+            }else{
+              global_address = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
+              xbt_str_rtrim(global_address, ")");
+              if(strcmp(elf_file, xbt_binary_name) != 0)
+                var->address.address = (char *)start_text_libsimgrid + (long)((void *)strtoul(global_address, NULL, 16));
+              else
+                var->address.address = (void *)strtoul(global_address, NULL, 16);
+              xbt_free(global_address);
+              global_address = NULL;
+            }
+
+          }
+                   
+        }else if(strcmp(node_type, "DW_AT_type") == 0){
+          
+          type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
+          xbt_str_ltrim(type_origin, "<0x");
+          xbt_str_rtrim(type_origin, ">");
+        
+        }else if(strcmp(node_type, "DW_AT_declaration") == 0){
 
+          new_variable = 0;
+          if(new_variable){
+            dw_variable_free(var);
+            var = NULL;
+          }
+        
+        }else if(strcmp(node_type, "DW_AT_artificial") == 0){
+          
+          new_variable = 0;
+          if(new_variable){
+            dw_variable_free(var);
+            var = NULL;
+          }
+        
+        }
 
-void MC_show_stack_liveness(xbt_fifo_t stack){
-  int value;
-  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_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){
-      if(pair->requests>0){
-        req_str = MC_request_to_string(req, value);
-        XBT_INFO("%s", req_str);
-        xbt_free(req_str);
-      }else{
-        XBT_INFO("End of system requests but evolution in Büchi automaton");
+        read = xbt_getline(&line, &n, fp);
       }
-    }
-  }
-}
 
-void MC_dump_stack_liveness(xbt_fifo_t stack){
+      if(new_variable == 1){
+        
+        if(!global_variable){
+          variable_frame = xbt_dict_get_or_null(*local_variables, current_frame);
+          var->type_origin = strdup(type_origin);
+          var->global = 0;
+          index = MC_dwarf_get_variable_index(variable_frame->variables, var->name, NULL);
+          if(index != -1)
+            xbt_dynar_insert_at(variable_frame->variables, index, &var);
+        }else{
+          var->type_origin = strdup(type_origin);
+          var->global = 1;
+          index = MC_dwarf_get_variable_index(*global_variables, var->name, var->address.address);
+          if(index != -1)
+            xbt_dynar_insert_at(*global_variables, index, &var); 
+        }
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+         xbt_free(type_origin);
+         type_origin = NULL;
+      }
 
-  mc_pair_t pair;
+      global_variable = 0;
+      new_variable = 1;
 
-  MC_SET_RAW_MEM;
-  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
-    MC_pair_delete(pair);
-  MC_UNSET_RAW_MEM;
+    }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+      read = xbt_getline(&line, &n, fp);
 
-}
+      while(read != -1){
 
+        /* Wipeout the new line character */
+        line[read - 1] = '\0'; 
 
-void MC_print_statistics(mc_stats_t stats)
-{
-  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);
-  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;
-}
+        if(n == 0 || strlen(line) == 0){
+          read = xbt_getline(&line, &n, fp);
+          continue;
+        }
 
-void MC_assert(int prop)
-{
-  if (MC_is_active() && !prop){
-    XBT_INFO("**************************");
-    XBT_INFO("*** PROPERTY NOT VALID ***");
-    XBT_INFO("**************************");
-    XBT_INFO("Counter-example execution trace:");
-    MC_dump_stack_safety(mc_stack_safety);
-    MC_print_statistics(mc_stats);
-    xbt_abort();
-  }
-}
+        xbt_dynar_free(&split);
+        xbt_str_rtrim(line, NULL);
+        xbt_str_strip_spaces(line);
+        split = xbt_str_split(line, " ");
+        
+        if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
+          break;
+          
+        node_type = xbt_dynar_get_as(split, 1, char *);
 
-static void MC_assert_pair(int prop){
-  if (MC_is_active() && !prop) {
-    XBT_INFO("**************************");
-    XBT_INFO("*** PROPERTY NOT VALID ***");
-    XBT_INFO("**************************");
-    //XBT_INFO("Counter-example execution trace:");
-    MC_show_stack_liveness(mc_stack_liveness);
-    //MC_dump_snapshot_stack(mc_snapshot_stack);
-    MC_print_statistics(mc_stats);
-    xbt_abort();
-  }
-}
+        if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 
-void MC_process_clock_add(smx_process_t process, double amount)
-{
-  mc_time[process->pid] += amount;
-}
+          origin = xbt_dynar_get_as(split, 2, char *);
+          xbt_str_ltrim(origin, "<0x");
+          xbt_str_rtrim(origin, ">");
+          
+          subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
+          subroutine_frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
+        
+        }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 
-double MC_process_clock_get(smx_process_t process)
-{
-  if(mc_time){
-    if(process != NULL)
-      return mc_time[process->pid];
-    else 
-      return -1;
-  }else{
-    return 0;
-  }
-}
+          subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 
-void MC_automaton_load(const char *file){
+        }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+          subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
+        }
 
-  MC_SET_RAW_MEM;
+        read = xbt_getline(&line, &n, fp);
+      
+      }
 
-  if (_mc_property_automaton == NULL)
-    _mc_property_automaton = xbt_automaton_new();
-  
-  xbt_automaton_load(_mc_property_automaton,file);
+    }else if(strcmp(node_type, "(DW_TAG_base_type)") == 0 
+             || strcmp(node_type, "(DW_TAG_enumeration_type)") == 0
+             || strcmp(node_type, "(DW_TAG_enumerator)") == 0
+             || strcmp(node_type, "(DW_TAG_typedef)") == 0
+             || strcmp(node_type, "(DW_TAG_const_type)") == 0
+             || strcmp(node_type, "(DW_TAG_subroutine_type)") == 0
+             || strcmp(node_type, "(DW_TAG_volatile_type)") == 0
+             || (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)"))){
+
+      if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
+        type_type = e_dw_base_type;
+      else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
+        type_type = e_dw_enumeration_type;
+      else if(strcmp(node_type, "(DW_TAG_enumerator)") == 0)
+        type_type = e_dw_enumerator;
+      else if(strcmp(node_type, "(DW_TAG_typedef)") == 0)
+        type_type = e_dw_typedef;
+      else if(strcmp(node_type, "(DW_TAG_const_type)") == 0)
+        type_type = e_dw_const_type;
+      else if(strcmp(node_type, "(DW_TAG_pointer_type)") == 0)
+        type_type = e_dw_pointer_type;
+      else if(strcmp(node_type, "(DW_TAG_subroutine_type)") == 0)
+        type_type = e_dw_subroutine_type;
+      else if(strcmp(node_type, "(DW_TAG_volatile_type)") == 0)
+        type_type = e_dw_volatile_type;
 
-  MC_UNSET_RAW_MEM;
+      strtok(xbt_dynar_get_as(split, 0, char *), "<");
+      origin = strdup(strtok(NULL, "<"));
+      xbt_str_rtrim(origin, ">:");
+      
+      read = xbt_getline(&line, &n, fp);
+      
+      while(read != -1){
+        
+         /* Wipeout the new line character */
+        line[read - 1] = '\0'; 
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
+        if(n == 0 || strlen(line) == 0){
+          read = xbt_getline(&line, &n, fp);
+          continue;
+        }
 
-}
+        xbt_dynar_free(&split);
+        xbt_str_rtrim(line, NULL);
+        xbt_str_strip_spaces(line);
+        split = xbt_str_split(line, " ");
+        
+        if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
+          break;
 
-void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
+        node_type = xbt_dynar_get_as(split, 1, char *);
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+        if(strcmp(node_type, "DW_AT_byte_size") == 0){
+          size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
+          if(type_type == e_dw_enumeration_type)
+            enumeration_size = size;
+        }else if(strcmp(node_type, "DW_AT_name") == 0){
+          end = xbt_str_join(split, " ");
+          xbt_dynar_free(&split);
+          split = xbt_str_split(end, "):");
+          xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
+          name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
+        }else if(strcmp(node_type, "DW_AT_type") == 0){
+          type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
+          xbt_str_ltrim(type_origin, "<0x");
+          xbt_str_rtrim(type_origin, ">");
+        }
+        
+        read = xbt_getline(&line, &n, fp);
+      }
 
-  MC_SET_RAW_MEM;
+      dw_type_t type = xbt_new0(s_dw_type_t, 1);
+      type->type = type_type;
+      if(name)
+        type->name = xbt_strdup(name);
+      else
+        type->name = xbt_strdup("undefined");
+      type->is_pointer_type = is_pointer;
+      type->id = (void *)strtoul(origin, NULL, 16);
+      if(type_origin)
+        type->dw_type_id = xbt_strdup(type_origin);
+      if(type_type == e_dw_enumerator)
+        type->size = enumeration_size;
+      else
+        type->size = size;
+      type->members = NULL;
 
-  if (_mc_property_automaton == NULL)
-    _mc_property_automaton = xbt_automaton_new();
+      xbt_dict_set(*types, origin, type, NULL); 
 
-  xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
+      xbt_free(name);
+      name = NULL;
+      xbt_free(type_origin);
+      type_origin = NULL;
+      xbt_free(end);
+      end = NULL;
 
-  MC_UNSET_RAW_MEM;
+      is_pointer = 0;
+      size = 0;
+      xbt_free(origin);
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-  
-}
+    }else if(strcmp(node_type, "(DW_TAG_structure_type)") == 0 || strcmp(node_type, "(DW_TAG_union_type)") == 0){
+      
+      if(strcmp(node_type, "(DW_TAG_structure_type)") == 0)
+        struct_decl = 1;
+      else
+        union_decl = 1;
 
-/************ MC_ignore ***********/ 
+      strtok(xbt_dynar_get_as(split, 0, char *), "<");
+      origin = strdup(strtok(NULL, "<"));
+      xbt_str_rtrim(origin, ">:");
+      
+      read = xbt_getline(&line, &n, fp);
 
-void heap_ignore_region_free(mc_heap_ignore_region_t r){
-  xbt_free(r);
-}
+      dw_type_t type = NULL;
 
-void heap_ignore_region_free_voidp(void *r){
-  heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
-}
+      while(read != -1){
+      
+        while(read != -1){
+        
+          /* Wipeout the new line character */
+          line[read - 1] = '\0'; 
 
-void MC_ignore_heap(void *address, size_t size){
+          if(n == 0 || strlen(line) == 0){
+            read = xbt_getline(&line, &n, fp);
+            continue;
+          }
 
-  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+          xbt_dynar_free(&split);
+          xbt_str_rtrim(line, NULL);
+          xbt_str_strip_spaces(line);
+          split = xbt_str_split(line, " ");
+        
+          node_type = xbt_dynar_get_as(split, 1, char *);
 
-  MC_SET_RAW_MEM;
+          if(strncmp(node_type, "DW_AT_", 6) != 0){
+            member_end = 1;
+            break;
+          }
 
-  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++;
-  }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]++;
-  }
-  
-  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;
-  }
+          if(strcmp(node_type, "DW_AT_byte_size") == 0){
+            size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
+          }else if(strcmp(node_type, "DW_AT_name") == 0){
+            xbt_free(end);
+            end = xbt_str_join(split, " ");
+            xbt_dynar_free(&split);
+            split = xbt_str_split(end, "):");
+            xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
+            name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
+          }else if(strcmp(node_type, "DW_AT_type") == 0){
+            type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
+            xbt_str_ltrim(type_origin, "<0x");
+            xbt_str_rtrim(type_origin, ">");
+          }else if(strcmp(node_type, "DW_AT_data_member_location:") == 0){
+            xbt_free(end);
+            end = xbt_str_join(split, " ");
+            xbt_dynar_free(&split);
+            split = xbt_str_split(end, "DW_OP_plus_uconst:");
+            xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), NULL);
+            xbt_str_rtrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), ")");
+            offset = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
+          }
+
+          read = xbt_getline(&line, &n, fp);
+          
+        }
+
+        if(member_end && type){         
+          member_end = 0;
+          
+          dw_type_t member_type = xbt_new0(s_dw_type_t, 1);
+          member_type->name = xbt_strdup(name);
+          member_type->size = size;
+          member_type->is_pointer_type = is_pointer;
+          member_type->id = (void *)strtoul(origin, NULL, 16);
+          member_type->offset = offset;
+          if(type_origin)
+            member_type->dw_type_id = xbt_strdup(type_origin);
+
+          xbt_dynar_push(type->members, &member_type);
+
+          xbt_free(name);
+          name = NULL;
+          xbt_free(end);
+          end = NULL;
+          xbt_free(type_origin);
+          type_origin = NULL;
+          size = 0;
+          offset = 0;
+
+          xbt_free(origin);
+          origin = NULL;
+          strtok(xbt_dynar_get_as(split, 0, char *), "<");
+          origin = strdup(strtok(NULL, "<"));
+          xbt_str_rtrim(origin, ">:");
+
+        }
+
+        if(struct_decl || union_decl){
+          type = xbt_new0(s_dw_type_t, 1);
+          if(struct_decl)
+            type->type = e_dw_structure_type;
+          else
+            type->type = e_dw_union_type;
+          type->name = xbt_strdup(name);
+          type->size = size;
+          type->is_pointer_type = is_pointer;
+          type->id = (void *)strtoul(origin, NULL, 16);
+          if(type_origin)
+            type->dw_type_id = xbt_strdup(type_origin);
+          type->members = xbt_dynar_new(sizeof(dw_type_t), dw_type_free_voidp);
+          
+          xbt_dict_set(*types, origin, type, NULL); 
+          
+          xbt_free(name);
+          name = NULL;
+          xbt_free(end);
+          end = NULL;
+          xbt_free(type_origin);
+          type_origin = NULL;
+          size = 0;
+          struct_decl = 0;
+          union_decl = 0;
+
+        }
+
+        if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_member)") != 0)
+          break;  
+
+        read = xbt_getline(&line, &n, fp);
+    
+      }
+
+      xbt_free(origin);
+      origin = NULL;
+
+    }else if(strcmp(node_type, "(DW_TAG_array_type)") == 0){
+      
+      strtok(xbt_dynar_get_as(split, 0, char *), "<");
+      origin = strdup(strtok(NULL, "<"));
+      xbt_str_rtrim(origin, ">:");
+      
+      read = xbt_getline(&line, &n, fp);
+
+      dw_type_t type = NULL;
+
+      while(read != -1){
+      
+        while(read != -1){
+        
+          /* Wipeout the new line character */
+          line[read - 1] = '\0'; 
+
+          if(n == 0 || strlen(line) == 0){
+            read = xbt_getline(&line, &n, fp);
+            continue;
+          }
+
+          xbt_dynar_free(&split);
+          xbt_str_rtrim(line, NULL);
+          xbt_str_strip_spaces(line);
+          split = xbt_str_split(line, " ");
+        
+          node_type = xbt_dynar_get_as(split, 1, char *);
+
+          if(strncmp(node_type, "DW_AT_", 6) != 0)
+            break;
+
+          if(strcmp(node_type, "DW_AT_upper_bound") == 0){
+            size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
+          }else if(strcmp(node_type, "DW_AT_name") == 0){
+            end = xbt_str_join(split, " ");
+            xbt_dynar_free(&split);
+            split = xbt_str_split(end, "):");
+            xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
+            name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
+          }else if(strcmp(node_type, "DW_AT_type") == 0){
+            type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
+            xbt_str_ltrim(type_origin, "<0x");
+            xbt_str_rtrim(type_origin, ">");
+          }
+
+          read = xbt_getline(&line, &n, fp);
+          
+        }
+
+        if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") == 0){
+          subrange = 1;         
+        }
+
+        if(subrange && type){         
+          type->size = size;
+      
+          xbt_free(name);
+          name = NULL;
+          xbt_free(end);
+          end = NULL;
+          xbt_free(type_origin);
+          type_origin = NULL;
+          size = 0;
+
+          xbt_free(origin);
+          origin = NULL;
+          strtok(xbt_dynar_get_as(split, 0, char *), "<");
+          origin = strdup(strtok(NULL, "<"));
+          xbt_str_rtrim(origin, ">:");
+
+        }else {
+          
+          type = xbt_new0(s_dw_type_t, 1);
+          type->type = e_dw_array_type;
+          type->name = xbt_strdup(name);
+          type->is_pointer_type = is_pointer;
+          type->id = (void *)strtoul(origin, NULL, 16);
+          if(type_origin)
+            type->dw_type_id = xbt_strdup(type_origin);
+          type->members = NULL;
+          
+          xbt_dict_set(*types, origin, type, NULL); 
+          
+          xbt_free(name);
+          name = NULL;
+          xbt_free(end);
+          end = NULL;
+          xbt_free(type_origin);
+          type_origin = NULL;
+          size = 0;
+        }
+
+        if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") != 0)
+          break;  
+
+        read = xbt_getline(&line, &n, fp);
+    
+      }
+
+      xbt_free(origin);
+      origin = NULL;
+
+    }else{
+
+      read = xbt_getline(&line, &n, fp);
+
+    }
+
+  }
+  
+  xbt_dynar_free(&split);
+  xbt_dict_free(&variables_origin);
+  xbt_dict_free(&subprograms_origin);
+  xbt_free(line);
+  xbt_free(command);
+  pclose(fp);
+  
+}
+
+
+/*******************************  Ignore mechanism *******************************/
+/*********************************************************************************/
+
+typedef struct s_mc_stack_ignore_variable{
+  int in_libsimgrid;
+  char *var_name;
+  char *frame;
+}s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
+
+typedef struct s_mc_data_bss_ignore_variable{
+  int in_libsimgrid;
+  char *name;
+}s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
+
+/**************************** Free functions ******************************/
+
+static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
+  xbt_free(v->var_name);
+  xbt_free(v->frame);
+  xbt_free(v);
+}
+
+static void stack_ignore_variable_free_voidp(void *v){
+  stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
+}
+
+void heap_ignore_region_free(mc_heap_ignore_region_t r){
+  xbt_free(r);
+}
+
+void heap_ignore_region_free_voidp(void *r){
+  heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
+}
+
+static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
+  xbt_free(v->name);
+  xbt_free(v);
+}
+
+static void data_bss_ignore_variable_free_voidp(void *v){
+  data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
+}
+
+/***********************************************************************/
+
+void MC_ignore_heap(void *address, size_t size){
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
+  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++;
+  }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]++;
+  }
+  
+  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 = NULL;
@@ -950,194 +1363,232 @@ void MC_remove_ignore_heap(void *address, size_t size){
 
 }
 
-void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
-  xbt_free(v);
-}
-
-void data_bss_ignore_variable_free_voidp(void *v){
-  data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
-}
-
-void MC_ignore_data_bss(void *address, size_t size){
+void MC_ignore_global_variable(const char *name,  ...){
 
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
-  
-  if(mc_data_bss_comparison_ignore == NULL)
-    mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
 
-  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;
+  va_list ap;
+  va_start(ap, name);
+  int in_libsimgrid = va_arg(ap, int);
+  va_end(ap);
 
-  if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
-
-    xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
+  xbt_dynar_t variables = NULL;
 
+  if(in_libsimgrid == 1){
+    variables = mc_global_variables_libsimgrid;
   }else{
-    
-    unsigned int cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
-    mc_data_bss_ignore_variable_t current_var = NULL;
-
-    while(start <= end){
-      cursor = (start + end) / 2;
-      current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
-      if(current_var->address == address){
-        data_bss_ignore_variable_free(var);
-        MC_UNSET_RAW_MEM;
-        if(raw_mem_set)
-          MC_SET_RAW_MEM;
-        return;
-      }
-      if(current_var->address < address)
-        start = cursor + 1;
-      if(current_var->address > address)
-        end = cursor - 1;
-    }
-
-    if(current_var->address < address)
-      xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
-    else
-      xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
-
+    variables = mc_global_variables_binary;
   }
 
-  /* Remove variable from mc_global_variables */
-
-  if(mc_global_variables != NULL){
+  if(variables){
 
     unsigned int cursor = 0;
+    dw_variable_t current_var;
     int start = 0;
-    int end = xbt_dynar_length(mc_global_variables) - 1;
-    global_variable_t current_var;
+    int end = xbt_dynar_length(variables) - 1;
     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){
+      cursor = (start + end) /2;
+      current_var = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
+      if(strcmp(current_var->name, name) == 0){
+        xbt_dynar_remove_at(variables, cursor, NULL);
         var_found = 1;
         break;
-      }
-      if(current_var->address < address)
+      }else if(strcmp(current_var->name, name) < 0){
         start = cursor + 1;
-      if(current_var->address > address)
+      }else{
         end = cursor - 1;
+      } 
     }
 
-    if(var_found)
-      xbt_dynar_remove_at(mc_global_variables, cursor, NULL);
+    if(var_found){
+      if(in_libsimgrid == 1)
+        MC_ignore_global_variable(name, 1);
+      else 
+        MC_ignore_global_variable(name);
+    }
     
-  }
+  }else{
 
-  MC_UNSET_RAW_MEM;
+    if(mc_data_bss_comparison_ignore == NULL)
+      mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
 
-  if(raw_mem_set)
-    MC_SET_RAW_MEM;
-}
+    mc_data_bss_ignore_variable_t var = NULL;
+    var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
+    var->name = strdup(name);
+    var->in_libsimgrid = (in_libsimgrid == 1);
 
-static size_t data_bss_ignore_size(void *address){
-  unsigned int cursor = 0;
-  int start = 0;
-  int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
-  mc_data_bss_ignore_variable_t var;
+    if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
 
-  while(start <= end){
-    cursor = (start + end) / 2;
-    var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
-    if(var->address == address)
-      return var->size;
-    if(var->address < address){
-      if((void *)((char *)var->address + var->size) > address)
-        return (char *)var->address + var->size - (char*)address;
+      xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
+
+    }else{
+    
+      unsigned int cursor = 0;
+      int start = 0;
+      int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
+      mc_data_bss_ignore_variable_t current_var = NULL;
+
+      while(start <= end){
+        cursor = (start + end) / 2;
+        current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
+        if(strcmp(current_var->name, name) == 0){
+          data_bss_ignore_variable_free(var);
+          if(!raw_mem_set)
+            MC_UNSET_RAW_MEM;
+          return;
+        }else if(strcmp(current_var->name, name) < 0){
+          start = cursor + 1;
+        }else{
+          end = cursor - 1;
+        }
+      }
+
+      if(strcmp(current_var->name, name) < 0)
+        xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
       else
-        start = cursor + 1;
+        xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
+
     }
-    if(var->address > address)
-      end = cursor - 1;   
   }
 
-  return 0;
-}
-
-void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
-  xbt_free(v->var_name);
-  xbt_free(v->frame);
-  xbt_free(v);
-}
+  MC_UNSET_RAW_MEM;
 
-void stack_ignore_variable_free_voidp(void *v){
-  stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 }
 
-void MC_ignore_stack(const char *var_name, const char *frame_name){
+void MC_ignore_local_variable(const char *var_name, const char *frame_name, ...){
   
   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
   MC_SET_RAW_MEM;
 
-  if(mc_stack_comparison_ignore == NULL)
-    mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
-  
-  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_name);
-  
-  if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
+  va_list ap;
+  va_start(ap, frame_name);
+  int in_libsimgrid = va_arg(ap, int);
+  va_end(ap);
 
-    xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
+  xbt_dict_t variables = NULL;
 
+  if(in_libsimgrid == 1){
+    variables = mc_local_variables_libsimgrid;
   }else{
-    
-    unsigned int cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
-    mc_stack_ignore_variable_t current_var = NULL;
+    variables = mc_local_variables_binary;
+  }
 
-    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_name) == 0){
-        if(strcmp(current_var->var_name, var_name) == 0){
-          stack_ignore_variable_free(var);
-          MC_UNSET_RAW_MEM;
-          if(raw_mem_set)
-            MC_SET_RAW_MEM;
-          return;
+  if(variables){
+    unsigned int cursor = 0;
+    dw_variable_t current_var;
+    int start, end;
+    if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames (binary and libsimgrid) */
+      xbt_dict_cursor_t dict_cursor, dict_cursor2;
+      char *current_frame_name;
+      dw_frame_t frame;
+      xbt_dict_foreach(mc_local_variables_libsimgrid, dict_cursor, current_frame_name, frame){
+        start = 0;
+        end = xbt_dynar_length(frame->variables) - 1;
+        while(start <= end){
+          cursor = (start + end) / 2;
+          current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);          
+          if(strcmp(current_var->name, var_name) == 0){
+            xbt_dynar_remove_at(frame->variables, cursor, NULL);
+            start = 0;
+            end = xbt_dynar_length(frame->variables) - 1;
+          }else if(strcmp(current_var->name, var_name) < 0){
+            start = cursor + 1;
+          }else{
+            end = cursor - 1;
+          } 
+        }
+      }
+      xbt_dict_foreach(mc_local_variables_binary, dict_cursor2, current_frame_name, frame){
+        start = 0;
+        end = xbt_dynar_length(frame->variables) - 1;
+        while(start <= end){
+          cursor = (start + end) / 2;
+          current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
+          if(strcmp(current_var->name, var_name) == 0){
+            xbt_dynar_remove_at(frame->variables, cursor, NULL);
+            start = 0;
+            end = xbt_dynar_length(frame->variables) - 1;
+          }else if(strcmp(current_var->name, var_name) < 0){
+            start = cursor + 1;
+          }else{
+            end = cursor - 1;
+          } 
         }
-        if(strcmp(current_var->var_name, var_name) < 0)
+      }
+    }else{
+      xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, frame_name))->variables;
+      start = 0;
+      end = xbt_dynar_length(variables_list) - 1;
+      while(start <= end){
+        cursor = (start + end) / 2;
+        current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
+        if(strcmp(current_var->name, var_name) == 0){
+          xbt_dynar_remove_at(variables_list, cursor, NULL);
+          start = 0;
+          end = xbt_dynar_length(variables_list) - 1;
+        }else if(strcmp(current_var->name, var_name) < 0){
           start = cursor + 1;
-        if(strcmp(current_var->var_name, var_name) > 0)
+        }else{
           end = cursor - 1;
+        } 
       }
-      if(strcmp(current_var->frame, frame_name) < 0)
-        start = cursor + 1;
-      if(strcmp(current_var->frame, frame_name) > 0)
-        end = cursor - 1;
-    }
+    } 
+  }else{
 
-    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);
+    if(mc_stack_comparison_ignore == NULL)
+      mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
+  
+    mc_stack_ignore_variable_t var = NULL;
+    var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
+    var->in_libsimgrid = (in_libsimgrid == 1);
+    var->var_name = strdup(var_name);
+    var->frame = strdup(frame_name);
+  
+    if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
 
-  }
+      xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
 
- /* Remove variable from mc_local_variables */
+    }else{
+    
+      unsigned int cursor = 0;
+      int start = 0;
+      int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
+      mc_stack_ignore_variable_t current_var = NULL;
+
+      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_name) == 0){
+          if(strcmp(current_var->var_name, var_name) == 0){
+            stack_ignore_variable_free(var);
+            if(!raw_mem_set)
+              MC_UNSET_RAW_MEM;
+            return;
+          }
+          if(strcmp(current_var->var_name, var_name) < 0)
+            start = cursor + 1;
+          if(strcmp(current_var->var_name, var_name) > 0)
+            end = cursor - 1;
+        }
+        if(strcmp(current_var->frame, frame_name) < 0)
+          start = cursor + 1;
+        if(strcmp(current_var->frame, frame_name) > 0)
+          end = cursor - 1;
+      }
 
-  if(mc_local_variables != NULL){
+      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);
 
-    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;
@@ -1170,857 +1621,830 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
     MC_SET_RAW_MEM;
 }
 
-/************ DWARF ***********/
+/*******************************  Initialisation of MC *******************************/
+/*********************************************************************************/
 
-xbt_dict_t MC_get_location_list(const char *elf_file){
+static void MC_dump_ignored_local_variables(void){
 
-  char *command = bprintf("objdump -Wo %s", elf_file);
+  if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
+    return;
 
-  FILE *fp = popen(command, "r");
+  unsigned int cursor = 0;
+  mc_stack_ignore_variable_t current_var;
+  xbt_dict_t variables;
 
-  if(fp == NULL){
-    perror("popen for objdump failed");
-    xbt_abort();
+  xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
+
+    if(current_var->in_libsimgrid == 1){
+      variables = mc_local_variables_libsimgrid;
+    }else{
+      variables = mc_local_variables_binary;
+    }
+
+    unsigned int cursor2 = 0;
+    dw_variable_t var;
+    int start, end;
+
+    if(strcmp(current_var->frame, "*") == 0){
+      xbt_dict_cursor_t dict_cursor;
+      char *frame_name;
+      dw_frame_t frame;
+      xbt_dict_foreach(variables, dict_cursor, frame_name, frame){
+        start = 0;
+        end = xbt_dynar_length(frame->variables) - 1;
+        while(start <= end){
+          cursor2 = (start + end) / 2;
+          var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor2, dw_variable_t);
+          if(strcmp(var->name, current_var->var_name) == 0){
+            xbt_dynar_remove_at(frame->variables, cursor2, NULL);
+            start = 0;
+            end = xbt_dynar_length(frame->variables) - 1;
+          }else if(strcmp(var->name, current_var->var_name) < 0){
+            start = cursor2 + 1;
+          }else{
+            end = cursor2 - 1;
+          } 
+        }
+      }
+    }else{
+      xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(variables, current_var->frame))->variables;
+      start = 0;
+      end = xbt_dynar_length(variables_list) - 1;
+      while(start <= end){
+        cursor2 = (start + end) / 2;
+        var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor2, dw_variable_t);
+        if(strcmp(var->name, current_var->var_name) == 0){
+          xbt_dynar_remove_at(variables_list, cursor2, NULL);
+          start = 0;
+          end = xbt_dynar_length(variables_list) - 1; 
+        }else if(strcmp(var->name, current_var->var_name) < 0){
+          start = cursor2 + 1;
+        }else{
+          end = cursor2 - 1;
+        } 
+      }
+    } 
   }
 
-  int debug = 0; /*Detect if the program has been compiled with -g */
+  xbt_dynar_free(&mc_stack_comparison_ignore);
+  mc_stack_comparison_ignore = NULL;
+}
 
-  xbt_dict_t location_list = xbt_dict_new_homogeneous(NULL);
-  char *line = NULL, *loc_expr = NULL;
-  ssize_t read;
-  size_t n = 0;
-  int cursor_remove;
-  xbt_dynar_t split = NULL;
-
-  while ((read = xbt_getline(&line, &n, fp)) != -1) {
+static void MC_dump_ignored_global_variables(void){
 
-    /* Wipeout the new line character */
-    line[read - 1] = '\0';
+  if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
+    return;
 
-    xbt_str_trim(line, NULL);
-    
-    if(n == 0)
-      continue;
+  unsigned int cursor = 0;
+  mc_data_bss_ignore_variable_t current_var;
+  xbt_dynar_t variables;
+  
+  unsigned int cursor2 = 0;
+  dw_variable_t var;
+  int start, end;
 
-    if(strlen(line) == 0)
-      continue;
+  xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
 
-    if(debug == 0){
+    if(current_var->in_libsimgrid == 1){
+      variables = mc_global_variables_libsimgrid;
+    }else{
+      variables = mc_global_variables_binary;
+    }
 
-      if(strncmp(line, elf_file, strlen(elf_file)) == 0)
-        continue;
-      
-      if(strncmp(line, "Contents", 8) == 0)
-        continue;
+    cursor2 = 0;
+    start = 0;
+    end = xbt_dynar_length(variables) - 1;
 
-      if(strncmp(line, "Offset", 6) == 0){
-        debug = 1;
-        continue;
-      }
+    while(start <= end){
+      cursor2 = (start + end) / 2;
+      var = (dw_variable_t)xbt_dynar_get_as(variables, cursor2, dw_variable_t);
+      if(strcmp(var->name, current_var->name) == 0){
+        xbt_dynar_remove_at(variables, cursor2, NULL);
+        return;
+      }else if(strcmp(var->name, current_var->name) < 0){
+        start = cursor2 + 1;
+      }else{
+        end = cursor2 - 1;
+      } 
     }
+  } 
 
-    if(debug == 0){
-      XBT_INFO("Your program must be compiled with -g");
-      xbt_abort();
-    }
+  xbt_dynar_free(&mc_data_bss_comparison_ignore);
+  mc_data_bss_comparison_ignore = NULL;
+  
 
-    xbt_dynar_t loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
+}
 
-    xbt_str_strip_spaces(line);
-    split = xbt_str_split(line, " ");
+void MC_init(){
 
-    while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
-      
-      dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
-      new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
-      new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
-      
-      cursor_remove =0;
-      while(cursor_remove < 3){
-        xbt_dynar_remove_at(split, 0, NULL);
-        cursor_remove++;
-      }
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+  
+  compare = 0;
 
-      loc_expr = xbt_str_join(split, " ");
-      xbt_str_ltrim(loc_expr, "(");
-      xbt_str_rtrim(loc_expr, ")");
-      new_entry->location = get_location(NULL, loc_expr);
+  /* Initialize the data structures that must be persistent across every
+     iteration of the model-checker (in RAW memory) */
 
-      xbt_dynar_push(loclist, &new_entry);
+  MC_SET_RAW_MEM;
 
-      xbt_dynar_free(&split);
-      free(loc_expr);
+  MC_init_memory_map_info();
+  
+  mc_local_variables_libsimgrid = xbt_dict_new_homogeneous(NULL);
+  mc_local_variables_binary = xbt_dict_new_homogeneous(NULL);
+  mc_global_variables_libsimgrid = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
+  mc_global_variables_binary = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
+  mc_variables_type_libsimgrid = xbt_dict_new_homogeneous(NULL);
+  mc_variables_type_binary = xbt_dict_new_homogeneous(NULL);
 
-      read = xbt_getline(&line, &n, fp);
-      if(read != -1){
-        line[read - 1] = '\0';
-        xbt_str_strip_spaces(line);
-        split = xbt_str_split(line, " ");
-      }
+  XBT_INFO("Get debug information ...");
 
-    }
+  /* Get local variables in binary for state equality detection */
+  xbt_dict_t binary_location_list = MC_dwarf_get_location_list(xbt_binary_name);
+  MC_dwarf_get_variables(xbt_binary_name, binary_location_list, &mc_local_variables_binary, &mc_global_variables_binary, &mc_variables_type_binary);
 
+  /* Get local variables in libsimgrid for state equality detection */
+  xbt_dict_t libsimgrid_location_list = MC_dwarf_get_location_list(libsimgrid_path);
+  MC_dwarf_get_variables(libsimgrid_path, libsimgrid_location_list, &mc_local_variables_libsimgrid, &mc_global_variables_libsimgrid, &mc_variables_type_libsimgrid);
 
-    char *key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
-    xbt_dict_set(location_list, key, loclist, NULL);
-    xbt_free(key);
-    
-    xbt_dynar_free(&split);
+  xbt_dict_free(&libsimgrid_location_list);
+  xbt_dict_free(&binary_location_list);
 
-  }
+  /* Remove variables ignored before getting list of variables */
+  MC_dump_ignored_local_variables();
+  MC_dump_ignored_global_variables();
+  
+  /* Get .plt section (start and end addresses) for data libsimgrid and data program comparison */
+  MC_get_libsimgrid_plt_section();
+  MC_get_binary_plt_section();
 
-  xbt_free(line);
-  xbt_free(command);
-  pclose(fp);
+  MC_UNSET_RAW_MEM;
 
-  return location_list;
-}
+   /* 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", "*", 1);
+  MC_ignore_local_variable("__ex_mctx_en", "*", 1);
+  MC_ignore_local_variable("__ex_mctx_me", "*", 1);
+  MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*", 1);
+  MC_ignore_local_variable("_log_ev", "*", 1);
+  MC_ignore_local_variable("_throw_ctx", "*", 1);
+  MC_ignore_local_variable("ctx", "*", 1);
+
+  MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial", 1);
+  MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial", 1);
 
-static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
+  /* Ignore local variable about time used for tracing */
+  MC_ignore_local_variable("start_time", "*", 1); 
 
-  xbt_dict_cursor_t cursor = NULL;
-  char *name;
-  dw_frame_t res;
+  MC_ignore_global_variable("mc_comp_times", 1);
+  MC_ignore_global_variable("mc_snapshot_comparison_time", 1); 
+  MC_ignore_global_variable("mc_time", 1);
+  MC_ignore_global_variable("smpi_current_rank", 1);
+  MC_ignore_global_variable("smx_current_context_serial", 1);
+  MC_ignore_global_variable("smx_current_context_key", 1);
+  MC_ignore_global_variable("sysv_maestro_context", 1);
+  MC_ignore_global_variable("counter", 1); /* Static variable used for tracing */
 
-  xbt_dict_foreach(all_variables, cursor, name, res) {
-    if(offset >= res->start && offset < res->end){
-      xbt_dict_cursor_free(&cursor);
-      return res;
-    }
-  }
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+
+  XBT_INFO("Get debug information done !");
 
-  xbt_dict_cursor_free(&cursor);
-  return NULL;
-  
 }
 
-void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *all_variables){
+static void MC_init_dot_output(){ /* FIXME : more colors */
 
-  char *command = bprintf("objdump -Wi %s", elf_file);
-  
-  FILE *fp = popen(command, "r");
+  colors[0] = "blue";
+  colors[1] = "red";
+  colors[2] = "green3";
+  colors[3] = "goldenrod";
+  colors[4] = "brown";
+  colors[5] = "purple";
+  colors[6] = "magenta";
+  colors[7] = "turquoise4";
+  colors[8] = "gray25";
+  colors[9] = "forestgreen";
+  colors[10] = "hotpink";
+  colors[11] = "lightblue";
+  colors[12] = "tan";
 
-  if(fp == NULL)
-    perror("popen for objdump failed");
+  dot_output = fopen(_sg_mc_dot_output_file, "w");
+  
+  if(dot_output == NULL){
+    perror("Error open dot output file");
+    xbt_abort();
+  }
 
-  char *line = NULL, *origin, *abstract_origin, *current_frame = NULL;
-  ssize_t read =0;
-  size_t n = 0;
-  int valid_variable = 1;
-  char *node_type = NULL, *location_type = NULL, *variable_name = NULL, *loc_expr = NULL;
-  xbt_dynar_t split = NULL, split2 = NULL;
+  fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
 
-  xbt_dict_t variables_origin = xbt_dict_new_homogeneous(NULL);
-  xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(NULL);
-  char *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL;
-  int new_frame = 0, new_variable = 0;
-  dw_frame_t variable_frame, subroutine_frame = NULL;
+}
 
-  read = xbt_getline(&line, &n, fp);
+/*******************************  Core of MC *******************************/
+/**************************************************************************/
 
-  while (read != -1) {
+void MC_do_the_modelcheck_for_real() {
 
-    if(n == 0){
-      read = xbt_getline(&line, &n, fp);
-      continue;
-    }
-    /* Wipeout the new line character */
-    line[read - 1] = '\0';
-   
-    if(strlen(line) == 0){
-      read = xbt_getline(&line, &n, fp);
-      continue;
-    }
+  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;
 
-    xbt_str_ltrim(line, NULL);
-    xbt_str_strip_spaces(line);
-    
-    if(line[0] != '<'){
-      read = xbt_getline(&line, &n, fp);
-      continue;
-    }
-    
-    xbt_dynar_free(&split);
-    split = xbt_str_split(line, " ");
+    XBT_INFO("Check a safety property");
+    MC_modelcheck_safety();
 
-    /* Get node type */
-    node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
+  } else  {
 
-    if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
+    if (mc_reduce_kind==e_mc_reduce_unset)
+      mc_reduce_kind=e_mc_reduce_none;
 
-      dw_frame_t frame = NULL;
+    XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
+    MC_automaton_load(_sg_mc_property_file);
+    MC_modelcheck_liveness();
+  }
+}
 
-      strtok(xbt_dynar_get_as(split, 0, char *), "<");
-      subprogram_start = strdup(strtok(NULL, "<"));
-      xbt_str_rtrim(subprogram_start, ">:");
+void MC_modelcheck_safety(void)
+{
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-      read = xbt_getline(&line, &n, fp);
-   
-      while(read != -1){
+  /* Check if MC is already initialized */
+  if (initial_state_safety)
+    return;
 
-        if(n == 0){
-          read = xbt_getline(&line, &n, fp);
-          continue;
-        }
+  mc_time = xbt_new0(double, simix_process_maxpid);
 
-        /* Wipeout the new line character */
-        line[read - 1] = '\0';
-        
-        if(strlen(line) == 0){
-          read = xbt_getline(&line, &n, fp);
-          continue;
-        }
-      
-        xbt_dynar_free(&split);
-        xbt_str_rtrim(line, NULL);
-        xbt_str_strip_spaces(line);
-        split = xbt_str_split(line, " ");
-          
-        node_type = xbt_dynar_get_as(split, 1, char *);
+  /* mc_time refers to clock for each process -> ignore it for heap comparison */  
+  MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
 
-        if(strncmp(node_type, "DW_AT_", 6) != 0)
-          break;
+  /* Initialize the data structures that must be persistent across every
+     iteration of the model-checker (in RAW memory) */
+  
+  MC_SET_RAW_MEM;
 
-        if(strcmp(node_type, "DW_AT_sibling") == 0){
+  /* Initialize statistics */
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  mc_stats->state_size = 1;
 
-          subprogram_end = strdup(xbt_dynar_get_as(split, 3, char*));
-          xbt_str_ltrim(subprogram_end, "<0x");
-          xbt_str_rtrim(subprogram_end, ">");
-          
-        }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
-          
-          new_frame = 0;
-          abstract_origin = strdup(xbt_dynar_get_as(split, 2, char*));
-          xbt_str_ltrim(abstract_origin, "<0x");
-          xbt_str_rtrim(abstract_origin, ">");
-          subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
-          frame = xbt_dict_get_or_null(*all_variables, subprogram_name); 
-          xbt_free(abstract_origin);
+  /* Create exploration stack */
+  mc_stack_safety = xbt_fifo_new();
 
-        }else if(strcmp(node_type, "DW_AT_name") == 0){
+  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+    MC_init_dot_output();
 
-          new_frame = 1;
-          xbt_free(current_frame);
-          frame = xbt_new0(s_dw_frame_t, 1);
-          frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *)); 
-          frame->variables = xbt_dict_new_homogeneous(NULL);
-          frame->frame_base = xbt_new0(s_dw_location_t, 1); 
-          current_frame = strdup(frame->name);
+  MC_UNSET_RAW_MEM;
 
-          xbt_dict_set(subprograms_origin, subprogram_start, frame->name, NULL);
-        
-        }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
+  if(_sg_mc_visited > 0){
+    MC_init();
+  }else{
+    MC_SET_RAW_MEM;
+    MC_init_memory_map_info();
+    MC_get_libsimgrid_plt_section();
+    MC_get_binary_plt_section();
+    MC_UNSET_RAW_MEM;
+  }
 
-          location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
+  MC_dpor_init();
 
-          if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
-
-            frame->frame_base = get_location(location_list, xbt_dynar_get_as(split, 3, char *));
-             
-          }else{
-                
-            xbt_str_strip_spaces(line);
-            split2 = xbt_str_split(line, "(");
-            xbt_dynar_remove_at(split2, 0, NULL);
-            loc_expr = xbt_str_join(split2, " ");
-            xbt_str_rtrim(loc_expr, ")");
-            frame->frame_base = get_location(NULL, loc_expr);
-            xbt_dynar_free(&split2);
-            xbt_free(loc_expr);
+  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_UNSET_RAW_MEM;
 
-          }
-        }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
-          
-          if(frame != NULL)
-            frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
+  MC_dpor();
 
-        }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 
-          if(frame != NULL)
-            frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
+  xbt_abort();
+  //MC_exit();
+}
 
-        }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
+void MC_modelcheck_liveness(){
 
-          xbt_free(frame->name);
-          xbt_free(current_frame);
-          frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));   
-          current_frame = strdup(frame->name);
-          xbt_dict_set(subprograms_origin, subprogram_start, frame->name, NULL);
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-        }
+  MC_init();
 
-        read = xbt_getline(&line, &n, fp);
+  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));
  
-      if(new_frame == 1){
-        frame->start = strtoul(subprogram_start, NULL, 16);
-        if(subprogram_end != NULL)
-          frame->end = strtoul(subprogram_end, NULL, 16);
-        xbt_dict_set(*all_variables, frame->name, frame, NULL);
-      }
+  MC_SET_RAW_MEM;
+  /* Initialize statistics */
+  mc_stats = xbt_new0(s_mc_stats_t, 1);
+  mc_stats->state_size = 1;
 
-      xbt_free(subprogram_start);
-      xbt_free(subprogram_end);
-      subprogram_end = NULL;
-        
+  /* Create exploration stack */
+  mc_stack_liveness = xbt_fifo_new();
 
-    }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
+  /* Create the initial state */
+  initial_state_liveness = xbt_new0(s_mc_global_t, 1);
 
-      dw_local_variable_t var = NULL;
-      
-      strtok(xbt_dynar_get_as(split, 0, char *), "<");
-      origin = strdup(strtok(NULL, "<"));
-      xbt_str_rtrim(origin, ">:");
-      
-      read = xbt_getline(&line, &n, fp);
-      
-      while(read != -1){
+  if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
+    MC_init_dot_output();
+  
+  MC_UNSET_RAW_MEM;
 
-        if(n == 0){
-          read = xbt_getline(&line, &n, fp);
-          continue;
-        }
+  MC_ddfs_init();
 
-        /* Wipeout the new line character */
-        line[read - 1] = '\0'; 
+  /* We're done */
+  MC_print_statistics(mc_stats);
+  xbt_free(mc_time);
 
-        if(strlen(line) == 0){
-          read = xbt_getline(&line, &n, fp);
-          continue;
-        }
-       
-        xbt_dynar_free(&split);
-        xbt_str_rtrim(line, NULL);
-        xbt_str_strip_spaces(line);
-        split = xbt_str_split(line, " ");
-  
-        node_type = xbt_dynar_get_as(split, 1, char *);
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 
-        if(strncmp(node_type, "DW_AT_", 6) != 0)
-          break;
+}
 
-        if(strcmp(node_type, "DW_AT_name") == 0){
 
-          new_variable = 1;
-          var = xbt_new0(s_dw_local_variable_t, 1);
-          var->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
+void MC_exit(void)
+{
+  xbt_free(mc_time);
+  MC_memory_exit();
+  //xbt_abort();
+}
 
-          xbt_dict_set(variables_origin, origin, var->name, NULL);
-         
-        }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
+int SIMIX_pre_mc_random(smx_simcall_t simcall){
 
-          new_variable = 0;
-          abstract_origin = xbt_dynar_get_as(split, 2, char *);
-          xbt_str_ltrim(abstract_origin, "<0x");
-          xbt_str_rtrim(abstract_origin, ">");
-          
-          variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
-          variable_frame = get_frame_by_offset(*all_variables, strtoul(abstract_origin, NULL, 16));
-          var = xbt_dict_get_or_null(variable_frame->variables, variable_name);   
+  return simcall->mc_value;
+}
 
-        }else if(strcmp(node_type, "DW_AT_location") == 0){
 
-          if(valid_variable == 1 && var != NULL){
+int MC_random(void)
+{
+  /*FIXME: return mc_current_state->executed_transition->random.value;*/
+  return simcall_mc_random();
+}
 
-            var->location = xbt_new0(s_dw_location_t, 1);
+/**
+ * \brief Schedules all the process that are ready to run
+ */
+void MC_wait_for_requests(void)
+{
+  smx_process_t process;
+  smx_simcall_t req;
+  unsigned int iter;
 
-            location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
+  while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
+    SIMIX_process_runall();
+    xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
+      req = &process->simcall;
+      if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
+        SIMIX_simcall_pre(req, 0);
+    }
+  }
+}
 
-            if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
+int MC_deadlock_check()
+{
+  int deadlock = FALSE;
+  smx_process_t process;
+  if(xbt_swag_size(simix_global->process_list)){
+    deadlock = TRUE;
+    xbt_swag_foreach(process, simix_global->process_list){
+      if(process->simcall.call != SIMCALL_NONE
+         && MC_request_is_enabled(&process->simcall)){
+        deadlock = FALSE;
+        break;
+      }
+    }
+  }
+  return deadlock;
+}
 
-              var->location = get_location(location_list, xbt_dynar_get_as(split, 3, char *));
-             
-            }else{
-                
-              xbt_str_strip_spaces(line);
-              split2 = xbt_str_split(line, "(");
-              xbt_dynar_remove_at(split2, 0, NULL);
-              loc_expr = xbt_str_join(split2, " ");
-              xbt_str_rtrim(loc_expr, ")");
-              var->location = get_location(NULL, loc_expr);
-              xbt_dynar_free(&split2);
-              xbt_free(loc_expr);
+/**
+ * \brief Re-executes from the state at position start all the transitions indicated by
+ *        a given model-checker stack.
+ * \param stack The stack with the transitions to execute.
+ * \param start Start index to begin the re-execution.
+ */
+void MC_replay(xbt_fifo_t stack, int start)
+{
+  int raw_mem = (mmalloc_get_current_heap() == raw_heap);
 
-            }
+  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;
 
-          }
-           
-        }else if(strcmp(node_type, "DW_AT_external") == 0){
+  XBT_DEBUG("**** Begin Replay ****");
 
-          valid_variable = 0;
-        
-        }
+  if(start == -1){
+    /* Restore the initial state */
+    MC_restore_snapshot(initial_state_safety->snapshot);
+    /* At the moment of taking the snapshot the raw heap was set, so restoring
+     * it will set it back again, we have to unset it to continue  */
+    MC_UNSET_RAW_MEM;
+  }
 
-        read = xbt_getline(&line, &n, fp);
-      }
+  start_item = xbt_fifo_get_last_item(stack);
+  if(start != -1){
+    while (i != start){
+      start_item = xbt_fifo_get_prev_item(start_item);
+      i++;
+    }
+  }
 
-      if(new_variable == 1 && valid_variable == 1){
-        
-        variable_frame = xbt_dict_get_or_null(*all_variables, current_frame);
-        xbt_dict_set(variable_frame->variables, var->name, var, NULL);
-      }
+  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;
+  
 
-      valid_variable = 1;
-      new_variable = 0;
+  /* 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);
+       item = xbt_fifo_get_prev_item(item)) {
 
-    }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
+    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 */
+      req = &saved_req->issuer->simcall;
 
-      strtok(xbt_dynar_get_as(split, 0, char *), "<");
-      origin = strdup(strtok(NULL, "<"));
-      xbt_str_rtrim(origin, ">:");
+      /* Debug information */
+      if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+        req_str = MC_request_to_string(req, value);
+        XBT_DEBUG("Replay: %s (%p)", req_str, state);
+        xbt_free(req_str);
+      }
+    }
+    
+    SIMIX_simcall_pre(req, value);
+    MC_wait_for_requests();
 
-      read = xbt_getline(&line, &n, fp);
+    count++;
 
-      while(read != -1){
+    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++;
 
-        /* Wipeout the new line character */
-        line[read - 1] = '\0'; 
+  }
 
-        if(n == 0){
-          read = xbt_getline(&line, &n, fp);
-          continue;
-        }
+  XBT_DEBUG("**** End Replay ****");
 
-        if(strlen(line) == 0){
-          read = xbt_getline(&line, &n, fp);
-          continue;
-        }
+  if(raw_mem)
+    MC_SET_RAW_MEM;
+  else
+    MC_UNSET_RAW_MEM;
+  
 
-        xbt_dynar_free(&split);
-        xbt_str_rtrim(line, NULL);
-        xbt_str_strip_spaces(line);
-        split = xbt_str_split(line, " ");
-        
-        if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
-          break;
-          
-        node_type = xbt_dynar_get_as(split, 1, char *);
+}
 
-        if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
+void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
+{
 
-          origin = xbt_dynar_get_as(split, 2, char *);
-          xbt_str_ltrim(origin, "<0x");
-          xbt_str_rtrim(origin, ">");
-          
-          subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
-          subroutine_frame = xbt_dict_get_or_null(*all_variables, subprogram_name);
-        
-        }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
+  initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-          subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
+  int value;
+  char *req_str;
+  smx_simcall_t req = NULL, saved_req = NULL;
+  xbt_fifo_item_t item;
+  mc_state_t state;
+  mc_pair_t pair;
+  int depth = 1;
 
-        }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
+  XBT_DEBUG("**** Begin Replay ****");
 
-          subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
-        }
+  /* Restore the initial state */
+  MC_restore_snapshot(initial_state_liveness->snapshot);
 
-        read = xbt_getline(&line, &n, fp);
-      
-      }
+  /* At the moment of taking the snapshot the raw heap was set, so restoring
+   * it will set it back again, we have to unset it to continue  */
+  if(!initial_state_liveness->raw_mem_set)
+    MC_UNSET_RAW_MEM;
 
-    }else{
+  if(all_stack){
 
-      read = xbt_getline(&line, &n, fp);
+    item = xbt_fifo_get_last_item(stack);
 
-    }
+    while(depth <= xbt_fifo_size(stack)){
 
-  }
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+      state = (mc_state_t) pair->graph_state;
+
+      if(pair->requests > 0){
+   
+        saved_req = MC_state_get_executed_request(state, &value);
+        //XBT_DEBUG("SavedReq->call %u", saved_req->call);
+      
+        if(saved_req != NULL){
+          /* 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 */
+          req = &saved_req->issuer->simcall;
+          //XBT_DEBUG("Req->call %u", req->call);
   
-  xbt_dynar_free(&split);
-  xbt_free(line);
-  xbt_free(command);
-  pclose(fp);
+          /* Debug information */
+          if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+            req_str = MC_request_to_string(req, value);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }
   
-}
-
-static dw_location_t get_location(xbt_dict_t location_list, char *expr){
-
-  dw_location_t loc = xbt_new0(s_dw_location_t, 1);
+        }
+        SIMIX_simcall_pre(req, value);
+        MC_wait_for_requests();
+      }
 
-  if(location_list != NULL){
+      depth++;
     
-    char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
-    loc->type = e_dw_loclist;
-    loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
-    if(loc->location.loclist == NULL)
-      XBT_INFO("Key not found in loclist");
-    xbt_free(key);
-    return loc;
+      /* Update statistics */
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
 
-  }else{
+      item = xbt_fifo_get_prev_item(item);
+    }
 
-    int cursor = 0;
-    char *tok = NULL, *tok2 = NULL; 
-    
-    xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
-    xbt_dynar_t tokens2;
+  }else{
 
-    loc->type = e_dw_compose;
-    loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
+    /* Traverse the stack from the initial state and re-execute the transitions */
+    for (item = xbt_fifo_get_last_item(stack);
+         item != xbt_fifo_get_first_item(stack);
+         item = xbt_fifo_get_prev_item(item)) {
 
-    while(cursor < xbt_dynar_length(tokens1)){
+      pair = (mc_pair_t) xbt_fifo_get_item_content(item);
+      state = (mc_state_t) pair->graph_state;
 
-      tok = xbt_dynar_get_as(tokens1, cursor, char*);
-      tokens2 = xbt_str_split(tok, " ");
-      tok2 = xbt_dynar_get_as(tokens2, 0, char*);
+      if(pair->requests > 0){
+   
+        saved_req = MC_state_get_executed_request(state, &value);
+        //XBT_DEBUG("SavedReq->call %u", saved_req->call);
       
-      if(strncmp(tok2, "DW_OP_reg", 9) == 0){
-        dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
-        new_element->type = e_dw_register;
-        new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
-        xbt_dynar_push(loc->location.compose, &new_element);     
-      }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, 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, 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);
-        new_element->type = e_dw_lit;
-        new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }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, 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
-        new_element->location.piece = xbt_dynar_get_as(tokens2, 1, char*)[0] - '0';*/
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }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, 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 ||
-               strcmp(tok, "DW_OP_div") == 0 ||
-               strcmp(tok, "DW_OP_minus") == 0 ||
-               strcmp(tok, "DW_OP_mod") == 0 ||
-               strcmp(tok, "DW_OP_mul") == 0 ||
-               strcmp(tok, "DW_OP_neg") == 0 ||
-               strcmp(tok, "DW_OP_not") == 0 ||
-               strcmp(tok, "DW_OP_or") == 0 ||
-               strcmp(tok, "DW_OP_plus") == 0){               
-        dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
-        new_element->type = e_dw_arithmetic;
-        new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }else if(strcmp(tok, "DW_OP_stack_value") == 0){
-      }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, 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
-        new_element->location.deref_size = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';*/
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }else if(strcmp(tok, "DW_OP_deref") == 0){
-        dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
-        new_element->type = e_dw_deref;
-        new_element->location.deref_size = sizeof(void *);
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }else if(strcmp(tok2, "DW_OP_constu:") == 0){
-        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, 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
-        new_element->location.uconstant.value = (unsigned long int)(xbt_dynar_get_as(tokens, cursor, char*)[0] - '0');*/
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }else if(strcmp(tok2, "DW_OP_consts:") == 0){
-        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, 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 ||
-               strcmp(tok2, "DW_OP_const4u:") == 0 ||
-               strcmp(tok2, "DW_OP_const8u:") == 0){
-        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, 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
-        new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0';*/
-        xbt_dynar_push(loc->location.compose, &new_element);
-      }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
-               strcmp(tok, "DW_OP_const2s") == 0 ||
-               strcmp(tok, "DW_OP_const4s") == 0 ||
-               strcmp(tok, "DW_OP_const8s") == 0){
-        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, 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);
-        new_element->type = e_dw_unsupported;
-        xbt_dynar_push(loc->location.compose, &new_element);
+        if(saved_req != NULL){
+          /* 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 */
+          req = &saved_req->issuer->simcall;
+          //XBT_DEBUG("Req->call %u", req->call);
+  
+          /* Debug information */
+          if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
+            req_str = MC_request_to_string(req, value);
+            XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
+            xbt_free(req_str);
+          }
+  
+        }
+        SIMIX_simcall_pre(req, value);
+        MC_wait_for_requests();
       }
 
-      cursor++;
-      xbt_dynar_free(&tokens2);
-
-    }
+      depth++;
     
-    xbt_dynar_free(&tokens1);
+      /* Update statistics */
+      mc_stats->visited_pairs++;
+      mc_stats->executed_transitions++;
+    }
+  }  
+
+  XBT_DEBUG("**** End Replay ****");
+
+  if(initial_state_liveness->raw_mem_set)
+    MC_SET_RAW_MEM;
+  else
+    MC_UNSET_RAW_MEM;
+  
+}
+
+/**
+ * \brief Dumps the contents of a model-checker's stack and shows the actual
+ *        execution trace
+ * \param stack The stack to dump
+ */
+void MC_dump_stack_safety(xbt_fifo_t stack)
+{
+  
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_show_stack_safety(stack);
+
+  if(!_sg_mc_checkpoint){
+
+    mc_state_t state;
+
+    MC_SET_RAW_MEM;
+    while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
+      MC_state_delete(state);
+    MC_UNSET_RAW_MEM;
 
-    return loc;
-    
   }
 
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+  else
+    MC_UNSET_RAW_MEM;
+  
 }
 
 
-void print_local_variables(xbt_dict_t list){
+void MC_show_stack_safety(xbt_fifo_t stack)
+{
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
+  int value;
+  mc_state_t state;
+  xbt_fifo_item_t item;
+  smx_simcall_t req;
+  char *req_str = NULL;
   
-  dw_location_entry_t entry;
-  dw_location_t location_entry;
-  unsigned int cursor3 = 0, cursor4 = 0;
-  xbt_dict_cursor_t cursor = 0, cursor2 = 0;
-
-  char *frame_name, *variable_name;
-  dw_frame_t current_frame;
-  dw_local_variable_t current_variable;
-
-  xbt_dict_foreach(list, cursor, frame_name, current_frame){ 
-    fprintf(stderr, "Frame name : %s\n", current_frame->name);
-    fprintf(stderr, "Location type : %d\n", current_frame->frame_base->type);
-    xbt_dict_foreach((xbt_dict_t)current_frame->variables, cursor2, variable_name, current_variable){
-      fprintf(stderr, "Name : %s\n", current_variable->name);
-      if(current_variable->location == NULL)
-        continue;
-      fprintf(stderr, "Location type : %d\n", current_variable->location->type);
-      switch(current_variable->location->type){
-      case e_dw_loclist :
-        xbt_dynar_foreach(current_variable->location->location.loclist, cursor3, entry){
-          fprintf(stderr, "Lowpc : %lx, Highpc : %lx,", entry->lowpc, entry->highpc);
-          switch(entry->location->type){
-          case e_dw_register :
-            fprintf(stderr, " Location : in register %d\n", entry->location->location.reg);
-            break;
-          case e_dw_bregister_op:
-            fprintf(stderr, " Location : Add %d to the value in register %d\n", entry->location->location.breg_op.offset, entry->location->location.breg_op.reg);
-            break;
-          case e_dw_lit:
-            fprintf(stderr, "Value already kwnown : %d\n", entry->location->location.lit);
-            break;
-          case e_dw_fbregister_op:
-            fprintf(stderr, " Location : %d bytes from logical frame pointer\n", entry->location->location.fbreg_op);
-            break;
-          case e_dw_compose:
-            fprintf(stderr, " Location :\n");
-            xbt_dynar_foreach(entry->location->location.compose, cursor4, location_entry){
-              switch(location_entry->type){
-              case e_dw_register :
-                fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
-                break;
-              case e_dw_bregister_op:
-                fprintf(stderr, " %d) add %d to the value in register %d\n", cursor4 + 1, location_entry->location.breg_op.offset, location_entry->location.breg_op.reg);
-                break;
-              case e_dw_lit:
-                fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
-                break;
-              case e_dw_fbregister_op:
-                fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
-                break;
-              case e_dw_deref:
-                fprintf(stderr, " %d) Pop the stack entry and treats it as an address (size of data %d)\n", cursor4 + 1, location_entry->location.deref_size);
-                break;
-              case e_dw_arithmetic :
-                fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
-                break;
-              case e_dw_piece:
-                fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
-                break;
-              case e_dw_uconstant :
-                fprintf(stderr, "%d) Unsigned constant %lu\n", cursor4 + 1, location_entry->location.uconstant.value);
-                break;
-              case e_dw_sconstant :
-                fprintf(stderr, "%d) Signed constant %lu\n", cursor4 + 1, location_entry->location.sconstant.value);
-                break;
-              default :
-                fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
-                break;
-              }
-            }
-            break;
-          default:
-            fprintf(stderr, "Location type not supported\n");
-            break;
-          }
-        }
-        break;
-      case e_dw_compose:
-        cursor4 = 0;
-        fprintf(stderr, "Location :\n");
-        xbt_dynar_foreach(current_variable->location->location.compose, cursor4, location_entry){
-          switch(location_entry->type){
-          case e_dw_register :
-            fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg);
-            break;
-          case e_dw_bregister_op:
-            fprintf(stderr, " %d) add %d to the value in register %d\n", cursor4 + 1, location_entry->location.breg_op.offset, location_entry->location.breg_op.reg);
-            break;
-          case e_dw_lit:
-            fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit);
-            break;
-          case e_dw_fbregister_op:
-            fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op);
-            break;
-          case e_dw_deref:
-            fprintf(stderr, " %d) Pop the stack entry and treats it as an address (size of data %d)\n", cursor4 + 1, location_entry->location.deref_size);
-            break;
-          case e_dw_arithmetic :
-            fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic);
-            break;
-          case e_dw_piece:
-            fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece);
-            break;
-          case e_dw_uconstant :
-            fprintf(stderr, "%d) Unsigned constant %lu\n", cursor4 + 1, location_entry->location.uconstant.value);
-            break;
-          case e_dw_sconstant :
-            fprintf(stderr, "%d) Signed constant %lu\n", cursor4 + 1, location_entry->location.sconstant.value);
-            break;
-          default :
-            fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1);
-            break;
-          }
-        }
-        break;
-      default :
-        fprintf(stderr, "Location type not supported\n");
-        break;
-      }
+  for (item = xbt_fifo_get_last_item(stack);
+       (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
+        : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+    req = MC_state_get_executed_request(state, &value);
+    if(req){
+      req_str = MC_request_to_string(req, value);
+      XBT_INFO("%s", req_str);
+      xbt_free(req_str);
     }
   }
 
+  if(!raw_mem_set)
+    MC_UNSET_RAW_MEM;
 }
 
-static void MC_get_global_variables(char *elf_file){
-
-  FILE *fp;
-
-  char *command = bprintf("objdump -t -j .data -j .bss %s", elf_file);
+void MC_show_deadlock(smx_simcall_t req)
+{
+  /*char *req_str = NULL;*/
+  XBT_INFO("**************************");
+  XBT_INFO("*** DEAD-LOCK DETECTED ***");
+  XBT_INFO("**************************");
+  XBT_INFO("Locked request:");
+  /*req_str = MC_request_to_string(req);
+    XBT_INFO("%s", req_str);
+    xbt_free(req_str);*/
+  XBT_INFO("Counter-example execution trace:");
+  MC_dump_stack_safety(mc_stack_safety);
+  MC_print_statistics(mc_stats);
+}
 
-  fp = popen(command, "r");
 
-  if(fp == NULL){
-    perror("popen failed");
-    xbt_abort();
+void MC_show_stack_liveness(xbt_fifo_t stack){
+  int value;
+  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_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){
+      if(pair->requests>0){
+        req_str = MC_request_to_string(req, value);
+        XBT_INFO("%s", req_str);
+        xbt_free(req_str);
+      }else{
+        XBT_INFO("End of system requests but evolution in Büchi automaton");
+      }
+    }
   }
+}
 
-  if(mc_global_variables == NULL)
-    mc_global_variables = xbt_dynar_new(sizeof(global_variable_t), global_variable_free_voidp);
+void MC_dump_stack_liveness(xbt_fifo_t stack){
 
-  char *line = NULL;
-  ssize_t read;
-  size_t n = 0;
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-  xbt_dynar_t line_tokens = NULL;
-  unsigned long offset;
+  mc_pair_t pair;
 
-  int type = strcmp(elf_file, xbt_binary_name); /* 0 = binary, other = libsimgrid */
+  MC_SET_RAW_MEM;
+  while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
+    MC_pair_delete(pair);
+  MC_UNSET_RAW_MEM;
 
-  while ((read = xbt_getline(&line, &n, fp)) != -1){
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 
-    if(n == 0)
-      continue;
+}
 
-     /* Wipeout the new line character */
-    line[read - 1] = '\0';
 
-    xbt_str_strip_spaces(line);
-    xbt_str_ltrim(line, NULL);
+void MC_print_statistics(mc_stats_t stats)
+{
+  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);
+  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;
+}
 
-    line_tokens = xbt_str_split(line, NULL);
+void MC_assert(int prop)
+{
+  if (MC_is_active() && !prop){
+    XBT_INFO("**************************");
+    XBT_INFO("*** PROPERTY NOT VALID ***");
+    XBT_INFO("**************************");
+    XBT_INFO("Counter-example execution trace:");
+    MC_dump_stack_safety(mc_stack_safety);
+    MC_print_statistics(mc_stats);
+    xbt_abort();
+  }
+}
 
-    if(xbt_dynar_length(line_tokens) <= 4 || strcmp(xbt_dynar_get_as(line_tokens, 0, char *), "SYMBOL") == 0)
-      continue;
+void MC_max_depth(int max_depth){
+  user_max_depth_reached = max_depth;
+}
 
-    if((strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "__gcov", 6) == 0)
-       || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "gcov", 4) == 0)
-       || (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)
-       || ((size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16) == 0))
-      continue;
+void MC_process_clock_add(smx_process_t process, double amount)
+{
+  mc_time[process->pid] += amount;
+}
 
-    global_variable_t var = xbt_new0(s_global_variable_t, 1);
+double MC_process_clock_get(smx_process_t process)
+{
+  if(mc_time){
+    if(process != NULL)
+      return mc_time[process->pid];
+    else 
+      return -1;
+  }else{
+    return 0;
+  }
+}
 
-    if(type == 0){
-      var->address = (void *)strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16);
-    }else{
-      offset = strtoul(xbt_dynar_get_as(line_tokens, 0, char*), NULL, 16);
-      var->address = (char *)start_text_libsimgrid+offset;
-    }
+void MC_automaton_load(const char *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*));
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
 
-    if(data_bss_ignore_size(var->address) > 0){
-      global_variable_free(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);
-      }
-    }
+  MC_SET_RAW_MEM;
 
-    xbt_dynar_free(&line_tokens);
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+  
+  xbt_automaton_load(_mc_property_automaton,file);
 
-  }
+  MC_UNSET_RAW_MEM;
 
-  xbt_free(command);
-  xbt_free(line);
-  pclose(fp);
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
 
 }
 
-void global_variable_free(global_variable_t v){
-  xbt_free(v->name);
-  xbt_free(v);
-}
+void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
+
+  int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+  MC_SET_RAW_MEM;
+
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+
+  xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
 
-void global_variable_free_voidp(void *v){
-  global_variable_free((global_variable_t) * (void **) v);
+  MC_UNSET_RAW_MEM;
+
+  if(raw_mem_set)
+    MC_SET_RAW_MEM;
+  
 }
+
+
+
index a348722..f5bd47d 100644 (file)
@@ -46,8 +46,9 @@ typedef struct s_mc_snapshot{
 } s_mc_snapshot_t, *mc_snapshot_t;
 
 typedef struct s_mc_snapshot_stack{
-  xbt_strbuff_t local_variables;
+  xbt_dynar_t local_variables;
   void *stack_pointer;
+  void *real_address;
 }s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
 
 typedef struct s_mc_global_t{
@@ -61,8 +62,6 @@ mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
 mc_snapshot_t MC_take_snapshot(void);
 void MC_restore_snapshot(mc_snapshot_t);
 void MC_free_snapshot(mc_snapshot_t);
-void snapshot_stack_free_voidp(void *s);
-int is_stack_ignore_variable(char *frame, char *var_name);
 
 /********************************* MC Global **********************************/
 
@@ -78,7 +77,6 @@ void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
 void MC_init(void);
-void MC_init_dot_output(void);
 int SIMIX_pre_mc_random(smx_simcall_t simcall);
 
 
@@ -206,16 +204,17 @@ typedef struct s_memory_map {
 
 
 void MC_init_memory_map_info(void);
-memory_map_t get_memory_map(void);
-void free_memory_map(memory_map_t map);
-void get_libsimgrid_plt_section(void);
-void get_binary_plt_section(void);
+memory_map_t MC_get_memory_map(void);
+void MC_free_memory_map(memory_map_t map);
+void MC_get_libsimgrid_plt_section(void);
+void MC_get_binary_plt_section(void);
 
 extern void *start_data_libsimgrid;
 extern void *start_data_binary;
 extern void *start_bss_binary;
 extern char *libsimgrid_path;
 extern void *start_text_libsimgrid;
+extern void *start_text_binary;
 extern void *start_bss_libsimgrid;
 extern void *start_plt_libsimgrid;
 extern void *end_plt_libsimgrid;
@@ -308,7 +307,14 @@ void MC_show_stack_liveness(xbt_fifo_t stack);
 void MC_dump_stack_liveness(xbt_fifo_t stack);
 
 
-/********************************** Local variables with DWARF **********************************/
+/********************************** Variables with DWARF **********************************/
+
+extern xbt_dict_t mc_local_variables_libsimgrid;
+extern xbt_dict_t mc_local_variables_binary;
+extern xbt_dynar_t mc_global_variables_libsimgrid;
+extern xbt_dynar_t mc_global_variables_binary;
+extern xbt_dict_t mc_variables_type_libsimgrid;
+extern xbt_dict_t mc_variables_type_binary;
 
 typedef enum {
   e_dw_loclist,
@@ -372,53 +378,36 @@ typedef struct s_dw_location_entry{
   dw_location_t location;
 }s_dw_location_entry_t, *dw_location_entry_t;
 
-typedef struct s_dw_local_variable{
+typedef struct s_dw_variable{
+  int global;
   char *name;
-  dw_location_t location;
-}s_dw_local_variable_t, *dw_local_variable_t;
+  char *type_origin;
+  union{
+    dw_location_t location;
+    void *address;
+  }address;
+}s_dw_variable_t, *dw_variable_t;
 
 typedef struct s_dw_frame{
   char *name;
   void *low_pc;
   void *high_pc;
   dw_location_t frame_base;
-  xbt_dict_t variables;
+  xbt_dynar_t variables; /* Cannot use dict, there may be several variables with the same name (in different lexical blocks)*/
   unsigned long int start;
   unsigned long int end;
 }s_dw_frame_t, *dw_frame_t;
 
-/* FIXME : implement free functions for each structure */
-
-extern xbt_dict_t mc_local_variables;
-
-typedef struct s_variable_value{
-  char *type;
-  
-  union{
-    void *address;
-    long int res;
-  }value;
-}s_variable_value_t, *variable_value_t;
-
-void variable_value_free_voidp(void* v);
-void variable_value_free(variable_value_t v);
-
-void MC_get_local_variables(const char *elf_file, xbt_dict_t location_list, xbt_dict_t *variables);
-void print_local_variables(xbt_dict_t list);
-xbt_dict_t MC_get_location_list(const char *elf_file);
-
+/********************************** Miscellaneous **********************************/
 
-/********************************** Global variables with objdump **********************************/
-
-typedef struct s_global_variable{
+typedef struct s_local_variable{
+  char *frame;
+  unsigned long ip;
   char *name;
-  size_t size;
+  char *type;
   void *address;
-}s_global_variable_t, *global_variable_t;
-
-void global_variable_free(global_variable_t v);
-void global_variable_free_voidp(void *v);
-
-extern xbt_dynar_t mc_global_variables;
+  int region;
+}s_local_variable_t, *local_variable_t;
 
 #endif
+
index 04538dd..b582b32 100644 (file)
@@ -9,7 +9,7 @@
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_memory_map, mc,
                                 "Logging specific to algorithms for memory_map");
 
-memory_map_t get_memory_map(void)
+memory_map_t MC_get_memory_map(void)
 {
   FILE *fp;                     /* File pointer to process's proc maps file */
   char *line = NULL;            /* Temporal storage for each line that is readed */
@@ -155,7 +155,7 @@ memory_map_t get_memory_map(void)
   return ret;
 }
 
-void free_memory_map(memory_map_t map){
+void MC_free_memory_map(memory_map_t map){
 
   int i;
   for(i=0; i< map->mapsize; i++){
index 7c6239a..2b1a2a4 100644 (file)
@@ -5,7 +5,6 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "msg_private.h"
-#include "mc/mc.h"
 
 #include "msg/datatypes.h"
 #include "simix/smx_process_private.h"
@@ -33,9 +32,6 @@ void TRACE_msg_process_change_host(msg_process_t process, msg_host_t old_host, m
   if (TRACE_msg_process_is_enabled()){
     static long long int counter = 0;
 
-    if(MC_is_active())
-      MC_ignore_data_bss(&counter, sizeof(counter));
-
     char key[INSTR_DEFAULT_STR_SIZE];
     snprintf (key, INSTR_DEFAULT_STR_SIZE, "%lld", counter++);
 
index 52acde4..d87fa85 100644 (file)
@@ -39,10 +39,8 @@ void TRACE_msg_task_create(msg_task_t task)
   task->counter = counter++;
   task->category = NULL;
   
-  if(MC_is_active()){
-    MC_ignore_data_bss(&counter, sizeof(counter));
+  if(MC_is_active())
     MC_ignore_heap(&(task->counter), sizeof(task->counter));
-  }
 
   XBT_DEBUG("CREATE %p, %lld", task, task->counter);
 }
index 3be4eb5..d51abb9 100644 (file)
@@ -31,7 +31,7 @@ void SIMIX_network_init(void)
 {
   rdv_points = xbt_dict_new_homogeneous(SIMIX_rdv_free);
   if(MC_is_active())
-    MC_ignore_data_bss(&smx_total_comms, sizeof(smx_total_comms));
+    MC_ignore_global_variable("smx_total_comms", 1);
 }
 
 void SIMIX_network_exit(void)
index dca11e4..e5a163b 100644 (file)
@@ -5,7 +5,6 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "private.h"
-#include "mc/mc.h"
 #include <ctype.h>
 #include <wchar.h>
 
@@ -88,9 +87,6 @@ static char *TRACE_smpi_put_key(int src, int dst, char *key, int n)
   }
   //generate the key
   static unsigned long long counter = 0;
-  
-  if(MC_is_active())
-    MC_ignore_data_bss(&counter, sizeof(counter));
 
   snprintf(key, n, "%d_%d_%llu", src, dst, counter++);
 
index 88c5596..63b2100 100644 (file)
@@ -5,7 +5,6 @@
   * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include "instr/instr_private.h"
-#include "mc/mc.h"
 
 #ifdef HAVE_TRACING
 #include "surf/surf_private.h"
@@ -117,9 +116,6 @@ static void linkContainers (container_t src, container_t dst, xbt_dict_t filter)
   //create the link
   static long long counter = 0;
 
-  if(MC_is_active())
-    MC_ignore_data_bss(&counter, sizeof(counter));
-
   char key[INSTR_DEFAULT_STR_SIZE];
   snprintf (key, INSTR_DEFAULT_STR_SIZE, "%lld", counter++);
   new_pajeStartLink(SIMIX_get_clock(), father, link_type, src, "topology", key);
index adf6b2e..819b161 100644 (file)
@@ -9,6 +9,7 @@
 #include "xbt/str.h"
 #include "mc/mc.h"
 #include "xbt/mmalloc.h"
+#include "mc/datatypes.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mm_diff, xbt,
                                 "Logging specific to mm_diff in mmalloc");
@@ -17,22 +18,11 @@ xbt_dynar_t mc_heap_comparison_ignore;
 xbt_dynar_t stacks_areas;
 void *maestro_stack_start, *maestro_stack_end;
 
-static void heap_area_pair_free(heap_area_pair_t pair);
-static void heap_area_pair_free_voidp(void *d);
-static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2);
-static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2);
-static heap_area_t new_heap_area(int block, int fragment);
 
-static size_t heap_comparison_ignore_size(xbt_dynar_t list, void *address);
-static void add_heap_equality(xbt_dynar_t equals, void *a1, void *a2);
-static void remove_heap_equality(xbt_dynar_t equals, int address, void *a);
+/********************************* Backtrace ***********************************/
+/******************************************************************************/
 
-static int is_stack(void *address);
-static int is_block_stack(int block);
-static int equal_blocks(int b1, int b2);
-static int equal_fragments(int b1, int f1, int b2, int f2);
-
-void mmalloc_backtrace_block_display(void* heapinfo, int block){
+static void mmalloc_backtrace_block_display(void* heapinfo, int block){
 
   /* xbt_ex_t e; */
 
@@ -59,7 +49,7 @@ void mmalloc_backtrace_block_display(void* heapinfo, int block){
   /* } */
 }
 
-void mmalloc_backtrace_fragment_display(void* heapinfo, int block, int frag){
+static void mmalloc_backtrace_fragment_display(void* heapinfo, int block, int frag){
 
   /* xbt_ex_t e; */
 
@@ -82,7 +72,7 @@ void mmalloc_backtrace_fragment_display(void* heapinfo, int block, int frag){
 
 }
 
-void mmalloc_backtrace_display(void *addr){
+static void mmalloc_backtrace_display(void *addr){
 
   /* size_t block, frag_nb; */
   /* int type; */
@@ -113,11 +103,204 @@ void mmalloc_backtrace_display(void *addr){
 }
 
 
+static int compare_backtrace(int b1, int f1, int b2, int f2){
+  /*int i = 0;
+  if(f1 != -1){
+    for(i=0; i< XBT_BACKTRACE_SIZE; i++){
+      if(heapinfo1[b1].busy_frag.bt[f1][i] != heapinfo2[b2].busy_frag.bt[f2][i]){
+        //mmalloc_backtrace_fragment_display((void*)heapinfo1, b1, f1);
+        //mmalloc_backtrace_fragment_display((void*)heapinfo2, b2, f2);
+        return 1;
+      }
+    }
+  }else{
+    for(i=0; i< heapinfo1[b1].busy_block.bt_size; i++){
+      if(heapinfo1[b1].busy_block.bt[i] != heapinfo2[b2].busy_block.bt[i]){
+        //mmalloc_backtrace_block_display((void*)heapinfo1, b1);
+        //mmalloc_backtrace_block_display((void*)heapinfo2, b2);
+        return 1;
+      }
+    }
+    }*/
+  return 0;
+}
+
+
+/*********************************** Heap comparison ***********************************/
+/***************************************************************************************/
+
 void *s_heap = NULL, *heapbase1 = NULL, *heapbase2 = NULL;
 malloc_info *heapinfo1 = NULL, *heapinfo2 = NULL;
 size_t heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
 xbt_dynar_t to_ignore1 = NULL, to_ignore2 = NULL;
 
+/*********************************** Free functions ************************************/
+
+static void heap_area_pair_free(heap_area_pair_t pair){
+  xbt_free(pair);
+  pair = NULL;
+}
+
+static void heap_area_pair_free_voidp(void *d){
+  heap_area_pair_free((heap_area_pair_t) * (void **) d);
+}
+
+/************************************************************************************/
+
+static heap_area_t new_heap_area(int block, int fragment){
+  heap_area_t area = NULL;
+  area = xbt_new0(s_heap_area_t, 1);
+  area->block = block;
+  area->fragment = fragment;
+  return area;
+}
+
+static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2){
+  
+  unsigned int cursor = 0;
+  heap_area_pair_t current_pair;
+
+  xbt_dynar_foreach(list, cursor, current_pair){
+    if(current_pair->block1 == block1 && current_pair->block2 == block2 && current_pair->fragment1 == fragment1 && current_pair->fragment2 == fragment2)
+      return 0; 
+  }
+  
+  return 1;
+}
+
+static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2){
+
+  if(is_new_heap_area_pair(list, block1, fragment1, block2, fragment2)){
+    heap_area_pair_t pair = NULL;
+    pair = xbt_new0(s_heap_area_pair_t, 1);
+    pair->block1 = block1;
+    pair->fragment1 = fragment1;
+    pair->block2 = block2;
+    pair->fragment2 = fragment2;
+    
+    xbt_dynar_push(list, &pair); 
+
+    return 1;
+  }
+
+  return 0;
+}
+
+static size_t heap_comparison_ignore_size(xbt_dynar_t ignore_list, void *address){
+
+  unsigned int cursor = 0;
+  int start = 0;
+  int end = xbt_dynar_length(ignore_list) - 1;
+  mc_heap_ignore_region_t region;
+
+  while(start <= end){
+    cursor = (start + end) / 2;
+    region = (mc_heap_ignore_region_t)xbt_dynar_get_as(ignore_list, cursor, mc_heap_ignore_region_t);
+    if(region->address == address)
+      return region->size;
+    if(region->address < address)
+      start = cursor + 1;
+    if(region->address > address)
+      end = cursor - 1;   
+  }
+
+  return 0;
+}
+
+static int is_stack(void *address){
+  unsigned int cursor = 0;
+  stack_region_t stack;
+
+  xbt_dynar_foreach(stacks_areas, cursor, stack){
+    if(address == stack->address)
+      return 1;
+  }
+
+  return 0;
+}
+
+static int is_block_stack(int block){
+  unsigned int cursor = 0;
+  stack_region_t stack;
+
+  xbt_dynar_foreach(stacks_areas, cursor, stack){
+    if(block == stack->block)
+      return 1;
+  }
+
+  return 0;
+}
+
+static void match_equals(xbt_dynar_t list){
+
+  unsigned int cursor = 0;
+  heap_area_pair_t current_pair;
+  heap_area_t previous_area;
+
+  xbt_dynar_foreach(list, cursor, current_pair){
+
+    if(current_pair->fragment1 != -1){
+      
+      if(heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1] != NULL){    
+        previous_area = heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1];
+        xbt_free(heapinfo2[previous_area->block].busy_frag.equal_to[previous_area->fragment]);
+        heapinfo2[previous_area->block].busy_frag.equal_to[previous_area->fragment] = NULL;
+        xbt_free(previous_area); 
+      }
+      if(heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2] != NULL){        
+        previous_area = heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2];
+        xbt_free(heapinfo1[previous_area->block].busy_frag.equal_to[previous_area->fragment]);
+        heapinfo1[previous_area->block].busy_frag.equal_to[previous_area->fragment] = NULL;
+        xbt_free(previous_area);
+      }
+
+      heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1] = new_heap_area(current_pair->block2, current_pair->fragment2);
+      heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2] = new_heap_area(current_pair->block1, current_pair->fragment1);
+      
+    }else{
+
+      if(heapinfo1[current_pair->block1].busy_block.equal_to != NULL){
+        previous_area = heapinfo1[current_pair->block1].busy_block.equal_to;
+        xbt_free(heapinfo2[previous_area->block].busy_block.equal_to);
+        heapinfo2[previous_area->block].busy_block.equal_to = NULL; 
+        xbt_free(previous_area);
+      }
+      if(heapinfo2[current_pair->block2].busy_block.equal_to != NULL){
+        previous_area = heapinfo2[current_pair->block2].busy_block.equal_to;
+        xbt_free(heapinfo1[previous_area->block].busy_block.equal_to);
+        heapinfo1[previous_area->block].busy_block.equal_to = NULL;
+        xbt_free(previous_area);
+      }
+
+      heapinfo1[current_pair->block1].busy_block.equal_to = new_heap_area(current_pair->block2, current_pair->fragment2);
+      heapinfo2[current_pair->block2].busy_block.equal_to = new_heap_area(current_pair->block1, current_pair->fragment1);
+
+    }
+
+  }
+}
+
+static int equal_blocks(int b1, int b2){
+  if(heapinfo1[b1].busy_block.equal_to != NULL){
+    if(heapinfo2[b2].busy_block.equal_to != NULL){
+      if(((heap_area_t)(heapinfo1[b1].busy_block.equal_to))->block == b2 && ((heap_area_t)(heapinfo2[b2].busy_block.equal_to))->block == b1)
+        return 1;
+    }
+  }
+  return 0;
+}
+
+static int equal_fragments(int b1, int f1, int b2, int f2){
+  if(heapinfo1[b1].busy_frag.equal_to[f1] != NULL){
+    if(heapinfo2[b2].busy_frag.equal_to[f2] != NULL){
+      if(((heap_area_t)(heapinfo1[b1].busy_frag.equal_to[f1]))->block == b2 && ((heap_area_t)(heapinfo2[b2].busy_frag.equal_to[f2]))->block == b1 && ((heap_area_t)(heapinfo1[b1].busy_frag.equal_to[f1]))->fragment == f2 && ((heap_area_t)(heapinfo2[b2].busy_frag.equal_to[f2]))->fragment == f1)
+        return 1;
+    }
+  }
+  return 0;
+}
+
 void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1, xbt_dynar_t i2){
 
   heaplimit = ((struct mdesc *)heap1)->heaplimit;
@@ -137,17 +320,59 @@ void init_heap_information(xbt_mheap_t heap1, xbt_mheap_t heap2, xbt_dynar_t i1,
   to_ignore2 = i2;
 
   if(MC_is_active()){
-    MC_ignore_data_bss(&heaplimit, sizeof(heaplimit));
-    MC_ignore_data_bss(&s_heap, sizeof(s_heap));
-    MC_ignore_data_bss(&heapbase1, sizeof(heapbase1));
-    MC_ignore_data_bss(&heapbase2, sizeof(heapbase2));
-    MC_ignore_data_bss(&heapinfo1, sizeof(heapinfo1));
-    MC_ignore_data_bss(&heapinfo2, sizeof(heapinfo2));
-    MC_ignore_data_bss(&heapsize1, sizeof(heapsize1));
-    MC_ignore_data_bss(&heapsize2, sizeof(heapsize2));
-    MC_ignore_data_bss(&to_ignore1, sizeof(to_ignore1));
-    MC_ignore_data_bss(&to_ignore2, sizeof(to_ignore2));
+    MC_ignore_global_variable("heaplimit", 1);
+    MC_ignore_global_variable("s_heap", 1);
+    MC_ignore_global_variable("heapbase1", 1);
+    MC_ignore_global_variable("heapbase2", 1);
+    MC_ignore_global_variable("heapinfo1", 1);
+    MC_ignore_global_variable("heapinfo2", 1);
+    MC_ignore_global_variable("heapsize1", 1);
+    MC_ignore_global_variable("heapsize2", 1);
+    MC_ignore_global_variable("to_ignore1", 1);
+    MC_ignore_global_variable("to_ignore2", 1);
+  }
+
+}
+
+void reset_heap_information(){
+
+  size_t i = 0, j;
+
+  while(i<=heaplimit){
+    if(heapinfo1[i].type == 0){
+      xbt_free(heapinfo1[i].busy_block.equal_to);
+      heapinfo1[i].busy_block.equal_to = NULL;
+    }
+    if(heapinfo1[i].type > 0){
+      for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo1[i].type); j++){
+        xbt_free(heapinfo1[i].busy_frag.equal_to[j]);
+        heapinfo1[i].busy_frag.equal_to[j] = NULL;
+      }
+    }
+    i++; 
+  }
+
+  i = 0;
+
+  while(i<=heaplimit){
+    if(heapinfo2[i].type == 0){
+      xbt_free(heapinfo2[i].busy_block.equal_to);
+      heapinfo2[i].busy_block.equal_to = NULL;
+    }
+    if(heapinfo2[i].type > 0){
+      for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo2[i].type); j++){
+        xbt_free(heapinfo2[i].busy_frag.equal_to[j]);
+        heapinfo2[i].busy_frag.equal_to[j] = NULL;
+      }
+    }
+    i++; 
   }
+
+  s_heap = NULL, heapbase1 = NULL, heapbase2 = NULL;
+  heapinfo1 = NULL, heapinfo2 = NULL;
+  heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
+  to_ignore1 = NULL, to_ignore2 = NULL;
+
 }
 
 int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
@@ -215,7 +440,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
         
           addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
         
-          res_compare = compare_area(addr_block1, addr_block2, NULL);
+          res_compare = compare_heap_area(addr_block1, addr_block2, NULL, NULL, NULL, NULL, 0); /*FIXME*/
         
           if(res_compare == 0){
             for(k=1; k < heapinfo2[current_block].busy_block.size; k++)
@@ -251,7 +476,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
           continue;
         }
           
-        res_compare = compare_area(addr_block1, addr_block2, NULL);
+        res_compare = compare_heap_area(addr_block1, addr_block2, NULL, NULL, NULL, NULL, 0); /*FIXME */
         
         if(res_compare == 0){
           for(k=1; k < heapinfo2[i2].busy_block.size; k++)
@@ -269,10 +494,10 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
       }
 
       if(!equal){
-        /*XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1, heapinfo1[i1].busy_block.busy_size, addr_block1);
+        XBT_DEBUG("Block %zu not found (size_used = %zu, addr = %p)", i1, heapinfo1[i1].busy_block.busy_size, addr_block1);
         i1 = heaplimit + 1;
-        nb_diff1++;*/
-        i1++;
+        nb_diff1++;
+          //i1++;
       }
       
     }else{ /* Fragmented block */
@@ -300,7 +525,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
             addr_block2 = ((void*) (((ADDR2UINT(current_block)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
             addr_frag2 = (void*) ((char *)addr_block2 + (current_fragment << ((xbt_mheap_t)s_heap)->heapinfo[current_block].type));
 
-            res_compare = compare_area(addr_frag1, addr_frag2, NULL);
+            res_compare = compare_heap_area(addr_frag1, addr_frag2, NULL, NULL, NULL, NULL, 0); /*FIXME*/
 
             if(res_compare == 0)
               equal = 1;
@@ -330,7 +555,7 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
             addr_block2 = ((void*) (((ADDR2UINT(i2)) - 1) * BLOCKSIZE + (char*)((xbt_mheap_t)s_heap)->heapbase));
             addr_frag2 = (void*) ((char *)addr_block2 + (j2 << ((xbt_mheap_t)s_heap)->heapinfo[i2].type));
 
-            res_compare = compare_area(addr_frag1, addr_frag2, NULL);
+            res_compare = compare_heap_area(addr_frag1, addr_frag2, NULL, NULL, NULL, NULL, 0); /*FIXME*/
             
             if(res_compare == 0){
               equal = 1;
@@ -346,13 +571,13 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
 
         }
 
-        /*if(heapinfo1[i1].busy_frag.equal_to[j1] == NULL){
+        if(heapinfo1[i1].busy_frag.equal_to[j1] == NULL){
           fprintf(stderr,"Block %zu, fragment %zu not found (size_used = %zd, address = %p, ignore %d)\n", i1, j1, heapinfo1[i1].busy_frag.frag_size[j1], addr_frag1, heapinfo1[i1].busy_frag.ignore[j1]);
           i2 = heaplimit + 1;
           i1 = heaplimit + 1;
           nb_diff1++;
           break;
-          }*/
+        }
 
       }
 
@@ -454,82 +679,230 @@ int mmalloc_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
   return ((nb_diff1 > 0) || (nb_diff2 > 0));
 }
 
-void reset_heap_information(){
-
-  size_t i = 0, j;
+static int compare_heap_area_without_type(void *real_area1, void *real_area2, void *area1, void *area2, xbt_dynar_t previous, xbt_dict_t all_types, xbt_dict_t other_types, int size, int check_ignore){
 
-  while(i<=heaplimit){
-    if(heapinfo1[i].type == 0){
-      xbt_free(heapinfo1[i].busy_block.equal_to);
-      heapinfo1[i].busy_block.equal_to = NULL;
-    }
-    if(heapinfo1[i].type > 0){
-      for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo1[i].type); j++){
-        xbt_free(heapinfo1[i].busy_frag.equal_to[j]);
-        heapinfo1[i].busy_frag.equal_to[j] = NULL;
-      }
-    }
-    i++; 
-  }
+  int i = 0;
+  void *addr_pointed1, *addr_pointed2;
+  int pointer_align, ignore1, ignore2, res_compare;
 
-  i = 0;
+  while(i<size){
 
-  while(i<=heaplimit){
-    if(heapinfo2[i].type == 0){
-      xbt_free(heapinfo2[i].busy_block.equal_to);
-      heapinfo2[i].busy_block.equal_to = NULL;
-    }
-    if(heapinfo2[i].type > 0){
-      for(j=0; j < (size_t) (BLOCKSIZE >> heapinfo2[i].type); j++){
-        xbt_free(heapinfo2[i].busy_frag.equal_to[j]);
-        heapinfo2[i].busy_frag.equal_to[j] = NULL;
+    if(check_ignore > 0){
+      if((ignore1 = heap_comparison_ignore_size(to_ignore1, (char *)real_area1 + i)) > 0){
+        if((ignore2 = heap_comparison_ignore_size(to_ignore2, (char *)real_area2 + i))  == ignore1){
+          i = i + ignore2;
+          check_ignore--;
+          continue;
+        }
       }
     }
-    i++; 
-  }
 
-  s_heap = NULL, heapbase1 = NULL, heapbase2 = NULL;
-  heapinfo1 = NULL, heapinfo2 = NULL;
-  heaplimit = 0, heapsize1 = 0, heapsize2 = 0;
-  to_ignore1 = NULL, to_ignore2 = NULL;
+    if(memcmp(((char *)area1) + i, ((char *)area2) + i, 1) != 0){
 
-}
+      pointer_align = (i / sizeof(void*)) * sizeof(void*);
+      addr_pointed1 = *((void **)((char *)area1 + pointer_align));
+      addr_pointed2 = *((void **)((char *)area2 + pointer_align));
+      
+      if(addr_pointed1 > maestro_stack_start && addr_pointed1 < maestro_stack_end && addr_pointed2 > maestro_stack_start && addr_pointed2 < maestro_stack_end){
+        i = pointer_align + sizeof(void *);
+        continue;
+      }else if((addr_pointed1 > s_heap) && ((char *)addr_pointed1 < (char *)s_heap + STD_HEAP_SIZE) 
+               && (addr_pointed2 > s_heap) && ((char *)addr_pointed2 < (char *)s_heap + STD_HEAP_SIZE)){
+        res_compare = compare_heap_area(addr_pointed1, addr_pointed2, previous, all_types, other_types, NULL, 0); 
+        if(res_compare != 0){
+          return res_compare;
+        }
+        i = pointer_align + sizeof(void *);
+        continue;
+      }else{
+        return 1;
+      }
+      
+    }
+    
+    i++;
 
-static heap_area_t new_heap_area(int block, int fragment){
-  heap_area_t area = NULL;
-  area = xbt_new0(s_heap_area_t, 1);
-  area->block = block;
-  area->fragment = fragment;
-  return area;
+  }
+
+  return 0;
 }
 
 
-static size_t heap_comparison_ignore_size(xbt_dynar_t ignore_list, void *address){
+static int compare_heap_area_with_type(void *real_area1, void *real_area2, void *area1, void *area2, 
+                                       xbt_dynar_t previous, xbt_dict_t all_types, xbt_dict_t other_types, char *type_id, 
+                                       int area_size, int check_ignore, int pointer_level){
+
+  if(is_stack(real_area1) && is_stack(real_area2))
+    return 0;
 
+  size_t ignore1, ignore2;
+
+  if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
+    return 0;
+  
+  dw_type_t type = xbt_dict_get_or_null(all_types, type_id);
+  dw_type_t subtype, subsubtype;
+  int res, elm_size, i, switch_types = 0;
   unsigned int cursor = 0;
-  int start = 0;
-  int end = xbt_dynar_length(ignore_list) - 1;
-  mc_heap_ignore_region_t region;
+  dw_type_t member;
+  void *addr_pointed1, *addr_pointed2;;
+  char *type_desc;
 
-  while(start <= end){
-    cursor = (start + end) / 2;
-    region = (mc_heap_ignore_region_t)xbt_dynar_get_as(ignore_list, cursor, mc_heap_ignore_region_t);
-    if(region->address == address)
-      return region->size;
-    if(region->address < address)
-      start = cursor + 1;
-    if(region->address > address)
-      end = cursor - 1;   
+  switch(type->type){
+  case e_dw_base_type:
+    if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
+      return 0;
+    if(strcmp(type->name, "char") == 0){ /* Chaine de caractères, donc taille aléatoire */
+      return (memcmp(area1, area2, area_size) != 0);
+    }else{
+      if(area_size != -1 && type->size != area_size)
+        return -1;
+      else
+        return (memcmp(area1, area2, type->size) != 0);
+    }
+    break;
+  case e_dw_enumeration_type:
+    if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
+      return 0;
+    if(area_size != -1 && type->size != area_size)
+      return -1;
+    else
+      return (memcmp(area1, area2, type->size) != 0);
+    break;
+  case e_dw_typedef:
+    return compare_heap_area_with_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->dw_type_id, area_size, check_ignore, pointer_level);
+    break;
+  case e_dw_const_type:
+    return 0;
+    break;
+  case e_dw_array_type:
+    subtype = xbt_dict_get_or_null(all_types, type->dw_type_id);
+    switch(subtype->type){
+    case e_dw_base_type:
+    case e_dw_enumeration_type:
+    case e_dw_pointer_type:
+    case e_dw_structure_type:
+    case e_dw_union_type:
+      if(subtype->size == 0){ /*declaration of the type, need the complete description */
+        type_desc = get_type_description(all_types, subtype->name);
+        if(type_desc){
+          subtype = xbt_dict_get_or_null(all_types, type_desc);
+        }else{
+          subtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subtype->name));
+          switch_types = 1;
+        }
+      }
+      elm_size = subtype->size;
+      break;
+    case e_dw_typedef:
+    case e_dw_volatile_type:
+      subsubtype = xbt_dict_get_or_null(all_types, subtype->dw_type_id);
+      if(subsubtype->size == 0){ /*declaration of the type, need the complete description */
+        type_desc = get_type_description(all_types, subsubtype->name);
+        if(type_desc){
+          subsubtype = xbt_dict_get_or_null(all_types, type_desc);
+        }else{
+          subsubtype = xbt_dict_get_or_null(other_types, get_type_description(other_types, subtype->name));
+          switch_types = 1;
+        }
+      }
+      elm_size = subsubtype->size;
+      break;
+    default : 
+      return 0;
+      break;
+    }
+    for(i=0; i<type->size; i++){
+      if(switch_types)
+        res = compare_heap_area_with_type((char *)real_area1 + (i*elm_size), (char *)real_area2 + (i*elm_size), (char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), previous, other_types, all_types, type->dw_type_id, type->size, check_ignore, pointer_level);
+      else
+        res = compare_heap_area_with_type((char *)real_area1 + (i*elm_size), (char *)real_area2 + (i*elm_size), (char *)area1 + (i*elm_size), (char *)area2 + (i*elm_size), previous, all_types, other_types, type->dw_type_id, type->size, check_ignore, pointer_level);
+      if(res != 0)
+        return res;
+    }
+    break;
+  case e_dw_pointer_type:
+    if(type->dw_type_id && ((dw_type_t)xbt_dict_get_or_null(all_types, type->dw_type_id))->type == e_dw_subroutine_type){
+      addr_pointed1 = *((void **)(area1)); 
+      addr_pointed2 = *((void **)(area2));
+      return (addr_pointed1 != addr_pointed2);;
+    }else{
+      pointer_level++;
+      if(pointer_level > 1){ /* Array of pointers */
+        for(i=0; i<(area_size/sizeof(void *)); i++){
+          addr_pointed1 = *((void **)((char *)area1 + (i*sizeof(void *)))); 
+          addr_pointed2 = *((void **)((char *)area2 + (i*sizeof(void *)))); 
+          if(addr_pointed1 > s_heap && (char *)addr_pointed1 < (char*) s_heap + STD_HEAP_SIZE && addr_pointed2 > s_heap && (char *)addr_pointed2 < (char*) s_heap + STD_HEAP_SIZE)
+            res =  compare_heap_area(addr_pointed1, addr_pointed2, previous, all_types, other_types, type->dw_type_id, pointer_level); 
+          else
+            res =  (addr_pointed1 != addr_pointed2);
+          if(res != 0)
+            return res;
+        }
+      }else{
+        addr_pointed1 = *((void **)(area1)); 
+        addr_pointed2 = *((void **)(area2));
+        if(addr_pointed1 > s_heap && (char *)addr_pointed1 < (char*) s_heap + STD_HEAP_SIZE && addr_pointed2 > s_heap && (char *)addr_pointed2 < (char*) s_heap + STD_HEAP_SIZE)
+          return compare_heap_area(addr_pointed1, addr_pointed2, previous, all_types, other_types, type->dw_type_id, pointer_level); 
+        else
+          return  (addr_pointed1 != addr_pointed2);
+      }
+    }
+    break;
+  case e_dw_structure_type:
+    if(type->size == 0){ /*declaration of the structure, need the complete description */
+      type_desc = get_type_description(all_types, type->name);
+      if(type_desc){
+        type = xbt_dict_get_or_null(all_types, type_desc);
+      }else{
+        type = xbt_dict_get_or_null(other_types, get_type_description(other_types, type->name));
+        switch_types = 1;
+      }
+    }
+    if(area_size != -1 && type->size != area_size){
+      if(area_size>type->size && area_size%type->size == 0){
+        for(i=0; i<(area_size/type->size); i++){
+          if(switch_types)
+            res = compare_heap_area_with_type((char *)real_area1 + (i*type->size), (char *)real_area2 + (i*type->size), (char *)area1 + (i*type->size), (char *)area2 + (i*type->size), previous, other_types, all_types, type_id, -1, check_ignore, 0); 
+          else
+            res = compare_heap_area_with_type((char *)real_area1 + (i*type->size), (char *)real_area2 + (i*type->size), (char *)area1 + (i*type->size), (char *)area2 + (i*type->size), previous, all_types, other_types, type_id, -1, check_ignore, 0); 
+          if(res != 0)
+            return res;
+        }
+      }else{
+        return -1;
+      }
+    }else{
+      cursor = 0;
+      xbt_dynar_foreach(type->members, cursor, member){
+        if(switch_types)
+          res = compare_heap_area_with_type((char *)real_area1 + member->offset, (char *)real_area2 + member->offset, (char *)area1 + member->offset, (char *)area2 + member->offset, previous, other_types, all_types, member->dw_type_id, -1, check_ignore, 0);
+        else
+          res = compare_heap_area_with_type((char *)real_area1 + member->offset, (char *)real_area2 + member->offset, (char *)area1 + member->offset, (char *)area2 + member->offset, previous, all_types, other_types, member->dw_type_id, -1, check_ignore, 0);  
+        if(res != 0)
+          return res;        
+      }
+    }
+    break;
+  case e_dw_union_type:
+    if((check_ignore > 0) && ((ignore1 = heap_comparison_ignore_size(to_ignore1, real_area1)) > 0) && ((ignore2 = heap_comparison_ignore_size(to_ignore2, real_area2))  == ignore1))
+      return 0;
+    return compare_heap_area_without_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->size, check_ignore);
+    break;
+  case e_dw_volatile_type:
+    return compare_heap_area_with_type(real_area1, real_area2, area1, area2, previous, all_types, other_types, type->dw_type_id, area_size, check_ignore, pointer_level);
+    break;
+  default:
+    break;
   }
 
   return 0;
-}
 
+}
 
-int compare_area(void *area1, void* area2, xbt_dynar_t previous){
+int compare_heap_area(void *area1, void* area2, xbt_dynar_t previous, xbt_dict_t all_types, xbt_dict_t other_types, char *type_id, int pointer_level){
 
-  size_t i = 0, pointer_align = 0, ignore1 = 0, ignore2 = 0;
-  void *addr_pointed1, *addr_pointed2;
   int res_compare;
   ssize_t block1, frag1, block2, frag2;
   ssize_t size;
@@ -629,7 +1002,8 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){
       if((heapinfo1[block1].busy_block.ignore > 0) && (heapinfo2[block2].busy_block.ignore == heapinfo1[block1].busy_block.ignore))
         check_ignore = heapinfo1[block1].busy_block.ignore;
       
-    }else{
+    }else{ /* Frgamented block */
+
       frag1 = ((uintptr_t) (ADDR2UINT (area1) % (BLOCKSIZE))) >> heapinfo1[block1].type;
       frag2 = ((uintptr_t) (ADDR2UINT (area2) % (BLOCKSIZE))) >> heapinfo2[block2].type;
       
@@ -734,48 +1108,23 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){
     }
     return 1;
   }
-  
-  while(i<size){
-
-    if(check_ignore > 0){
-      if((ignore1 = heap_comparison_ignore_size(to_ignore1, (char *)area1 + i)) > 0){
-        if((ignore2 = heap_comparison_ignore_size(to_ignore2, (char *)area2 + i))  == ignore1){
-          i = i + ignore2;
-          check_ignore--;
-          continue;
-        }
-      }
-    }
 
-    if(memcmp(((char *)area1_to_compare) + i, ((char *)area2_to_compare) + i, 1) != 0){
 
-      pointer_align = (i / sizeof(void*)) * sizeof(void*);
-      addr_pointed1 = *((void **)((char *)area1_to_compare + pointer_align));
-      addr_pointed2 = *((void **)((char *)area2_to_compare + pointer_align));
-      
-      if(addr_pointed1 > maestro_stack_start && addr_pointed1 < maestro_stack_end && addr_pointed2 > maestro_stack_start && addr_pointed2 < maestro_stack_end){
-        i = pointer_align + sizeof(void *);
-        continue;
-      }else if((addr_pointed1 > s_heap) && ((char *)addr_pointed1 < (char *)s_heap + STD_HEAP_SIZE) 
-           && (addr_pointed2 > s_heap) && ((char *)addr_pointed2 < (char *)s_heap + STD_HEAP_SIZE)){
-        res_compare = compare_area(addr_pointed1, addr_pointed2, previous);
-        if(res_compare != 0){
-          if(match_pairs)
-            xbt_dynar_free(&previous);
-          return res_compare;
-        }
-        i = pointer_align + sizeof(void *);
-        continue;
-      }else{
+  /* Start comparison*/
+  if(type_id != NULL){
+    res_compare = compare_heap_area_with_type(area1, area2, area1_to_compare, area2_to_compare, previous, all_types, other_types, type_id, size, check_ignore, pointer_level);
+    if(res_compare != 0){
+      if(match_pairs)
+        xbt_dynar_free(&previous);
+      return res_compare;
+    }
+  }else{
+    res_compare = compare_heap_area_without_type(area1, area2, area1_to_compare, area2_to_compare, previous, all_types, other_types, size, check_ignore);
+      if(res_compare != 0){
         if(match_pairs)
           xbt_dynar_free(&previous);
-        return 1;
+        return res_compare;
       }
-      
-    }
-    
-    i++;
-
   }
 
   if(match_pairs){
@@ -784,101 +1133,56 @@ int compare_area(void *area1, void* area2, xbt_dynar_t previous){
   }
 
   return 0;
-  
-
 }
 
-static void heap_area_pair_free(heap_area_pair_t pair){
-  xbt_free(pair);
-  pair = NULL;
-}
+/*********************************************** Miscellaneous ***************************************************/
+/****************************************************************************************************************/
 
-static void heap_area_pair_free_voidp(void *d)
-{
-  heap_area_pair_free((heap_area_pair_t) * (void **) d);
-}
 
-static int add_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2){
+int get_pointed_area_size(void *area, int heap){
 
-  if(is_new_heap_area_pair(list, block1, fragment1, block2, fragment2)){
-    heap_area_pair_t pair = NULL;
-    pair = xbt_new0(s_heap_area_pair_t, 1);
-    pair->block1 = block1;
-    pair->fragment1 = fragment1;
-    pair->block2 = block2;
-    pair->fragment2 = fragment2;
-    
-    xbt_dynar_push(list, &pair); 
+  int block, frag;
+  malloc_info *heapinfo;
 
-    return 1;
-  }
+  if(heap == 1)
+    heapinfo = heapinfo1;
+  else
+    heapinfo = heapinfo2;
 
-  return 0;
-}
-static int is_new_heap_area_pair(xbt_dynar_t list, int block1, int fragment1, int block2, int fragment2){
-  
-  unsigned int cursor = 0;
-  heap_area_pair_t current_pair;
+  block = ((char*)area - (char*)((xbt_mheap_t)s_heap)->heapbase) / BLOCKSIZE + 1;
 
-  xbt_dynar_foreach(list, cursor, current_pair){
-    if(current_pair->block1 == block1 && current_pair->block2 == block2 && current_pair->fragment1 == fragment1 && current_pair->fragment2 == fragment2)
-      return 0; 
-  }
-  
-  return 1;
-}
-
-
-void match_equals(xbt_dynar_t list){
-
-  unsigned int cursor = 0;
-  heap_area_pair_t current_pair;
-  heap_area_t previous_area;
-
-  xbt_dynar_foreach(list, cursor, current_pair){
-
-    if(current_pair->fragment1 != -1){
-      
-      if(heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1] != NULL){    
-        previous_area = heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1];
-        xbt_free(heapinfo2[previous_area->block].busy_frag.equal_to[previous_area->fragment]);
-        heapinfo2[previous_area->block].busy_frag.equal_to[previous_area->fragment] = NULL;
-        xbt_free(previous_area); 
-      }
-      if(heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2] != NULL){        
-        previous_area = heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2];
-        xbt_free(heapinfo1[previous_area->block].busy_frag.equal_to[previous_area->fragment]);
-        heapinfo1[previous_area->block].busy_frag.equal_to[previous_area->fragment] = NULL;
-        xbt_free(previous_area);
-      }
+  if(((char *)area < (char*)((xbt_mheap_t)s_heap)->heapbase)  || (block > heapsize1) || (block < 1))
+    return -1;
 
-      heapinfo1[current_pair->block1].busy_frag.equal_to[current_pair->fragment1] = new_heap_area(current_pair->block2, current_pair->fragment2);
-      heapinfo2[current_pair->block2].busy_frag.equal_to[current_pair->fragment2] = new_heap_area(current_pair->block1, current_pair->fragment1);
+  if(heapinfo[block].type == -1){ /* Free block */
+    return -1;  
+  }else if(heapinfo[block].type == 0){ /* Complete block */
+    return (int)heapinfo[block].busy_block.busy_size;
+  }else{
+    frag = ((uintptr_t) (ADDR2UINT (area) % (BLOCKSIZE))) >> heapinfo[block].type;
+    return (int)heapinfo[block].busy_frag.frag_size[frag];
+  }
 
-    }else{
+}
 
-      if(heapinfo1[current_pair->block1].busy_block.equal_to != NULL){
-        previous_area = heapinfo1[current_pair->block1].busy_block.equal_to;
-        xbt_free(heapinfo2[previous_area->block].busy_block.equal_to);
-        heapinfo2[previous_area->block].busy_block.equal_to = NULL; 
-        xbt_free(previous_area);
-      }
-      if(heapinfo2[current_pair->block2].busy_block.equal_to != NULL){
-        previous_area = heapinfo2[current_pair->block2].busy_block.equal_to;
-        xbt_free(heapinfo1[previous_area->block].busy_block.equal_to);
-        heapinfo1[previous_area->block].busy_block.equal_to = NULL;
-        xbt_free(previous_area);
-      }
+char *get_type_description(xbt_dict_t types, char *type_name){
 
-      heapinfo1[current_pair->block1].busy_block.equal_to = new_heap_area(current_pair->block2, current_pair->fragment2);
-      heapinfo2[current_pair->block2].busy_block.equal_to = new_heap_area(current_pair->block1, current_pair->fragment1);
+  xbt_dict_cursor_t dict_cursor;
+  char *type_origin;
+  dw_type_t type;
 
+  xbt_dict_foreach(types, dict_cursor, type_origin, type){
+    if(type->name && (strcmp(type->name, type_name) == 0) && type->size > 0){
+      xbt_dict_cursor_free(&dict_cursor);
+      return type_origin;
     }
   }
 
+  xbt_dict_cursor_free(&dict_cursor);
+  return NULL;
 }
 
+
 #ifndef max
 #define max( a, b ) ( ((a) > (b)) ? (a) : (b) )
 #endif
@@ -1007,165 +1311,3 @@ int mmalloc_linear_compare_heap(xbt_mheap_t heap1, xbt_mheap_t heap2){
   
 }
 
-static int is_stack(void *address){
-  unsigned int cursor = 0;
-  stack_region_t stack;
-
-  xbt_dynar_foreach(stacks_areas, cursor, stack){
-    if(address == stack->address)
-      return 1;
-  }
-
-  return 0;
-}
-
-static int is_block_stack(int block){
-  unsigned int cursor = 0;
-  stack_region_t stack;
-
-  xbt_dynar_foreach(stacks_areas, cursor, stack){
-    if(block == stack->block)
-      return 1;
-  }
-
-  return 0;
-}
-
-static void add_heap_equality(xbt_dynar_t equals, void *a1, void *a2){
-  
-  if(xbt_dynar_is_empty(equals)){
-
-    heap_equality_t he = xbt_new0(s_heap_equality_t, 1);
-    he->address1 = a1;
-    he->address2 = a2;
-
-    xbt_dynar_insert_at(equals, 0, &he);
-  
-  }else{
-
-    unsigned int cursor = 0;
-    int start = 0;
-    int end = xbt_dynar_length(equals) - 1;
-    heap_equality_t current_equality = NULL;
-
-    while(start <= end){
-      cursor = (start + end) / 2;
-      current_equality = (heap_equality_t)xbt_dynar_get_as(equals, cursor, heap_equality_t);
-      if(current_equality->address1 == a1){
-        if(current_equality->address2 == a2)
-          return;
-        if(current_equality->address2 < a2)
-          start = cursor + 1;
-        if(current_equality->address2 > a2)
-          end = cursor - 1;
-      }
-      if(current_equality->address1 < a1)
-        start = cursor + 1;
-      if(current_equality->address1 > a1)
-        end = cursor - 1; 
-    }
-
-    heap_equality_t he = xbt_new0(s_heap_equality_t, 1);
-    he->address1 = a1;
-    he->address2 = a2;
-  
-    if(current_equality->address1 < a1)
-      xbt_dynar_insert_at(equals, cursor + 1 , &he);
-    else
-       xbt_dynar_insert_at(equals, cursor, &he); 
-
-  }
-
-}
-
-static void remove_heap_equality(xbt_dynar_t equals, int address, void *a){
-  
-  unsigned int cursor = 0;
-  heap_equality_t current_equality;
-  int found = 0;
-
-  if(address == 1){
-
-    int start = 0;
-    int end = xbt_dynar_length(equals) - 1;
-
-
-    while(start <= end && found == 0){
-      cursor = (start + end) / 2;
-      current_equality = (heap_equality_t)xbt_dynar_get_as(equals, cursor, heap_equality_t);
-      if(current_equality->address1 == a)
-        found = 1;
-      if(current_equality->address1 < a)
-        start = cursor + 1;
-      if(current_equality->address1 > a)
-        end = cursor - 1; 
-    }
-
-    if(found == 1)
-      xbt_dynar_remove_at(equals, cursor, NULL);
-  
-  }else{
-
-    xbt_dynar_foreach(equals, cursor, current_equality){
-      if(current_equality->address2 == a){
-        found = 1;
-        break;
-      }
-    }
-
-    if(found == 1)
-      xbt_dynar_remove_at(equals, cursor, NULL);
-
-  }
-  
-}
-
-int is_free_area(void *area, xbt_mheap_t heap){
-
-  void *sheap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize();
-  malloc_info *heapinfo = (malloc_info *)((char *)heap + ((uintptr_t)((char *)heap->heapinfo - (char *)sheap)));
-  size_t heapsize = heap->heapsize;
-
-  /* Get block number */ 
-  size_t block = ((char*)area - (char*)((xbt_mheap_t)sheap)->heapbase) / BLOCKSIZE + 1;
-  size_t fragment;
-
-  /* Check if valid block number */
-  if((char *)area < (char*)((xbt_mheap_t)sheap)->heapbase || block > heapsize || block < 1)
-    return 0;
-
-  if(heapinfo[block].type < 0)
-    return 1;
-
-  if(heapinfo[block].type == 0)
-    return 0;
-
-  if(heapinfo[block].type > 0){
-    fragment = ((uintptr_t) (ADDR2UINT(area) % (BLOCKSIZE))) >> heapinfo[block].type;
-    if(heapinfo[block].busy_frag.frag_size[fragment] == 0)
-      return 1;  
-  }
-
-  return 0;
-}
-
-static int equal_blocks(int b1, int b2){
-  if(heapinfo1[b1].busy_block.equal_to != NULL){
-    if(heapinfo2[b2].busy_block.equal_to != NULL){
-      if(((heap_area_t)(heapinfo1[b1].busy_block.equal_to))->block == b2 && ((heap_area_t)(heapinfo2[b2].busy_block.equal_to))->block == b1)
-        return 1;
-    }
-  }
-  return 0;
-}
-
-static int equal_fragments(int b1, int f1, int b2, int f2){
-  if(heapinfo1[b1].busy_frag.equal_to[f1] != NULL){
-    if(heapinfo2[b2].busy_frag.equal_to[f2] != NULL){
-      if(((heap_area_t)(heapinfo1[b1].busy_frag.equal_to[f1]))->block == b2 && ((heap_area_t)(heapinfo2[b2].busy_frag.equal_to[f2]))->block == b1 && ((heap_area_t)(heapinfo1[b1].busy_frag.equal_to[f1]))->fragment == f2 && ((heap_area_t)(heapinfo2[b2].busy_frag.equal_to[f2]))->fragment == f1)
-        return 1;
-    }
-  }
-  return 0;
-}