src/mc/mc_global.c

   1 /* Copyright (c) 2008-2013. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <unistd.h>
   8 #include <sys/types.h>
   9 #include <sys/wait.h>
  10 #include <sys/time.h>
  11 #include <libgen.h>
  12
  13 #include "simgrid/sg_config.h"
  14 #include "../surf/surf_private.h"
  15 #include "../simix/smx_private.h"
  16 #include "../xbt/mmalloc/mmprivate.h"
  17 #include "xbt/fifo.h"
  18 #include "mc_private.h"
  19 #include "xbt/automaton.h"
  20 #include "xbt/dict.h"
  21
  22 static void MC_post_process_types(mc_object_info_t info);
  23
  24 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
  25 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
  26                                 "Logging specific to MC (global)");
  27
  28 /* Configuration support */
  29 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
  30
  31 int _sg_do_model_check = 0;
  32 int _sg_mc_checkpoint=0;
  33 char* _sg_mc_property_file=NULL;
  34 int _sg_mc_timeout=0;
  35 int _sg_mc_max_depth=1000;
  36 int _sg_mc_visited=0;
  37 char *_sg_mc_dot_output_file = NULL;
  38
  39 int user_max_depth_reached = 0;
  40
  41 void _mc_cfg_cb_reduce(const char *name, int pos) {
  42   if (_sg_cfg_init_status && !_sg_do_model_check) {
  43     xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  44   }
  45   char *val= xbt_cfg_get_string(_sg_cfg_set, name);
  46   if (!strcasecmp(val,"none")) {
  47     mc_reduce_kind = e_mc_reduce_none;
  48   } else if (!strcasecmp(val,"dpor")) {
  49     mc_reduce_kind = e_mc_reduce_dpor;
  50   } else {
  51     xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
  52   }
  53 }
  54
  55 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
  56   if (_sg_cfg_init_status && !_sg_do_model_check) {
  57     xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  58   }
  59   _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
  60 }
  61 void _mc_cfg_cb_property(const char *name, int pos) {
  62   if (_sg_cfg_init_status && !_sg_do_model_check) {
  63     xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  64   }
  65   _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
  66 }
  67
  68 void _mc_cfg_cb_timeout(const char *name, int pos) {
  69   if (_sg_cfg_init_status && !_sg_do_model_check) {
  70     xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  71   }
  72   _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
  73 }
  74
  75 void _mc_cfg_cb_max_depth(const char *name, int pos) {
  76   if (_sg_cfg_init_status && !_sg_do_model_check) {
  77     xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  78   }
  79   _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
  80 }
  81
  82 void _mc_cfg_cb_visited(const char *name, int pos) {
  83   if (_sg_cfg_init_status && !_sg_do_model_check) {
  84     xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  85   }
  86   _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
  87 }
  88
  89 void _mc_cfg_cb_dot_output(const char *name, int pos) {
  90   if (_sg_cfg_init_status && !_sg_do_model_check) {
  91     xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
  92   }
  93   _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
  94 }
  95
  96 /* MC global data structures */
  97 mc_state_t mc_current_state = NULL;
  98 char mc_replay_mode = FALSE;
  99 double *mc_time = NULL;
 100 __thread mc_comparison_times_t mc_comp_times = NULL;
 101 __thread double mc_snapshot_comparison_time;
 102 mc_stats_t mc_stats = NULL;
 103
 104 /* Safety */
 105 xbt_fifo_t mc_stack_safety = NULL;
 106 mc_global_t initial_state_safety = NULL;
 107
 108 /* Liveness */
 109 xbt_fifo_t mc_stack_liveness = NULL;
 110 mc_global_t initial_state_liveness = NULL;
 111 int compare;
 112
 113 xbt_automaton_t _mc_property_automaton = NULL;
 114
 115 /* Variables */
 116 mc_object_info_t mc_libsimgrid_info = NULL;
 117 mc_object_info_t mc_binary_info = NULL;
 118
 119 /* Ignore mechanism */
 120 xbt_dynar_t mc_stack_comparison_ignore;
 121 xbt_dynar_t mc_data_bss_comparison_ignore;
 122 extern xbt_dynar_t mc_heap_comparison_ignore;
 123 extern xbt_dynar_t stacks_areas;
 124
 125 /* Dot output */
 126 FILE *dot_output = NULL;
 127 const char* colors[13];
 128
 129
 130 /*******************************  DWARF Information *******************************/
 131 /**********************************************************************************/
 132
 133 /************************** Free functions *************************/
 134
 135 static void dw_location_free(dw_location_t l){
 136   if(l){
 137     if(l->type == e_dw_loclist)
 138       xbt_dynar_free(&(l->location.loclist));
 139     else if(l->type == e_dw_compose)
 140       xbt_dynar_free(&(l->location.compose));
 141     else if(l->type == e_dw_arithmetic)
 142       xbt_free(l->location.arithmetic);
 143
 144     xbt_free(l);
 145   }
 146 }
 147
 148 static void dw_location_entry_free(dw_location_entry_t e){
 149   dw_location_free(e->location);
 150   xbt_free(e);
 151 }
 152
 153 void dw_type_free(dw_type_t t){
 154   xbt_free(t->name);
 155   xbt_free(t->dw_type_id);
 156   xbt_dynar_free(&(t->members));
 157   xbt_free(t);
 158 }
 159
 160 static void dw_type_free_voidp(void *t){
 161   dw_type_free((dw_type_t) * (void **) t);
 162 }
 163
 164 static void dw_variable_free(dw_variable_t v){
 165   if(v){
 166     xbt_free(v->name);
 167     xbt_free(v->type_origin);
 168     if(!v->global)
 169       dw_location_free(v->address.location);
 170     xbt_free(v);
 171   }
 172 }
 173
 174 static void dw_variable_free_voidp(void *t){
 175   dw_variable_free((dw_variable_t) * (void **) t);
 176 }
 177
 178 // object_info
 179
 180 mc_object_info_t MC_new_object_info(void) {
 181   mc_object_info_t res = xbt_new(s_mc_object_info_t, 1);
 182   res->file_name = NULL;
 183   res->start_text = NULL;
 184   res->start_data = NULL;
 185   res->start_bss = NULL;
 186   res->start_plt = NULL;
 187   res->end_plt = NULL;
 188   res->start_got_plt = NULL;
 189   res->end_got_plt = NULL;
 190   res->local_variables = xbt_dict_new_homogeneous(NULL);
 191   res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
 192   res->types = xbt_dict_new_homogeneous(NULL);
 193   return res;
 194 }
 195
 196 void MC_free_object_info(mc_object_info_t* info) {
 197   xbt_free(&(*info)->file_name);
 198   xbt_dict_free(&(*info)->local_variables);
 199   xbt_dynar_free(&(*info)->global_variables);
 200   xbt_dict_free(&(*info)->types);
 201   xbt_free(info);
 202   info = NULL;
 203 }
 204
 205 /*************************************************************************/
 206
 207 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
 208
 209   dw_location_t loc = xbt_new0(s_dw_location_t, 1);
 210
 211   if(location_list != NULL){
 212
 213     char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
 214     loc->type = e_dw_loclist;
 215     loc->location.loclist =  (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
 216     if(loc->location.loclist == NULL)
 217       XBT_INFO("Key not found in loclist");
 218     xbt_free(key);
 219     return loc;
 220
 221   }else{
 222
 223     int cursor = 0;
 224     char *tok = NULL, *tok2 = NULL;
 225
 226     xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
 227     xbt_dynar_t tokens2;
 228
 229     loc->type = e_dw_compose;
 230     loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
 231
 232     while(cursor < xbt_dynar_length(tokens1)){
 233
 234       tok = xbt_dynar_get_as(tokens1, cursor, char*);
 235       tokens2 = xbt_str_split(tok, " ");
 236       tok2 = xbt_dynar_get_as(tokens2, 0, char*);
 237
 238       if(strncmp(tok2, "DW_OP_reg", 9) == 0){
 239         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 240         new_element->type = e_dw_register;
 241         new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
 242         xbt_dynar_push(loc->location.compose, &new_element);
 243       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
 244         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 245         new_element->type = e_dw_fbregister_op;
 246         new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 247         xbt_dynar_push(loc->location.compose, &new_element);
 248       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
 249         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 250         new_element->type = e_dw_bregister_op;
 251         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
 252         new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 253         xbt_dynar_push(loc->location.compose, &new_element);
 254       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
 255         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 256         new_element->type = e_dw_lit;
 257         new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
 258         xbt_dynar_push(loc->location.compose, &new_element);
 259       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
 260         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 261         new_element->type = e_dw_piece;
 262         new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 263         xbt_dynar_push(loc->location.compose, &new_element);
 264       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
 265         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 266         new_element->type = e_dw_plus_uconst;
 267         new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
 268         xbt_dynar_push(loc->location.compose, &new_element);
 269       }else if(strcmp(tok, "DW_OP_abs") == 0 ||
 270                strcmp(tok, "DW_OP_and") == 0 ||
 271                strcmp(tok, "DW_OP_div") == 0 ||
 272                strcmp(tok, "DW_OP_minus") == 0 ||
 273                strcmp(tok, "DW_OP_mod") == 0 ||
 274                strcmp(tok, "DW_OP_mul") == 0 ||
 275                strcmp(tok, "DW_OP_neg") == 0 ||
 276                strcmp(tok, "DW_OP_not") == 0 ||
 277                strcmp(tok, "DW_OP_or") == 0 ||
 278                strcmp(tok, "DW_OP_plus") == 0){
 279         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 280         new_element->type = e_dw_arithmetic;
 281         new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
 282         xbt_dynar_push(loc->location.compose, &new_element);
 283       }else if(strcmp(tok, "DW_OP_stack_value") == 0){
 284       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
 285         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 286         new_element->type = e_dw_deref;
 287         new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
 288         xbt_dynar_push(loc->location.compose, &new_element);
 289       }else if(strcmp(tok, "DW_OP_deref") == 0){
 290         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 291         new_element->type = e_dw_deref;
 292         new_element->location.deref_size = sizeof(void *);
 293         xbt_dynar_push(loc->location.compose, &new_element);
 294       }else if(strcmp(tok2, "DW_OP_constu:") == 0){
 295         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 296         new_element->type = e_dw_uconstant;
 297         new_element->location.uconstant.bytes = 1;
 298         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 299         xbt_dynar_push(loc->location.compose, &new_element);
 300       }else if(strcmp(tok2, "DW_OP_consts:") == 0){
 301         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 302         new_element->type = e_dw_sconstant;
 303         new_element->location.sconstant.bytes = 1;
 304         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 305         xbt_dynar_push(loc->location.compose, &new_element);
 306       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
 307                strcmp(tok2, "DW_OP_const2u:") == 0 ||
 308                strcmp(tok2, "DW_OP_const4u:") == 0 ||
 309                strcmp(tok2, "DW_OP_const8u:") == 0){
 310         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 311         new_element->type = e_dw_uconstant;
 312         new_element->location.uconstant.bytes = tok2[11] - '0';
 313         new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 314         xbt_dynar_push(loc->location.compose, &new_element);
 315       }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
 316                strcmp(tok, "DW_OP_const2s") == 0 ||
 317                strcmp(tok, "DW_OP_const4s") == 0 ||
 318                strcmp(tok, "DW_OP_const8s") == 0){
 319         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 320         new_element->type = e_dw_sconstant;
 321         new_element->location.sconstant.bytes = tok2[11] - '0';
 322         new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
 323         xbt_dynar_push(loc->location.compose, &new_element);
 324       }else{
 325         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
 326         new_element->type = e_dw_unsupported;
 327         xbt_dynar_push(loc->location.compose, &new_element);
 328       }
 329
 330       cursor++;
 331       xbt_dynar_free(&tokens2);
 332
 333     }
 334
 335     xbt_dynar_free(&tokens1);
 336
 337     return loc;
 338
 339   }
 340
 341 }
 342
 343 /** @brief Extract the location lists from an ELF file (.debug_loc)
 344  *
 345  *  @return A map from the offset in the list (in hexadecimal string)
 346  *          into a location list (dynar of dw_location_entry_t).
 347  */
 348 static xbt_dict_t MC_dwarf_get_location_list(const char *elf_file){
 349
 350   char *command = bprintf("LANG=C objdump -Wo %s", elf_file);
 351
 352   FILE *fp = popen(command, "r");
 353
 354   if(fp == NULL){
 355     perror("popen for objdump failed");
 356     xbt_abort();
 357   }
 358
 359   int debug = 0; /*Detect if the program has been compiled with -g */
 360
 361   xbt_dict_t location_list = xbt_dict_new_homogeneous(NULL);
 362   char *line = NULL, *loc_expr = NULL;
 363   ssize_t read;
 364   size_t n = 0;
 365   int cursor_remove;
 366   xbt_dynar_t split = NULL;
 367
 368   while ((read = xbt_getline(&line, &n, fp)) != -1) {
 369
 370     /* Wipeout the new line character */
 371     line[read - 1] = '\0';
 372
 373     xbt_str_trim(line, NULL);
 374
 375     if(n == 0)
 376       continue;
 377
 378     if(strlen(line) == 0)
 379       continue;
 380
 381     if(debug == 0){
 382
 383       if(strncmp(line, elf_file, strlen(elf_file)) == 0)
 384         continue;
 385
 386       if(strncmp(line, "Contents", 8) == 0)
 387         continue;
 388
 389       if(strncmp(line, "Offset", 6) == 0){
 390         debug = 1;
 391         continue;
 392       }
 393     }
 394
 395     if(debug == 0){
 396       XBT_INFO("Your program must be compiled with -g");
 397       xbt_abort();
 398     }
 399
 400     xbt_dynar_t loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL);
 401
 402     xbt_str_strip_spaces(line);
 403     split = xbt_str_split(line, " ");
 404
 405     char *key = NULL;
 406     while(read != -1 && strcmp("<End", (char *)xbt_dynar_get_as(split, 1, char *)) != 0){
 407
 408       // Take the key from the first line of the list:
 409       if(key==NULL){
 410         key = bprintf("%d", (int)strtoul((char *)xbt_dynar_get_as(split, 0, char *), NULL, 16));
 411       }
 412
 413       dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1);
 414       new_entry->lowpc = strtoul((char *)xbt_dynar_get_as(split, 1, char *), NULL, 16);
 415       new_entry->highpc = strtoul((char *)xbt_dynar_get_as(split, 2, char *), NULL, 16);
 416
 417       cursor_remove =0;
 418       while(cursor_remove < 3){
 419         xbt_dynar_remove_at(split, 0, NULL);
 420         cursor_remove++;
 421       }
 422
 423       loc_expr = xbt_str_join(split, " ");
 424       xbt_str_ltrim(loc_expr, "(");
 425       xbt_str_rtrim(loc_expr, ")");
 426       new_entry->location = MC_dwarf_get_location(NULL, loc_expr);
 427
 428       xbt_dynar_push(loclist, &new_entry);
 429
 430       xbt_dynar_free(&split);
 431       free(loc_expr);
 432
 433       read = xbt_getline(&line, &n, fp);
 434       if(read != -1){
 435         line[read - 1] = '\0';
 436         xbt_str_strip_spaces(line);
 437         split = xbt_str_split(line, " ");
 438       }
 439
 440     }
 441
 442
 443     xbt_dict_set(location_list, key, loclist, NULL);
 444     xbt_free(key);
 445
 446     xbt_dynar_free(&split);
 447
 448   }
 449
 450   xbt_free(line);
 451   xbt_free(command);
 452   pclose(fp);
 453
 454   return location_list;
 455 }
 456
 457 /** \brief Finds a frame (DW_TAG_subprogram) from an DWARF offset in the rangd of this subprogram
 458  *
 459  * The offset can be an offset of a child DW_TAG_variable.
 460  */
 461 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
 462
 463   xbt_dict_cursor_t cursor = NULL;
 464   char *name;
 465   dw_frame_t res;
 466
 467   xbt_dict_foreach(all_variables, cursor, name, res) {
 468     if(offset >= res->start && offset < res->end){
 469       xbt_dict_cursor_free(&cursor);
 470       return res;
 471     }
 472   }
 473
 474   xbt_dict_cursor_free(&cursor);
 475   return NULL;
 476
 477 }
 478
 479 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
 480
 481   unsigned int cursor = 0;
 482   dw_variable_t current_var;
 483
 484   xbt_dynar_foreach(frame->variables, cursor, current_var){
 485     if(strcmp(var, current_var->name) == 0)
 486       return current_var;
 487   }
 488
 489   return NULL;
 490 }
 491
 492 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
 493
 494   if(xbt_dynar_is_empty(variables))
 495     return 0;
 496
 497   unsigned int cursor = 0;
 498   int start = 0;
 499   int end = xbt_dynar_length(variables) - 1;
 500   dw_variable_t var_test = NULL;
 501
 502   while(start <= end){
 503     cursor = (start + end) / 2;
 504     var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
 505     if(strcmp(var_test->name, var) < 0){
 506       start = cursor + 1;
 507     }else if(strcmp(var_test->name, var) > 0){
 508       end = cursor - 1;
 509     }else{
 510       if(address){ /* global variable */
 511         if(var_test->address.address == address)
 512           return -1;
 513         if(var_test->address.address > address)
 514           end = cursor - 1;
 515         else
 516           start = cursor + 1;
 517       }else{ /* local variable */
 518         return -1;
 519       }
 520     }
 521   }
 522
 523   if(strcmp(var_test->name, var) == 0){
 524     if(address && var_test->address.address < address)
 525       return cursor+1;
 526     else
 527       return cursor;
 528   }else if(strcmp(var_test->name, var) < 0)
 529     return cursor+1;
 530   else
 531     return cursor;
 532
 533 }
 534
 535 /** \brief Fill DWARf debug infomations (types, frames, variables ...). */
 536 void MC_dwarf_get_variables(mc_object_info_t info) {
 537   if(MC_USE_LIBDW_TYPES)
 538     MC_dwarf_get_variables_libdw(info);
 539   mc_object_info_t result = info;
 540   const char *elf_file = info->file_name;
 541
 542   xbt_dict_t location_list = MC_dwarf_get_location_list(elf_file);
 543
 544   char *command = bprintf("LANG=C objdump -Wi %s", elf_file);
 545
 546   FILE *fp = popen(command, "r");
 547
 548   if(fp == NULL)
 549     perror("popen for objdump failed");
 550
 551   xbt_dict_t *local_variables = &result->local_variables;
 552   xbt_dynar_t *global_variables = &result->global_variables;
 553   xbt_dict_t *types = &result->types;
 554
 555   char *line = NULL, *origin, *abstract_origin, *current_frame = NULL,
 556     *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
 557     *node_type = NULL, *location_type = NULL, *variable_name = NULL,
 558     *loc_expr = NULL, *name = NULL, *end =NULL, *type_origin = NULL, *global_address = NULL,
 559     *parent_value = NULL;
 560
 561   ssize_t read =0;
 562   size_t n = 0;
 563   int global_variable = 0, parent = 0, new_frame = 0, new_variable = 1, size = 0,
 564     is_pointer = 0, struct_decl = 0, member_end = 0,
 565     enumeration_size = 0, subrange = 0, union_decl = 0, offset = 0, index = 0;
 566
 567   xbt_dynar_t split = NULL, split2 = NULL;
 568
 569   xbt_dict_t variables_origin = xbt_dict_new_homogeneous(xbt_free);
 570   xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(xbt_free);
 571
 572   dw_frame_t variable_frame, subroutine_frame = NULL;
 573
 574   e_dw_type_type type_type = -1;
 575
 576   read = xbt_getline(&line, &n, fp);
 577
 578   while (read != -1) {
 579
 580     /* Wipeout the new line character */
 581     line[read - 1] = '\0';
 582
 583     if(n == 0 || strlen(line) == 0){
 584       read = xbt_getline(&line, &n, fp);
 585       continue;
 586     }
 587
 588     xbt_str_ltrim(line, NULL);
 589     xbt_str_strip_spaces(line);
 590
 591     if(line[0] != '<'){
 592       read = xbt_getline(&line, &n, fp);
 593       continue;
 594     }
 595
 596     xbt_dynar_free(&split);
 597     split = xbt_str_split(line, " ");
 598
 599     /* Get node type */
 600     node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 601
 602     if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
 603       /* We build/complete a dw_frame_t object
 604        * and append it if necessary to the local_variables dictionnary */
 605
 606       dw_frame_t frame = NULL;
 607
 608       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 609       subprogram_start = xbt_strdup(strtok(NULL, "<"));
 610       xbt_str_rtrim(subprogram_start, ">:");
 611
 612       read = xbt_getline(&line, &n, fp);
 613
 614       while(read != -1){
 615
 616         /* Wipeout the new line character */
 617         line[read - 1] = '\0';
 618
 619         if(n == 0 || strlen(line) == 0){
 620           read = xbt_getline(&line, &n, fp);
 621           continue;
 622         }
 623
 624         xbt_dynar_free(&split);
 625         xbt_str_rtrim(line, NULL);
 626         xbt_str_strip_spaces(line);
 627         split = xbt_str_split(line, " ");
 628
 629         node_type = xbt_dynar_get_as(split, 1, char *);
 630
 631         if(strncmp(node_type, "DW_AT_", 6) != 0)
 632           break;
 633
 634         if(strcmp(node_type, "DW_AT_sibling") == 0){
 635
 636           subprogram_end = xbt_strdup(xbt_dynar_get_as(split, 3, char*));
 637           xbt_str_ltrim(subprogram_end, "<0x");
 638           xbt_str_rtrim(subprogram_end, ">");
 639
 640         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
 641
 642           new_frame = 0;
 643           abstract_origin = xbt_strdup(xbt_dynar_get_as(split, 2, char*));
 644           xbt_str_ltrim(abstract_origin, "<0x");
 645           xbt_str_rtrim(abstract_origin, ">");
 646           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
 647           frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
 648           xbt_free(abstract_origin);
 649
 650         }else if(strcmp(node_type, "DW_AT_name") == 0){
 651
 652           new_frame = 1;
 653           xbt_free(current_frame);
 654           frame = xbt_new0(s_dw_frame_t, 1);
 655           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 656           frame->variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
 657           frame->frame_base = xbt_new0(s_dw_location_t, 1);
 658           current_frame = strdup(frame->name);
 659
 660           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 661
 662         }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
 663
 664           location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 665
 666           if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
 667
 668             frame->frame_base = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
 669
 670           }else{
 671
 672             xbt_str_strip_spaces(line);
 673             split2 = xbt_str_split(line, "(");
 674             xbt_dynar_remove_at(split2, 0, NULL);
 675             loc_expr = xbt_str_join(split2, " ");
 676             xbt_str_rtrim(loc_expr, ")");
 677             frame->frame_base = MC_dwarf_get_location(NULL, loc_expr);
 678             xbt_dynar_free(&split2);
 679             xbt_free(loc_expr);
 680
 681           }
 682
 683         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 684
 685           if(frame != NULL)
 686             frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 687
 688         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 689
 690           if(frame != NULL)
 691             frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 692
 693         }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
 694
 695           xbt_free(frame->name);
 696           xbt_free(current_frame);
 697           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 698           current_frame = strdup(frame->name);
 699           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 700
 701         }
 702
 703         read = xbt_getline(&line, &n, fp);
 704
 705       }
 706
 707       if(new_frame == 1){
 708         frame->start = strtoul(subprogram_start, NULL, 16);
 709         if(subprogram_end != NULL)
 710           frame->end = strtoul(subprogram_end, NULL, 16);
 711         xbt_dict_set(*local_variables, frame->name, frame, NULL);
 712       }
 713
 714       xbt_free(subprogram_start);
 715       xbt_free(subprogram_end);
 716       subprogram_end = NULL;
 717
 718
 719     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
 720       /* We build a dw_variable_t object and append it either to
 721          the list of variables of the frame (local variable)
 722          or to the list of global variables (global variables). */
 723
 724       dw_variable_t var = NULL;
 725
 726       parent_value = strdup(xbt_dynar_get_as(split, 0, char *));
 727       parent_value = strtok(parent_value,"<");
 728       xbt_str_rtrim(parent_value, ">");
 729       parent = atoi(parent_value);
 730       xbt_free(parent_value);
 731
 732       if(parent == 1)
 733         global_variable = 1;
 734
 735       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 736       origin = xbt_strdup(strtok(NULL, "<"));
 737       xbt_str_rtrim(origin, ">:");
 738
 739       read = xbt_getline(&line, &n, fp);
 740
 741       while(read != -1){
 742
 743         /* Wipeout the new line character */
 744         line[read - 1] = '\0';
 745
 746         if(n == 0 || strlen(line) == 0){
 747           read = xbt_getline(&line, &n, fp);
 748           continue;
 749         }
 750
 751         xbt_dynar_free(&split);
 752         xbt_str_rtrim(line, NULL);
 753         xbt_str_strip_spaces(line);
 754         split = xbt_str_split(line, " ");
 755
 756         node_type = xbt_dynar_get_as(split, 1, char *);
 757
 758         if(strncmp(node_type, "DW_AT_", 6) != 0)
 759           break;
 760
 761         if(strcmp(node_type, "DW_AT_name") == 0){
 762
 763           var = xbt_new0(s_dw_variable_t, 1);
 764           var->name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 765           xbt_dict_set(variables_origin, origin, xbt_strdup(var->name), NULL);
 766
 767         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 768
 769           new_variable = 0;
 770
 771           abstract_origin = xbt_dynar_get_as(split, 2, char *);
 772           xbt_str_ltrim(abstract_origin, "<0x");
 773           xbt_str_rtrim(abstract_origin, ">");
 774
 775           variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
 776           variable_frame = MC_dwarf_get_frame_by_offset(*local_variables, strtoul(abstract_origin, NULL, 16));
 777           var = MC_dwarf_get_variable_by_name(variable_frame, variable_name);
 778
 779         }else if(strcmp(node_type, "DW_AT_location") == 0){
 780
 781           if(var != NULL){
 782
 783             if(!global_variable){
 784
 785               location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 786
 787               if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
 788                 var->address.location = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
 789               }else{
 790                 xbt_str_strip_spaces(line);
 791                 split2 = xbt_str_split(line, "(");
 792                 xbt_dynar_remove_at(split2, 0, NULL);
 793                 loc_expr = xbt_str_join(split2, " ");
 794                 xbt_str_rtrim(loc_expr, ")");
 795                 if(strncmp("DW_OP_addr", loc_expr, 10) == 0){
 796                   global_variable = 1;
 797                   xbt_dynar_free(&split2);
 798                   split2 = xbt_str_split(loc_expr, " ");
 799                   if(strcmp(elf_file, xbt_binary_name) != 0)
 800                     var->address.address = (char *) info->start_text + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
 801                   else
 802                     // Why is it different ?
 803                     var->address.address = (void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16);
 804                 }else{
 805                   var->address.location = MC_dwarf_get_location(NULL, loc_expr);
 806                 }
 807                 xbt_dynar_free(&split2);
 808                 xbt_free(loc_expr);
 809               }
 810             }else{
 811               global_address = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 812               xbt_str_rtrim(global_address, ")");
 813               if(strcmp(elf_file, xbt_binary_name) != 0)
 814                 var->address.address = (char *) info->start_text + (long)((void *)strtoul(global_address, NULL, 16));
 815               else
 816                 // Why is it different ?
 817                 var->address.address = (void *)strtoul(global_address, NULL, 16);
 818               xbt_free(global_address);
 819               global_address = NULL;
 820             }
 821
 822           }
 823
 824         }else if(strcmp(node_type, "DW_AT_type") == 0){
 825
 826           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
 827           xbt_str_ltrim(type_origin, "<0x");
 828           xbt_str_rtrim(type_origin, ">");
 829
 830         }else if(strcmp(node_type, "DW_AT_declaration") == 0){
 831
 832           new_variable = 0;
 833           if(new_variable){
 834             dw_variable_free(var);
 835             var = NULL;
 836           }
 837
 838         }else if(strcmp(node_type, "DW_AT_artificial") == 0){
 839
 840           new_variable = 0;
 841           if(new_variable){
 842             dw_variable_free(var);
 843             var = NULL;
 844           }
 845
 846         }
 847
 848         read = xbt_getline(&line, &n, fp);
 849
 850       }
 851
 852       if(new_variable == 1){
 853
 854         if(!global_variable){
 855           variable_frame = xbt_dict_get_or_null(*local_variables, current_frame);
 856           var->type_origin = strdup(type_origin);
 857           var->global = 0;
 858           index = MC_dwarf_get_variable_index(variable_frame->variables, var->name, NULL);
 859           if(index != -1)
 860             xbt_dynar_insert_at(variable_frame->variables, index, &var);
 861         }else{
 862           var->type_origin = strdup(type_origin);
 863           var->global = 1;
 864           index = MC_dwarf_get_variable_index(*global_variables, var->name, var->address.address);
 865           if(index != -1)
 866             xbt_dynar_insert_at(*global_variables, index, &var);
 867         }
 868
 869          xbt_free(type_origin);
 870          type_origin = NULL;
 871       }
 872
 873       global_variable = 0;
 874       new_variable = 1;
 875
 876     }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
 877       /* Update the information on the frame (we should duplicate it instead). */
 878
 879       read = xbt_getline(&line, &n, fp);
 880
 881       while(read != -1){
 882
 883         /* Wipeout the new line character */
 884         line[read - 1] = '\0';
 885
 886         if(n == 0 || strlen(line) == 0){
 887           read = xbt_getline(&line, &n, fp);
 888           continue;
 889         }
 890
 891         xbt_dynar_free(&split);
 892         xbt_str_rtrim(line, NULL);
 893         xbt_str_strip_spaces(line);
 894         split = xbt_str_split(line, " ");
 895
 896         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
 897           break;
 898
 899         node_type = xbt_dynar_get_as(split, 1, char *);
 900
 901         if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 902
 903           origin = xbt_dynar_get_as(split, 2, char *);
 904           xbt_str_ltrim(origin, "<0x");
 905           xbt_str_rtrim(origin, ">");
 906
 907           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
 908           subroutine_frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
 909
 910         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 911
 912           subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 913
 914         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 915
 916           subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 917         }
 918
 919         read = xbt_getline(&line, &n, fp);
 920
 921       }
 922
 923     }else if(!MC_USE_LIBDW_TYPES&&(strcmp(node_type, "(DW_TAG_base_type)") == 0
 924              || strcmp(node_type, "(DW_TAG_enumeration_type)") == 0
 925              || strcmp(node_type, "(DW_TAG_typedef)") == 0
 926              || strcmp(node_type, "(DW_TAG_const_type)") == 0
 927              || strcmp(node_type, "(DW_TAG_subroutine_type)") == 0
 928              || strcmp(node_type, "(DW_TAG_volatile_type)") == 0
 929              || (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)")))){
 930
 931       /* Create the and add it to the types dictionnary */
 932
 933       if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
 934         type_type = DW_TAG_base_type;
 935       else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
 936         type_type = DW_TAG_enumeration_type;
 937       else if(strcmp(node_type, "(DW_TAG_typedef)") == 0)
 938         type_type = DW_TAG_typedef;
 939       else if(strcmp(node_type, "(DW_TAG_const_type)") == 0)
 940         type_type = DW_TAG_const_type;
 941       else if(strcmp(node_type, "(DW_TAG_pointer_type)") == 0)
 942         type_type = DW_TAG_pointer_type;
 943       else if(strcmp(node_type, "(DW_TAG_subroutine_type)") == 0)
 944         type_type = DW_TAG_subroutine_type;
 945       else if(strcmp(node_type, "(DW_TAG_volatile_type)") == 0)
 946         type_type = DW_TAG_volatile_type;
 947
 948       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 949       origin = strdup(strtok(NULL, "<"));
 950       xbt_str_rtrim(origin, ">:");
 951
 952       read = xbt_getline(&line, &n, fp);
 953
 954       while(read != -1){
 955
 956          /* Wipeout the new line character */
 957         line[read - 1] = '\0';
 958
 959         if(n == 0 || strlen(line) == 0){
 960           read = xbt_getline(&line, &n, fp);
 961           continue;
 962         }
 963
 964         xbt_dynar_free(&split);
 965         xbt_str_rtrim(line, NULL);
 966         xbt_str_strip_spaces(line);
 967         split = xbt_str_split(line, " ");
 968
 969         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
 970           break;
 971
 972         node_type = xbt_dynar_get_as(split, 1, char *);
 973
 974         if(strcmp(node_type, "DW_AT_byte_size") == 0){
 975           size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
 976           if(type_type == DW_TAG_enumeration_type)
 977             enumeration_size = size;
 978         }else if(strcmp(node_type, "DW_AT_name") == 0){
 979           end = xbt_str_join(split, " ");
 980           xbt_dynar_free(&split);
 981           split = xbt_str_split(end, "):");
 982           xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
 983           name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
 984         }else if(strcmp(node_type, "DW_AT_type") == 0){
 985           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
 986           xbt_str_ltrim(type_origin, "<0x");
 987           xbt_str_rtrim(type_origin, ">");
 988         }
 989
 990         read = xbt_getline(&line, &n, fp);
 991       }
 992
 993       dw_type_t type = xbt_new0(s_dw_type_t, 1);
 994       type->type = type_type;
 995       if(name)
 996         type->name = xbt_strdup(name);
 997       else
 998         type->name = xbt_strdup("undefined");
 999       type->is_pointer_type = is_pointer;
1000       type->id = (void *)strtoul(origin, NULL, 16);
1001       if(type_origin)
1002         type->dw_type_id = xbt_strdup(type_origin);
1003
1004       type->byte_size = size;
1005       // Not relevant:
1006       type->element_count = -1;
1007
1008       type->members = NULL;
1009
1010       xbt_dict_set(*types, origin, type, NULL);
1011
1012       xbt_free(name);
1013       name = NULL;
1014       xbt_free(type_origin);
1015       type_origin = NULL;
1016       xbt_free(end);
1017       end = NULL;
1018
1019       is_pointer = 0;
1020       size = 0;
1021       xbt_free(origin);
1022
1023     }else if(strcmp(node_type, "(DW_TAG_structure_type)") == 0 || strcmp(node_type, "(DW_TAG_union_type)") == 0){
1024
1025       if(strcmp(node_type, "(DW_TAG_structure_type)") == 0)
1026         struct_decl = 1;
1027       else
1028         union_decl = 1;
1029
1030       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1031       origin = strdup(strtok(NULL, "<"));
1032       xbt_str_rtrim(origin, ">:");
1033
1034       read = xbt_getline(&line, &n, fp);
1035
1036       dw_type_t type = NULL;
1037
1038       while(read != -1){
1039
1040         while(read != -1){
1041
1042           /* Wipeout the new line character */
1043           line[read - 1] = '\0';
1044
1045           if(n == 0 || strlen(line) == 0){
1046             read = xbt_getline(&line, &n, fp);
1047             continue;
1048           }
1049
1050           xbt_dynar_free(&split);
1051           xbt_str_rtrim(line, NULL);
1052           xbt_str_strip_spaces(line);
1053           split = xbt_str_split(line, " ");
1054
1055           node_type = xbt_dynar_get_as(split, 1, char *);
1056
1057           if(strncmp(node_type, "DW_AT_", 6) != 0){
1058             member_end = 1;
1059             break;
1060           }
1061
1062           if(strcmp(node_type, "DW_AT_byte_size") == 0){
1063             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1064           }else if(strcmp(node_type, "DW_AT_name") == 0){
1065             xbt_free(end);
1066             end = xbt_str_join(split, " ");
1067             xbt_dynar_free(&split);
1068             split = xbt_str_split(end, "):");
1069             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1070             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1071           }else if(strcmp(node_type, "DW_AT_type") == 0){
1072             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1073             xbt_str_ltrim(type_origin, "<0x");
1074             xbt_str_rtrim(type_origin, ">");
1075           }else if(strcmp(node_type, "DW_AT_data_member_location:") == 0){
1076             xbt_free(end);
1077             end = xbt_str_join(split, " ");
1078             xbt_dynar_free(&split);
1079             split = xbt_str_split(end, "DW_OP_plus_uconst:");
1080             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), NULL);
1081             xbt_str_rtrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), ")");
1082             offset = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1083           }
1084
1085           read = xbt_getline(&line, &n, fp);
1086
1087         }
1088
1089         if(member_end && type){
1090           member_end = 0;
1091
1092           // Why are we not simply referencing, the DW_AT_type?
1093           dw_type_t member_type = xbt_new0(s_dw_type_t, 1);
1094           member_type->name = xbt_strdup(name);
1095           member_type->byte_size = size;
1096           member_type->element_count = -1;
1097           member_type->is_pointer_type = is_pointer;
1098           member_type->id = (void *)strtoul(origin, NULL, 16);
1099           member_type->offset = offset;
1100           if(type_origin)
1101             member_type->dw_type_id = xbt_strdup(type_origin);
1102
1103           xbt_dynar_push(type->members, &member_type);
1104
1105           xbt_free(name);
1106           name = NULL;
1107           xbt_free(end);
1108           end = NULL;
1109           xbt_free(type_origin);
1110           type_origin = NULL;
1111           size = 0;
1112           offset = 0;
1113
1114           xbt_free(origin);
1115           origin = NULL;
1116           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1117           origin = strdup(strtok(NULL, "<"));
1118           xbt_str_rtrim(origin, ">:");
1119
1120         }
1121
1122         if(struct_decl || union_decl){
1123           type = xbt_new0(s_dw_type_t, 1);
1124           if(struct_decl)
1125             type->type = DW_TAG_structure_type;
1126           else
1127             type->type = DW_TAG_union_type;
1128           type->name = xbt_strdup(name);
1129           type->byte_size = size;
1130           type->element_count = -1;
1131           type->is_pointer_type = is_pointer;
1132           type->id = (void *)strtoul(origin, NULL, 16);
1133           if(type_origin)
1134             type->dw_type_id = xbt_strdup(type_origin);
1135           type->members = xbt_dynar_new(sizeof(dw_type_t), dw_type_free_voidp);
1136
1137           xbt_dict_set(*types, origin, type, NULL);
1138
1139           xbt_free(name);
1140           name = NULL;
1141           xbt_free(end);
1142           end = NULL;
1143           xbt_free(type_origin);
1144           type_origin = NULL;
1145           size = 0;
1146           struct_decl = 0;
1147           union_decl = 0;
1148
1149         }
1150
1151         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_member)") != 0)
1152           break;
1153
1154         read = xbt_getline(&line, &n, fp);
1155
1156       }
1157
1158       xbt_free(origin);
1159       origin = NULL;
1160
1161     }else if(strcmp(node_type, "(DW_TAG_array_type)") == 0){
1162
1163       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1164       origin = strdup(strtok(NULL, "<"));
1165       xbt_str_rtrim(origin, ">:");
1166
1167       read = xbt_getline(&line, &n, fp);
1168
1169       dw_type_t type = NULL;
1170
1171       // Read DW_TAG_subrange_type children:
1172       while(read != -1){
1173
1174         // Read attributes of the DW_TAG_subrange_type:
1175         while(read != -1){
1176
1177           /* Wipeout the new line character */
1178           line[read - 1] = '\0';
1179
1180           if(n == 0 || strlen(line) == 0){
1181             read = xbt_getline(&line, &n, fp);
1182             continue;
1183           }
1184
1185           xbt_dynar_free(&split);
1186           xbt_str_rtrim(line, NULL);
1187           xbt_str_strip_spaces(line);
1188           split = xbt_str_split(line, " ");
1189
1190           node_type = xbt_dynar_get_as(split, 1, char *);
1191
1192           if(strncmp(node_type, "DW_AT_", 6) != 0)
1193             break;
1194
1195           if(strcmp(node_type, "DW_AT_upper_bound") == 0){
1196             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1197           }else if(strcmp(node_type, "DW_AT_name") == 0){
1198             end = xbt_str_join(split, " ");
1199             xbt_dynar_free(&split);
1200             split = xbt_str_split(end, "):");
1201             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1202             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1203           }else if(strcmp(node_type, "DW_AT_type") == 0){
1204             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1205             xbt_str_ltrim(type_origin, "<0x");
1206             xbt_str_rtrim(type_origin, ">");
1207           }
1208
1209           read = xbt_getline(&line, &n, fp);
1210
1211         }
1212
1213         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") == 0){
1214           subrange = 1;
1215         }
1216
1217         if(subrange && type){
1218           type->element_count = size;
1219
1220           xbt_free(name);
1221           name = NULL;
1222           xbt_free(end);
1223           end = NULL;
1224           xbt_free(type_origin);
1225           type_origin = NULL;
1226           size = 0;
1227
1228           xbt_free(origin);
1229           origin = NULL;
1230           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1231           origin = strdup(strtok(NULL, "<"));
1232           xbt_str_rtrim(origin, ">:");
1233
1234         }else {
1235
1236           type = xbt_new0(s_dw_type_t, 1);
1237           type->type = DW_TAG_array_type;
1238           type->name = xbt_strdup(name);
1239           type->is_pointer_type = is_pointer;
1240           type->id = (void *)strtoul(origin, NULL, 16);
1241           if(type_origin)
1242             type->dw_type_id = xbt_strdup(type_origin);
1243           type->members = NULL;
1244
1245           // Filled in a post processing step:
1246           type-> byte_size = 0;
1247
1248           xbt_dict_set(*types, origin, type, NULL);
1249
1250           xbt_free(name);
1251           name = NULL;
1252           xbt_free(end);
1253           end = NULL;
1254           xbt_free(type_origin);
1255           type_origin = NULL;
1256           size = 0;
1257         }
1258
1259         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") != 0)
1260           break;
1261
1262         read = xbt_getline(&line, &n, fp);
1263
1264       }
1265
1266       xbt_free(origin);
1267       origin = NULL;
1268
1269     }else{
1270
1271       read = xbt_getline(&line, &n, fp);
1272
1273     }
1274
1275   }
1276
1277   xbt_dynar_free(&split);
1278   xbt_dict_free(&variables_origin);
1279   xbt_dict_free(&subprograms_origin);
1280   xbt_free(line);
1281   xbt_free(command);
1282   xbt_dict_free(&location_list);
1283
1284   pclose(fp);
1285
1286   MC_post_process_types(info);
1287 }
1288
1289 static void MC_post_process_array_size(mc_object_info_t info, dw_type_t type) {
1290   xbt_assert(type->dw_type_id, "No base type for array <%p>%s", type->id, type->name);
1291   dw_type_t subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
1292   xbt_assert(subtype, "Unkown base type <%s> for array <%p>%s", type->dw_type_id, type->id, type->name);
1293   if(subtype->type==DW_TAG_array_type && type->byte_size==0) {
1294           MC_post_process_array_size(info, subtype);
1295   }
1296   type->byte_size = type->element_count*subtype->byte_size;
1297 }
1298
1299 static void MC_post_process_types(mc_object_info_t info) {
1300   xbt_dict_cursor_t cursor;
1301   char *origin;
1302   dw_type_t type;
1303   xbt_dict_foreach(info->types, cursor, origin, type){
1304     if(type->type==DW_TAG_array_type && type->byte_size==0)
1305       MC_post_process_array_size(info, type);
1306   }
1307 }
1308
1309 /*******************************  Ignore mechanism *******************************/
1310 /*********************************************************************************/
1311
1312 xbt_dynar_t mc_checkpoint_ignore;
1313
1314 typedef struct s_mc_stack_ignore_variable{
1315   char *var_name;
1316   char *frame;
1317 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
1318
1319 typedef struct s_mc_data_bss_ignore_variable{
1320   char *name;
1321 }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
1322
1323 /**************************** Free functions ******************************/
1324
1325 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
1326   xbt_free(v->var_name);
1327   xbt_free(v->frame);
1328   xbt_free(v);
1329 }
1330
1331 static void stack_ignore_variable_free_voidp(void *v){
1332   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
1333 }
1334
1335 void heap_ignore_region_free(mc_heap_ignore_region_t r){
1336   xbt_free(r);
1337 }
1338
1339 void heap_ignore_region_free_voidp(void *r){
1340   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
1341 }
1342
1343 static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
1344   xbt_free(v->name);
1345   xbt_free(v);
1346 }
1347
1348 static void data_bss_ignore_variable_free_voidp(void *v){
1349   data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
1350 }
1351
1352 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
1353   xbt_free(r);
1354 }
1355
1356 static void checkpoint_ignore_region_free_voidp(void *r){
1357   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
1358 }
1359
1360 /***********************************************************************/
1361
1362 void MC_ignore_heap(void *address, size_t size){
1363
1364   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1365
1366   MC_SET_RAW_MEM;
1367
1368   mc_heap_ignore_region_t region = NULL;
1369   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
1370   region->address = address;
1371   region->size = size;
1372
1373   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1374
1375   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
1376     region->fragment = -1;
1377     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
1378   }else{
1379     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
1380     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
1381   }
1382
1383   if(mc_heap_comparison_ignore == NULL){
1384     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
1385     xbt_dynar_push(mc_heap_comparison_ignore, &region);
1386     if(!raw_mem_set)
1387       MC_UNSET_RAW_MEM;
1388     return;
1389   }
1390
1391   unsigned int cursor = 0;
1392   mc_heap_ignore_region_t current_region = NULL;
1393   int start = 0;
1394   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1395
1396   while(start <= end){
1397     cursor = (start + end) / 2;
1398     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1399     if(current_region->address == address){
1400       heap_ignore_region_free(region);
1401       if(!raw_mem_set)
1402         MC_UNSET_RAW_MEM;
1403       return;
1404     }else if(current_region->address < address){
1405       start = cursor + 1;
1406     }else{
1407       end = cursor - 1;
1408     }
1409   }
1410
1411   if(current_region->address < address)
1412     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
1413   else
1414     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
1415
1416   if(!raw_mem_set)
1417     MC_UNSET_RAW_MEM;
1418 }
1419
1420 void MC_remove_ignore_heap(void *address, size_t size){
1421
1422   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1423
1424   MC_SET_RAW_MEM;
1425
1426   unsigned int cursor = 0;
1427   int start = 0;
1428   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1429   mc_heap_ignore_region_t region;
1430   int ignore_found = 0;
1431
1432   while(start <= end){
1433     cursor = (start + end) / 2;
1434     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1435     if(region->address == address){
1436       ignore_found = 1;
1437       break;
1438     }else if(region->address < address){
1439       start = cursor + 1;
1440     }else{
1441       if((char * )region->address <= ((char *)address + size)){
1442         ignore_found = 1;
1443         break;
1444       }else{
1445         end = cursor - 1;
1446       }
1447     }
1448   }
1449
1450   if(ignore_found == 1){
1451     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
1452     MC_remove_ignore_heap(address, size);
1453   }
1454
1455   if(!raw_mem_set)
1456     MC_UNSET_RAW_MEM;
1457
1458 }
1459
1460 void MC_ignore_global_variable(const char *name){
1461
1462   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1463
1464   MC_SET_RAW_MEM;
1465
1466   if(mc_libsimgrid_info){
1467
1468     unsigned int cursor = 0;
1469     dw_variable_t current_var;
1470     int start = 0;
1471     int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
1472
1473     while(start <= end){
1474       cursor = (start + end) /2;
1475       current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
1476       if(strcmp(current_var->name, name) == 0){
1477         xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
1478         start = 0;
1479         end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
1480       }else if(strcmp(current_var->name, name) < 0){
1481         start = cursor + 1;
1482       }else{
1483         end = cursor - 1;
1484       }
1485     }
1486
1487   }else{
1488
1489     if(mc_data_bss_comparison_ignore == NULL)
1490       mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
1491
1492     mc_data_bss_ignore_variable_t var = NULL;
1493     var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
1494     var->name = strdup(name);
1495
1496     if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
1497
1498       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
1499
1500     }else{
1501
1502       unsigned int cursor = 0;
1503       int start = 0;
1504       int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
1505       mc_data_bss_ignore_variable_t current_var = NULL;
1506
1507       while(start <= end){
1508         cursor = (start + end) / 2;
1509         current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
1510         if(strcmp(current_var->name, name) == 0){
1511           data_bss_ignore_variable_free(var);
1512           if(!raw_mem_set)
1513             MC_UNSET_RAW_MEM;
1514           return;
1515         }else if(strcmp(current_var->name, name) < 0){
1516           start = cursor + 1;
1517         }else{
1518           end = cursor - 1;
1519         }
1520       }
1521
1522       if(strcmp(current_var->name, name) < 0)
1523         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
1524       else
1525         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
1526
1527     }
1528   }
1529
1530   if(!raw_mem_set)
1531     MC_UNSET_RAW_MEM;
1532 }
1533
1534 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
1535
1536   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1537
1538   MC_SET_RAW_MEM;
1539
1540   if(mc_libsimgrid_info){
1541     unsigned int cursor = 0;
1542     dw_variable_t current_var;
1543     int start, end;
1544     if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
1545       xbt_dict_cursor_t dict_cursor;
1546       char *current_frame_name;
1547       dw_frame_t frame;
1548       xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
1549         start = 0;
1550         end = xbt_dynar_length(frame->variables) - 1;
1551         while(start <= end){
1552           cursor = (start + end) / 2;
1553           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1554           if(strcmp(current_var->name, var_name) == 0){
1555             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1556             start = 0;
1557             end = xbt_dynar_length(frame->variables) - 1;
1558           }else if(strcmp(current_var->name, var_name) < 0){
1559             start = cursor + 1;
1560           }else{
1561             end = cursor - 1;
1562           }
1563         }
1564       }
1565        xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
1566         start = 0;
1567         end = xbt_dynar_length(frame->variables) - 1;
1568         while(start <= end){
1569           cursor = (start + end) / 2;
1570           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1571           if(strcmp(current_var->name, var_name) == 0){
1572             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1573             start = 0;
1574             end = xbt_dynar_length(frame->variables) - 1;
1575           }else if(strcmp(current_var->name, var_name) < 0){
1576             start = cursor + 1;
1577           }else{
1578             end = cursor - 1;
1579           }
1580         }
1581       }
1582     }else{
1583       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
1584                                       mc_libsimgrid_info->local_variables, frame_name))->variables;
1585       start = 0;
1586       end = xbt_dynar_length(variables_list) - 1;
1587       while(start <= end){
1588         cursor = (start + end) / 2;
1589         current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
1590         if(strcmp(current_var->name, var_name) == 0){
1591           xbt_dynar_remove_at(variables_list, cursor, NULL);
1592           start = 0;
1593           end = xbt_dynar_length(variables_list) - 1;
1594         }else if(strcmp(current_var->name, var_name) < 0){
1595           start = cursor + 1;
1596         }else{
1597           end = cursor - 1;
1598         }
1599       }
1600     }
1601   }else{
1602
1603     if(mc_stack_comparison_ignore == NULL)
1604       mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
1605
1606     mc_stack_ignore_variable_t var = NULL;
1607     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
1608     var->var_name = strdup(var_name);
1609     var->frame = strdup(frame_name);
1610
1611     if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
1612
1613       xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
1614
1615     }else{
1616
1617       unsigned int cursor = 0;
1618       int start = 0;
1619       int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
1620       mc_stack_ignore_variable_t current_var = NULL;
1621
1622       while(start <= end){
1623         cursor = (start + end) / 2;
1624         current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
1625         if(strcmp(current_var->frame, frame_name) == 0){
1626           if(strcmp(current_var->var_name, var_name) == 0){
1627             stack_ignore_variable_free(var);
1628             if(!raw_mem_set)
1629               MC_UNSET_RAW_MEM;
1630             return;
1631           }else if(strcmp(current_var->var_name, var_name) < 0){
1632             start = cursor + 1;
1633           }else{
1634             end = cursor - 1;
1635           }
1636         }else if(strcmp(current_var->frame, frame_name) < 0){
1637           start = cursor + 1;
1638         }else{
1639           end = cursor - 1;
1640         }
1641       }
1642
1643       if(strcmp(current_var->frame, frame_name) == 0){
1644         if(strcmp(current_var->var_name, var_name) < 0){
1645           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1646         }else{
1647           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1648         }
1649       }else if(strcmp(current_var->frame, frame_name) < 0){
1650         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1651       }else{
1652         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1653       }
1654     }
1655   }
1656
1657   if(!raw_mem_set)
1658     MC_UNSET_RAW_MEM;
1659
1660 }
1661
1662 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
1663
1664   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1665
1666   MC_SET_RAW_MEM;
1667
1668   if(stacks_areas == NULL)
1669     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
1670
1671   stack_region_t region = NULL;
1672   region = xbt_new0(s_stack_region_t, 1);
1673   region->address = stack;
1674   region->process_name = strdup(name);
1675   region->context = context;
1676   region->size = size;
1677   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1678   xbt_dynar_push(stacks_areas, &region);
1679
1680   if(!raw_mem_set)
1681     MC_UNSET_RAW_MEM;
1682 }
1683
1684 void MC_ignore(void *addr, size_t size){
1685
1686   int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
1687
1688   MC_SET_RAW_MEM;
1689
1690   if(mc_checkpoint_ignore == NULL)
1691     mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
1692
1693   mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
1694   region->addr = addr;
1695   region->size = size;
1696
1697   if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
1698     xbt_dynar_push(mc_checkpoint_ignore, &region);
1699   }else{
1700
1701     unsigned int cursor = 0;
1702     int start = 0;
1703     int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
1704     mc_checkpoint_ignore_region_t current_region = NULL;
1705
1706     while(start <= end){
1707       cursor = (start + end) / 2;
1708       current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
1709       if(current_region->addr == addr){
1710         if(current_region->size == size){
1711           checkpoint_ignore_region_free(region);
1712           if(!raw_mem_set)
1713             MC_UNSET_RAW_MEM;
1714           return;
1715         }else if(current_region->size < size){
1716           start = cursor + 1;
1717         }else{
1718           end = cursor - 1;
1719         }
1720       }else if(current_region->addr < addr){
1721           start = cursor + 1;
1722       }else{
1723         end = cursor - 1;
1724       }
1725     }
1726
1727      if(current_region->addr == addr){
1728        if(current_region->size < size){
1729         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
1730       }else{
1731         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
1732       }
1733     }else if(current_region->addr < addr){
1734        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
1735     }else{
1736        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
1737     }
1738   }
1739
1740   if(!raw_mem_set)
1741     MC_UNSET_RAW_MEM;
1742 }
1743
1744 /*******************************  Initialisation of MC *******************************/
1745 /*********************************************************************************/
1746
1747 static void MC_dump_ignored_local_variables(void){
1748
1749   if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
1750     return;
1751
1752   unsigned int cursor = 0;
1753   mc_stack_ignore_variable_t current_var;
1754
1755   xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
1756     MC_ignore_local_variable(current_var->var_name, current_var->frame);
1757   }
1758
1759   xbt_dynar_free(&mc_stack_comparison_ignore);
1760   mc_stack_comparison_ignore = NULL;
1761
1762 }
1763
1764 static void MC_dump_ignored_global_variables(void){
1765
1766   if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
1767     return;
1768
1769   unsigned int cursor = 0;
1770   mc_data_bss_ignore_variable_t current_var;
1771
1772   xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
1773     MC_ignore_global_variable(current_var->name);
1774   }
1775
1776   xbt_dynar_free(&mc_data_bss_comparison_ignore);
1777   mc_data_bss_comparison_ignore = NULL;
1778
1779 }
1780
1781 static void MC_init_debug_info();
1782 static void MC_init_debug_info() {
1783   XBT_INFO("Get debug information ...");
1784
1785   memory_map_t maps = MC_get_memory_map();
1786
1787   /* Get local variables for state equality detection */
1788   mc_binary_info = MC_find_object_info(maps, xbt_binary_name);
1789   mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path);
1790
1791   MC_free_memory_map(maps);
1792   XBT_INFO("Get debug information done !");
1793 }
1794
1795 void MC_init(){
1796
1797   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1798
1799   compare = 0;
1800
1801   /* Initialize the data structures that must be persistent across every
1802      iteration of the model-checker (in RAW memory) */
1803
1804   MC_SET_RAW_MEM;
1805
1806   MC_init_memory_map_info();
1807   MC_init_debug_info();
1808
1809   /* Remove variables ignored before getting list of variables */
1810   MC_dump_ignored_local_variables();
1811   MC_dump_ignored_global_variables();
1812
1813    /* Init parmap */
1814   parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
1815
1816   MC_UNSET_RAW_MEM;
1817
1818    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
1819   MC_ignore_local_variable("e", "*");
1820   MC_ignore_local_variable("__ex_cleanup", "*");
1821   MC_ignore_local_variable("__ex_mctx_en", "*");
1822   MC_ignore_local_variable("__ex_mctx_me", "*");
1823   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
1824   MC_ignore_local_variable("_log_ev", "*");
1825   MC_ignore_local_variable("_throw_ctx", "*");
1826   MC_ignore_local_variable("ctx", "*");
1827
1828   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
1829   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
1830
1831   /* Ignore local variable about time used for tracing */
1832   MC_ignore_local_variable("start_time", "*");
1833
1834   MC_ignore_global_variable("mc_comp_times");
1835   MC_ignore_global_variable("mc_snapshot_comparison_time");
1836   MC_ignore_global_variable("mc_time");
1837   MC_ignore_global_variable("smpi_current_rank");
1838   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
1839   MC_ignore_global_variable("maestro_stack_start");
1840   MC_ignore_global_variable("maestro_stack_end");
1841
1842   MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
1843   MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
1844   MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
1845   MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
1846
1847   smx_process_t process;
1848   xbt_swag_foreach(process, simix_global->process_list){
1849     MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
1850   }
1851
1852   if(raw_mem_set)
1853     MC_SET_RAW_MEM;
1854
1855 }
1856
1857 static void MC_init_dot_output(){ /* FIXME : more colors */
1858
1859   colors[0] = "blue";
1860   colors[1] = "red";
1861   colors[2] = "green3";
1862   colors[3] = "goldenrod";
1863   colors[4] = "brown";
1864   colors[5] = "purple";
1865   colors[6] = "magenta";
1866   colors[7] = "turquoise4";
1867   colors[8] = "gray25";
1868   colors[9] = "forestgreen";
1869   colors[10] = "hotpink";
1870   colors[11] = "lightblue";
1871   colors[12] = "tan";
1872
1873   dot_output = fopen(_sg_mc_dot_output_file, "w");
1874
1875   if(dot_output == NULL){
1876     perror("Error open dot output file");
1877     xbt_abort();
1878   }
1879
1880   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");
1881
1882 }
1883
1884 /*******************************  Core of MC *******************************/
1885 /**************************************************************************/
1886
1887 void MC_do_the_modelcheck_for_real() {
1888
1889   MC_SET_RAW_MEM;
1890   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
1891   MC_UNSET_RAW_MEM;
1892
1893   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1894     if (mc_reduce_kind==e_mc_reduce_unset)
1895       mc_reduce_kind=e_mc_reduce_dpor;
1896
1897     XBT_INFO("Check a safety property");
1898     MC_modelcheck_safety();
1899
1900   } else  {
1901
1902     if (mc_reduce_kind==e_mc_reduce_unset)
1903       mc_reduce_kind=e_mc_reduce_none;
1904
1905     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1906     MC_automaton_load(_sg_mc_property_file);
1907     MC_modelcheck_liveness();
1908   }
1909 }
1910
1911 void MC_modelcheck_safety(void)
1912 {
1913   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1914
1915   /* Check if MC is already initialized */
1916   if (initial_state_safety)
1917     return;
1918
1919   mc_time = xbt_new0(double, simix_process_maxpid);
1920
1921   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1922   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1923
1924   /* Initialize the data structures that must be persistent across every
1925      iteration of the model-checker (in RAW memory) */
1926
1927   MC_SET_RAW_MEM;
1928
1929   /* Initialize statistics */
1930   mc_stats = xbt_new0(s_mc_stats_t, 1);
1931   mc_stats->state_size = 1;
1932
1933   /* Create exploration stack */
1934   mc_stack_safety = xbt_fifo_new();
1935
1936   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1937     MC_init_dot_output();
1938
1939   MC_UNSET_RAW_MEM;
1940
1941   if(_sg_mc_visited > 0){
1942     MC_init();
1943   }else{
1944     MC_SET_RAW_MEM;
1945     MC_init_memory_map_info();
1946     MC_init_debug_info();
1947     MC_UNSET_RAW_MEM;
1948   }
1949
1950   MC_dpor_init();
1951
1952   MC_SET_RAW_MEM;
1953   /* Save the initial state */
1954   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1955   initial_state_safety->snapshot = MC_take_snapshot(0);
1956   MC_UNSET_RAW_MEM;
1957
1958   MC_dpor();
1959
1960   if(raw_mem_set)
1961     MC_SET_RAW_MEM;
1962
1963   xbt_abort();
1964   //MC_exit();
1965 }
1966
1967 void MC_modelcheck_liveness(){
1968
1969   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1970
1971   MC_init();
1972
1973   mc_time = xbt_new0(double, simix_process_maxpid);
1974
1975   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1976   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1977
1978   MC_SET_RAW_MEM;
1979
1980   /* Initialize statistics */
1981   mc_stats = xbt_new0(s_mc_stats_t, 1);
1982   mc_stats->state_size = 1;
1983
1984   /* Create exploration stack */
1985   mc_stack_liveness = xbt_fifo_new();
1986
1987   /* Create the initial state */
1988   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1989
1990   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1991     MC_init_dot_output();
1992
1993   MC_UNSET_RAW_MEM;
1994
1995   MC_ddfs_init();
1996
1997   /* We're done */
1998   MC_print_statistics(mc_stats);
1999   xbt_free(mc_time);
2000
2001   if(raw_mem_set)
2002     MC_SET_RAW_MEM;
2003
2004 }
2005
2006
2007 void MC_exit(void)
2008 {
2009   xbt_free(mc_time);
2010   MC_memory_exit();
2011   //xbt_abort();
2012 }
2013
2014 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
2015
2016   return simcall->mc_value;
2017 }
2018
2019
2020 int MC_random(int min, int max)
2021 {
2022   /*FIXME: return mc_current_state->executed_transition->random.value;*/
2023   return simcall_mc_random(min, max);
2024 }
2025
2026 /**
2027  * \brief Schedules all the process that are ready to run
2028  */
2029 void MC_wait_for_requests(void)
2030 {
2031   smx_process_t process;
2032   smx_simcall_t req;
2033   unsigned int iter;
2034
2035   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
2036     SIMIX_process_runall();
2037     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
2038       req = &process->simcall;
2039       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
2040         SIMIX_simcall_pre(req, 0);
2041     }
2042   }
2043 }
2044
2045 int MC_deadlock_check()
2046 {
2047   int deadlock = FALSE;
2048   smx_process_t process;
2049   if(xbt_swag_size(simix_global->process_list)){
2050     deadlock = TRUE;
2051     xbt_swag_foreach(process, simix_global->process_list){
2052       if(process->simcall.call != SIMCALL_NONE
2053          && MC_request_is_enabled(&process->simcall)){
2054         deadlock = FALSE;
2055         break;
2056       }
2057     }
2058   }
2059   return deadlock;
2060 }
2061
2062 /**
2063  * \brief Re-executes from the state at position start all the transitions indicated by
2064  *        a given model-checker stack.
2065  * \param stack The stack with the transitions to execute.
2066  * \param start Start index to begin the re-execution.
2067  */
2068 void MC_replay(xbt_fifo_t stack, int start)
2069 {
2070   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
2071
2072   int value, i = 1, count = 1;
2073   char *req_str;
2074   smx_simcall_t req = NULL, saved_req = NULL;
2075   xbt_fifo_item_t item, start_item;
2076   mc_state_t state;
2077   smx_process_t process = NULL;
2078
2079   XBT_DEBUG("**** Begin Replay ****");
2080
2081   if(start == -1){
2082     /* Restore the initial state */
2083     MC_restore_snapshot(initial_state_safety->snapshot);
2084     /* At the moment of taking the snapshot the raw heap was set, so restoring
2085      * it will set it back again, we have to unset it to continue  */
2086     MC_UNSET_RAW_MEM;
2087   }
2088
2089   start_item = xbt_fifo_get_last_item(stack);
2090   if(start != -1){
2091     while (i != start){
2092       start_item = xbt_fifo_get_prev_item(start_item);
2093       i++;
2094     }
2095   }
2096
2097   MC_SET_RAW_MEM;
2098   xbt_dict_reset(first_enabled_state);
2099   xbt_swag_foreach(process, simix_global->process_list){
2100     if(MC_process_is_enabled(process)){
2101       char *key = bprintf("%lu", process->pid);
2102       char *data = bprintf("%d", count);
2103       xbt_dict_set(first_enabled_state, key, data, NULL);
2104       xbt_free(key);
2105     }
2106   }
2107   MC_UNSET_RAW_MEM;
2108
2109
2110   /* Traverse the stack from the state at position start and re-execute the transitions */
2111   for (item = start_item;
2112        item != xbt_fifo_get_first_item(stack);
2113        item = xbt_fifo_get_prev_item(item)) {
2114
2115     state = (mc_state_t) xbt_fifo_get_item_content(item);
2116     saved_req = MC_state_get_executed_request(state, &value);
2117
2118     MC_SET_RAW_MEM;
2119     char *key = bprintf("%lu", saved_req->issuer->pid);
2120     xbt_dict_remove(first_enabled_state, key);
2121     xbt_free(key);
2122     MC_UNSET_RAW_MEM;
2123
2124     if(saved_req){
2125       /* because we got a copy of the executed request, we have to fetch the
2126          real one, pointed by the request field of the issuer process */
2127       req = &saved_req->issuer->simcall;
2128
2129       /* Debug information */
2130       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2131         req_str = MC_request_to_string(req, value);
2132         XBT_DEBUG("Replay: %s (%p)", req_str, state);
2133         xbt_free(req_str);
2134       }
2135     }
2136
2137     SIMIX_simcall_pre(req, value);
2138     MC_wait_for_requests();
2139
2140     count++;
2141
2142     MC_SET_RAW_MEM;
2143     /* Insert in dict all enabled processes */
2144     xbt_swag_foreach(process, simix_global->process_list){
2145       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
2146         char *key = bprintf("%lu", process->pid);
2147         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
2148           char *data = bprintf("%d", count);
2149           xbt_dict_set(first_enabled_state, key, data, NULL);
2150         }
2151         xbt_free(key);
2152       }
2153     }
2154     MC_UNSET_RAW_MEM;
2155
2156     /* Update statistics */
2157     mc_stats->visited_states++;
2158     mc_stats->executed_transitions++;
2159
2160   }
2161
2162   XBT_DEBUG("**** End Replay ****");
2163
2164   if(raw_mem)
2165     MC_SET_RAW_MEM;
2166   else
2167     MC_UNSET_RAW_MEM;
2168
2169
2170 }
2171
2172 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
2173 {
2174
2175   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2176
2177   int value;
2178   char *req_str;
2179   smx_simcall_t req = NULL, saved_req = NULL;
2180   xbt_fifo_item_t item;
2181   mc_state_t state;
2182   mc_pair_t pair;
2183   int depth = 1;
2184
2185   XBT_DEBUG("**** Begin Replay ****");
2186
2187   /* Restore the initial state */
2188   MC_restore_snapshot(initial_state_liveness->snapshot);
2189
2190   /* At the moment of taking the snapshot the raw heap was set, so restoring
2191    * it will set it back again, we have to unset it to continue  */
2192   if(!initial_state_liveness->raw_mem_set)
2193     MC_UNSET_RAW_MEM;
2194
2195   if(all_stack){
2196
2197     item = xbt_fifo_get_last_item(stack);
2198
2199     while(depth <= xbt_fifo_size(stack)){
2200
2201       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2202       state = (mc_state_t) pair->graph_state;
2203
2204       if(pair->requests > 0){
2205
2206         saved_req = MC_state_get_executed_request(state, &value);
2207         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2208
2209         if(saved_req != NULL){
2210           /* because we got a copy of the executed request, we have to fetch the
2211              real one, pointed by the request field of the issuer process */
2212           req = &saved_req->issuer->simcall;
2213           //XBT_DEBUG("Req->call %u", req->call);
2214
2215           /* Debug information */
2216           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2217             req_str = MC_request_to_string(req, value);
2218             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2219             xbt_free(req_str);
2220           }
2221
2222         }
2223
2224         SIMIX_simcall_pre(req, value);
2225         MC_wait_for_requests();
2226       }
2227
2228       depth++;
2229
2230       /* Update statistics */
2231       mc_stats->visited_pairs++;
2232       mc_stats->executed_transitions++;
2233
2234       item = xbt_fifo_get_prev_item(item);
2235     }
2236
2237   }else{
2238
2239     /* Traverse the stack from the initial state and re-execute the transitions */
2240     for (item = xbt_fifo_get_last_item(stack);
2241          item != xbt_fifo_get_first_item(stack);
2242          item = xbt_fifo_get_prev_item(item)) {
2243
2244       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2245       state = (mc_state_t) pair->graph_state;
2246
2247       if(pair->requests > 0){
2248
2249         saved_req = MC_state_get_executed_request(state, &value);
2250         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2251
2252         if(saved_req != NULL){
2253           /* because we got a copy of the executed request, we have to fetch the
2254              real one, pointed by the request field of the issuer process */
2255           req = &saved_req->issuer->simcall;
2256           //XBT_DEBUG("Req->call %u", req->call);
2257
2258           /* Debug information */
2259           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2260             req_str = MC_request_to_string(req, value);
2261             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2262             xbt_free(req_str);
2263           }
2264
2265         }
2266
2267         SIMIX_simcall_pre(req, value);
2268         MC_wait_for_requests();
2269       }
2270
2271       depth++;
2272
2273       /* Update statistics */
2274       mc_stats->visited_pairs++;
2275       mc_stats->executed_transitions++;
2276     }
2277   }
2278
2279   XBT_DEBUG("**** End Replay ****");
2280
2281   if(initial_state_liveness->raw_mem_set)
2282     MC_SET_RAW_MEM;
2283   else
2284     MC_UNSET_RAW_MEM;
2285
2286 }
2287
2288 /**
2289  * \brief Dumps the contents of a model-checker's stack and shows the actual
2290  *        execution trace
2291  * \param stack The stack to dump
2292  */
2293 void MC_dump_stack_safety(xbt_fifo_t stack)
2294 {
2295
2296   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2297
2298   MC_show_stack_safety(stack);
2299
2300   if(!_sg_mc_checkpoint){
2301
2302     mc_state_t state;
2303
2304     MC_SET_RAW_MEM;
2305     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
2306       MC_state_delete(state);
2307     MC_UNSET_RAW_MEM;
2308
2309   }
2310
2311   if(raw_mem_set)
2312     MC_SET_RAW_MEM;
2313   else
2314     MC_UNSET_RAW_MEM;
2315
2316 }
2317
2318
2319 void MC_show_stack_safety(xbt_fifo_t stack)
2320 {
2321
2322   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2323
2324   MC_SET_RAW_MEM;
2325
2326   int value;
2327   mc_state_t state;
2328   xbt_fifo_item_t item;
2329   smx_simcall_t req;
2330   char *req_str = NULL;
2331
2332   for (item = xbt_fifo_get_last_item(stack);
2333        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
2334         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2335     req = MC_state_get_executed_request(state, &value);
2336     if(req){
2337       req_str = MC_request_to_string(req, value);
2338       XBT_INFO("%s", req_str);
2339       xbt_free(req_str);
2340     }
2341   }
2342
2343   if(!raw_mem_set)
2344     MC_UNSET_RAW_MEM;
2345 }
2346
2347 void MC_show_deadlock(smx_simcall_t req)
2348 {
2349   /*char *req_str = NULL;*/
2350   XBT_INFO("**************************");
2351   XBT_INFO("*** DEAD-LOCK DETECTED ***");
2352   XBT_INFO("**************************");
2353   XBT_INFO("Locked request:");
2354   /*req_str = MC_request_to_string(req);
2355     XBT_INFO("%s", req_str);
2356     xbt_free(req_str);*/
2357   XBT_INFO("Counter-example execution trace:");
2358   MC_dump_stack_safety(mc_stack_safety);
2359   MC_print_statistics(mc_stats);
2360 }
2361
2362
2363 void MC_show_stack_liveness(xbt_fifo_t stack){
2364   int value;
2365   mc_pair_t pair;
2366   xbt_fifo_item_t item;
2367   smx_simcall_t req;
2368   char *req_str = NULL;
2369
2370   for (item = xbt_fifo_get_last_item(stack);
2371        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
2372         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2373     req = MC_state_get_executed_request(pair->graph_state, &value);
2374     if(req){
2375       if(pair->requests>0){
2376         req_str = MC_request_to_string(req, value);
2377         XBT_INFO("%s", req_str);
2378         xbt_free(req_str);
2379       }else{
2380         XBT_INFO("End of system requests but evolution in Büchi automaton");
2381       }
2382     }
2383   }
2384 }
2385
2386 void MC_dump_stack_liveness(xbt_fifo_t stack){
2387
2388   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2389
2390   mc_pair_t pair;
2391
2392   MC_SET_RAW_MEM;
2393   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
2394     MC_pair_delete(pair);
2395   MC_UNSET_RAW_MEM;
2396
2397   if(raw_mem_set)
2398     MC_SET_RAW_MEM;
2399
2400 }
2401
2402
2403 void MC_print_statistics(mc_stats_t stats)
2404 {
2405   if(stats->expanded_pairs == 0){
2406     XBT_INFO("Expanded states = %lu", stats->expanded_states);
2407     XBT_INFO("Visited states = %lu", stats->visited_states);
2408   }else{
2409     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
2410     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
2411   }
2412   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
2413   MC_SET_RAW_MEM;
2414   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
2415     fprintf(dot_output, "}\n");
2416     fclose(dot_output);
2417   }
2418   MC_UNSET_RAW_MEM;
2419 }
2420
2421 void MC_assert(int prop)
2422 {
2423   if (MC_is_active() && !prop){
2424     XBT_INFO("**************************");
2425     XBT_INFO("*** PROPERTY NOT VALID ***");
2426     XBT_INFO("**************************");
2427     XBT_INFO("Counter-example execution trace:");
2428     MC_dump_stack_safety(mc_stack_safety);
2429     MC_print_statistics(mc_stats);
2430     xbt_abort();
2431   }
2432 }
2433
2434 void MC_cut(void){
2435   user_max_depth_reached = 1;
2436 }
2437
2438 void MC_process_clock_add(smx_process_t process, double amount)
2439 {
2440   mc_time[process->pid] += amount;
2441 }
2442
2443 double MC_process_clock_get(smx_process_t process)
2444 {
2445   if(mc_time){
2446     if(process != NULL)
2447       return mc_time[process->pid];
2448     else
2449       return -1;
2450   }else{
2451     return 0;
2452   }
2453 }
2454
2455 void MC_automaton_load(const char *file){
2456
2457   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2458
2459   MC_SET_RAW_MEM;
2460
2461   if (_mc_property_automaton == NULL)
2462     _mc_property_automaton = xbt_automaton_new();
2463
2464   xbt_automaton_load(_mc_property_automaton,file);
2465
2466   MC_UNSET_RAW_MEM;
2467
2468   if(raw_mem_set)
2469     MC_SET_RAW_MEM;
2470
2471 }
2472
2473 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
2474
2475   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2476
2477   MC_SET_RAW_MEM;
2478
2479   if (_mc_property_automaton == NULL)
2480     _mc_property_automaton = xbt_automaton_new();
2481
2482   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
2483
2484   MC_UNSET_RAW_MEM;
2485
2486   if(raw_mem_set)
2487     MC_SET_RAW_MEM;
2488
2489 }
2490
2491
2492