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 static 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() {
 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   mc_object_info_t result = info;
 538   const char *elf_file = info->file_name;
 539
 540   xbt_dict_t location_list = MC_dwarf_get_location_list(elf_file);
 541
 542   char *command = bprintf("LANG=C objdump -Wi %s", elf_file);
 543
 544   FILE *fp = popen(command, "r");
 545
 546   if(fp == NULL)
 547     perror("popen for objdump failed");
 548
 549   xbt_dict_t *local_variables = &result->local_variables;
 550   xbt_dynar_t *global_variables = &result->global_variables;
 551   xbt_dict_t *types = &result->types;
 552
 553   char *line = NULL, *origin, *abstract_origin, *current_frame = NULL,
 554     *subprogram_name = NULL, *subprogram_start = NULL, *subprogram_end = NULL,
 555     *node_type = NULL, *location_type = NULL, *variable_name = NULL,
 556     *loc_expr = NULL, *name = NULL, *end =NULL, *type_origin = NULL, *global_address = NULL,
 557     *parent_value = NULL;
 558
 559   ssize_t read =0;
 560   size_t n = 0;
 561   int global_variable = 0, parent = 0, new_frame = 0, new_variable = 1, size = 0,
 562     is_pointer = 0, struct_decl = 0, member_end = 0,
 563     enumeration_size = 0, subrange = 0, union_decl = 0, offset = 0, index = 0;
 564
 565   xbt_dynar_t split = NULL, split2 = NULL;
 566
 567   xbt_dict_t variables_origin = xbt_dict_new_homogeneous(xbt_free);
 568   xbt_dict_t subprograms_origin = xbt_dict_new_homogeneous(xbt_free);
 569
 570   dw_frame_t variable_frame, subroutine_frame = NULL;
 571
 572   e_dw_type_type type_type = -1;
 573
 574   read = xbt_getline(&line, &n, fp);
 575
 576   while (read != -1) {
 577
 578     /* Wipeout the new line character */
 579     line[read - 1] = '\0';
 580
 581     if(n == 0 || strlen(line) == 0){
 582       read = xbt_getline(&line, &n, fp);
 583       continue;
 584     }
 585
 586     xbt_str_ltrim(line, NULL);
 587     xbt_str_strip_spaces(line);
 588
 589     if(line[0] != '<'){
 590       read = xbt_getline(&line, &n, fp);
 591       continue;
 592     }
 593
 594     xbt_dynar_free(&split);
 595     split = xbt_str_split(line, " ");
 596
 597     /* Get node type */
 598     node_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 599
 600     if(strcmp(node_type, "(DW_TAG_subprogram)") == 0){ /* New frame */
 601       /* We build/complete a dw_frame_t object
 602        * and append it if necessary to the local_variables dictionnary */
 603
 604       dw_frame_t frame = NULL;
 605
 606       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 607       subprogram_start = xbt_strdup(strtok(NULL, "<"));
 608       xbt_str_rtrim(subprogram_start, ">:");
 609
 610       read = xbt_getline(&line, &n, fp);
 611
 612       while(read != -1){
 613
 614         /* Wipeout the new line character */
 615         line[read - 1] = '\0';
 616
 617         if(n == 0 || strlen(line) == 0){
 618           read = xbt_getline(&line, &n, fp);
 619           continue;
 620         }
 621
 622         xbt_dynar_free(&split);
 623         xbt_str_rtrim(line, NULL);
 624         xbt_str_strip_spaces(line);
 625         split = xbt_str_split(line, " ");
 626
 627         node_type = xbt_dynar_get_as(split, 1, char *);
 628
 629         if(strncmp(node_type, "DW_AT_", 6) != 0)
 630           break;
 631
 632         if(strcmp(node_type, "DW_AT_sibling") == 0){
 633
 634           subprogram_end = xbt_strdup(xbt_dynar_get_as(split, 3, char*));
 635           xbt_str_ltrim(subprogram_end, "<0x");
 636           xbt_str_rtrim(subprogram_end, ">");
 637
 638         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){ /* Frame already in dict */
 639
 640           new_frame = 0;
 641           abstract_origin = xbt_strdup(xbt_dynar_get_as(split, 2, char*));
 642           xbt_str_ltrim(abstract_origin, "<0x");
 643           xbt_str_rtrim(abstract_origin, ">");
 644           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, abstract_origin);
 645           frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
 646           xbt_free(abstract_origin);
 647
 648         }else if(strcmp(node_type, "DW_AT_name") == 0){
 649
 650           new_frame = 1;
 651           xbt_free(current_frame);
 652           frame = xbt_new0(s_dw_frame_t, 1);
 653           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 654           frame->variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
 655           frame->frame_base = xbt_new0(s_dw_location_t, 1);
 656           current_frame = strdup(frame->name);
 657
 658           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 659
 660         }else if(strcmp(node_type, "DW_AT_frame_base") == 0){
 661
 662           location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 663
 664           if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
 665
 666             frame->frame_base = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
 667
 668           }else{
 669
 670             xbt_str_strip_spaces(line);
 671             split2 = xbt_str_split(line, "(");
 672             xbt_dynar_remove_at(split2, 0, NULL);
 673             loc_expr = xbt_str_join(split2, " ");
 674             xbt_str_rtrim(loc_expr, ")");
 675             frame->frame_base = MC_dwarf_get_location(NULL, loc_expr);
 676             xbt_dynar_free(&split2);
 677             xbt_free(loc_expr);
 678
 679           }
 680
 681         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 682
 683           if(frame != NULL)
 684             frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 685
 686         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 687
 688           if(frame != NULL)
 689             frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 690
 691         }else if(strcmp(node_type, "DW_AT_MIPS_linkage_name:") == 0){
 692
 693           xbt_free(frame->name);
 694           xbt_free(current_frame);
 695           frame->name = strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 696           current_frame = strdup(frame->name);
 697           xbt_dict_set(subprograms_origin, subprogram_start, xbt_strdup(frame->name), NULL);
 698
 699         }
 700
 701         read = xbt_getline(&line, &n, fp);
 702
 703       }
 704
 705       if(new_frame == 1){
 706         frame->start = strtoul(subprogram_start, NULL, 16);
 707         if(subprogram_end != NULL)
 708           frame->end = strtoul(subprogram_end, NULL, 16);
 709         xbt_dict_set(*local_variables, frame->name, frame, NULL);
 710       }
 711
 712       xbt_free(subprogram_start);
 713       xbt_free(subprogram_end);
 714       subprogram_end = NULL;
 715
 716
 717     }else if(strcmp(node_type, "(DW_TAG_variable)") == 0){ /* New variable */
 718       /* We build a dw_variable_t object and append it either to
 719          the list of variables of the frame (local variable)
 720          or to the list of global variables (global variables). */
 721
 722       dw_variable_t var = NULL;
 723
 724       parent_value = strdup(xbt_dynar_get_as(split, 0, char *));
 725       parent_value = strtok(parent_value,"<");
 726       xbt_str_rtrim(parent_value, ">");
 727       parent = atoi(parent_value);
 728       xbt_free(parent_value);
 729
 730       if(parent == 1)
 731         global_variable = 1;
 732
 733       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 734       origin = xbt_strdup(strtok(NULL, "<"));
 735       xbt_str_rtrim(origin, ">:");
 736
 737       read = xbt_getline(&line, &n, fp);
 738
 739       while(read != -1){
 740
 741         /* Wipeout the new line character */
 742         line[read - 1] = '\0';
 743
 744         if(n == 0 || strlen(line) == 0){
 745           read = xbt_getline(&line, &n, fp);
 746           continue;
 747         }
 748
 749         xbt_dynar_free(&split);
 750         xbt_str_rtrim(line, NULL);
 751         xbt_str_strip_spaces(line);
 752         split = xbt_str_split(line, " ");
 753
 754         node_type = xbt_dynar_get_as(split, 1, char *);
 755
 756         if(strncmp(node_type, "DW_AT_", 6) != 0)
 757           break;
 758
 759         if(strcmp(node_type, "DW_AT_name") == 0){
 760
 761           var = xbt_new0(s_dw_variable_t, 1);
 762           var->name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 763           xbt_dict_set(variables_origin, origin, xbt_strdup(var->name), NULL);
 764
 765         }else if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 766
 767           new_variable = 0;
 768
 769           abstract_origin = xbt_dynar_get_as(split, 2, char *);
 770           xbt_str_ltrim(abstract_origin, "<0x");
 771           xbt_str_rtrim(abstract_origin, ">");
 772
 773           variable_name = (char *)xbt_dict_get_or_null(variables_origin, abstract_origin);
 774           variable_frame = MC_dwarf_get_frame_by_offset(*local_variables, strtoul(abstract_origin, NULL, 16));
 775           var = MC_dwarf_get_variable_by_name(variable_frame, variable_name);
 776
 777         }else if(strcmp(node_type, "DW_AT_location") == 0){
 778
 779           if(var != NULL){
 780
 781             if(!global_variable){
 782
 783               location_type = xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *);
 784
 785               if(strcmp(location_type, "list)") == 0){ /* Search location in location list */
 786                 var->address.location = MC_dwarf_get_location(location_list, xbt_dynar_get_as(split, 3, char *));
 787               }else{
 788                 xbt_str_strip_spaces(line);
 789                 split2 = xbt_str_split(line, "(");
 790                 xbt_dynar_remove_at(split2, 0, NULL);
 791                 loc_expr = xbt_str_join(split2, " ");
 792                 xbt_str_rtrim(loc_expr, ")");
 793                 if(strncmp("DW_OP_addr", loc_expr, 10) == 0){
 794                   global_variable = 1;
 795                   xbt_dynar_free(&split2);
 796                   split2 = xbt_str_split(loc_expr, " ");
 797                   if(strcmp(elf_file, xbt_binary_name) != 0)
 798                     var->address.address = (char *) info->start_text + (long)((void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16));
 799                   else
 800                     // Why is it different ?
 801                     var->address.address = (void *)strtoul(xbt_dynar_get_as(split2, xbt_dynar_length(split2) - 1, char*), NULL, 16);
 802                 }else{
 803                   var->address.location = MC_dwarf_get_location(NULL, loc_expr);
 804                 }
 805                 xbt_dynar_free(&split2);
 806                 xbt_free(loc_expr);
 807               }
 808             }else{
 809               global_address = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *));
 810               xbt_str_rtrim(global_address, ")");
 811               if(strcmp(elf_file, xbt_binary_name) != 0)
 812                 var->address.address = (char *) info->start_text + (long)((void *)strtoul(global_address, NULL, 16));
 813               else
 814                 // Why is it different ?
 815                 var->address.address = (void *)strtoul(global_address, NULL, 16);
 816               xbt_free(global_address);
 817               global_address = NULL;
 818             }
 819
 820           }
 821
 822         }else if(strcmp(node_type, "DW_AT_type") == 0){
 823
 824           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
 825           xbt_str_ltrim(type_origin, "<0x");
 826           xbt_str_rtrim(type_origin, ">");
 827
 828         }else if(strcmp(node_type, "DW_AT_declaration") == 0){
 829
 830           new_variable = 0;
 831           if(new_variable){
 832             dw_variable_free(var);
 833             var = NULL;
 834           }
 835
 836         }else if(strcmp(node_type, "DW_AT_artificial") == 0){
 837
 838           new_variable = 0;
 839           if(new_variable){
 840             dw_variable_free(var);
 841             var = NULL;
 842           }
 843
 844         }
 845
 846         read = xbt_getline(&line, &n, fp);
 847
 848       }
 849
 850       if(new_variable == 1){
 851
 852         if(!global_variable){
 853           variable_frame = xbt_dict_get_or_null(*local_variables, current_frame);
 854           var->type_origin = strdup(type_origin);
 855           var->global = 0;
 856           index = MC_dwarf_get_variable_index(variable_frame->variables, var->name, NULL);
 857           if(index != -1)
 858             xbt_dynar_insert_at(variable_frame->variables, index, &var);
 859         }else{
 860           var->type_origin = strdup(type_origin);
 861           var->global = 1;
 862           index = MC_dwarf_get_variable_index(*global_variables, var->name, var->address.address);
 863           if(index != -1)
 864             xbt_dynar_insert_at(*global_variables, index, &var);
 865         }
 866
 867          xbt_free(type_origin);
 868          type_origin = NULL;
 869       }
 870
 871       global_variable = 0;
 872       new_variable = 1;
 873
 874     }else if(strcmp(node_type, "(DW_TAG_inlined_subroutine)") == 0){
 875       /* Update the information on the frame (we should duplicate it instead). */
 876
 877       read = xbt_getline(&line, &n, fp);
 878
 879       while(read != -1){
 880
 881         /* Wipeout the new line character */
 882         line[read - 1] = '\0';
 883
 884         if(n == 0 || strlen(line) == 0){
 885           read = xbt_getline(&line, &n, fp);
 886           continue;
 887         }
 888
 889         xbt_dynar_free(&split);
 890         xbt_str_rtrim(line, NULL);
 891         xbt_str_strip_spaces(line);
 892         split = xbt_str_split(line, " ");
 893
 894         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
 895           break;
 896
 897         node_type = xbt_dynar_get_as(split, 1, char *);
 898
 899         if(strcmp(node_type, "DW_AT_abstract_origin:") == 0){
 900
 901           origin = xbt_dynar_get_as(split, 2, char *);
 902           xbt_str_ltrim(origin, "<0x");
 903           xbt_str_rtrim(origin, ">");
 904
 905           subprogram_name = (char *)xbt_dict_get_or_null(subprograms_origin, origin);
 906           subroutine_frame = xbt_dict_get_or_null(*local_variables, subprogram_name);
 907
 908         }else if(strcmp(node_type, "DW_AT_low_pc") == 0){
 909
 910           subroutine_frame->low_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 911
 912         }else if(strcmp(node_type, "DW_AT_high_pc") == 0){
 913
 914           subroutine_frame->high_pc = (void *)strtoul(xbt_dynar_get_as(split, 3, char *), NULL, 16);
 915         }
 916
 917         read = xbt_getline(&line, &n, fp);
 918
 919       }
 920
 921     }else if(strcmp(node_type, "(DW_TAG_base_type)") == 0
 922              || strcmp(node_type, "(DW_TAG_enumeration_type)") == 0
 923              || strcmp(node_type, "(DW_TAG_enumerator)") == 0
 924              || strcmp(node_type, "(DW_TAG_typedef)") == 0
 925              || strcmp(node_type, "(DW_TAG_const_type)") == 0
 926              || strcmp(node_type, "(DW_TAG_subroutine_type)") == 0
 927              || strcmp(node_type, "(DW_TAG_volatile_type)") == 0
 928              || (is_pointer = !strcmp(node_type, "(DW_TAG_pointer_type)"))){
 929
 930       /* Create the and add it to the types dictionnary */
 931
 932       if(strcmp(node_type, "(DW_TAG_base_type)") == 0)
 933         type_type = e_dw_base_type;
 934       else if(strcmp(node_type, "(DW_TAG_enumeration_type)") == 0)
 935         type_type = e_dw_enumeration_type;
 936       else if(strcmp(node_type, "(DW_TAG_enumerator)") == 0)
 937         type_type = e_dw_enumerator;
 938       else if(strcmp(node_type, "(DW_TAG_typedef)") == 0)
 939         type_type = e_dw_typedef;
 940       else if(strcmp(node_type, "(DW_TAG_const_type)") == 0)
 941         type_type = e_dw_const_type;
 942       else if(strcmp(node_type, "(DW_TAG_pointer_type)") == 0)
 943         type_type = e_dw_pointer_type;
 944       else if(strcmp(node_type, "(DW_TAG_subroutine_type)") == 0)
 945         type_type = e_dw_subroutine_type;
 946       else if(strcmp(node_type, "(DW_TAG_volatile_type)") == 0)
 947         type_type = e_dw_volatile_type;
 948
 949       strtok(xbt_dynar_get_as(split, 0, char *), "<");
 950       origin = strdup(strtok(NULL, "<"));
 951       xbt_str_rtrim(origin, ">:");
 952
 953       read = xbt_getline(&line, &n, fp);
 954
 955       while(read != -1){
 956
 957          /* Wipeout the new line character */
 958         line[read - 1] = '\0';
 959
 960         if(n == 0 || strlen(line) == 0){
 961           read = xbt_getline(&line, &n, fp);
 962           continue;
 963         }
 964
 965         xbt_dynar_free(&split);
 966         xbt_str_rtrim(line, NULL);
 967         xbt_str_strip_spaces(line);
 968         split = xbt_str_split(line, " ");
 969
 970         if(strncmp(xbt_dynar_get_as(split, 1, char *), "DW_AT_", 6) != 0)
 971           break;
 972
 973         node_type = xbt_dynar_get_as(split, 1, char *);
 974
 975         if(strcmp(node_type, "DW_AT_byte_size") == 0){
 976           size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
 977           if(type_type == e_dw_enumeration_type)
 978             enumeration_size = size;
 979         }else if(strcmp(node_type, "DW_AT_name") == 0){
 980           end = xbt_str_join(split, " ");
 981           xbt_dynar_free(&split);
 982           split = xbt_str_split(end, "):");
 983           xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
 984           name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
 985         }else if(strcmp(node_type, "DW_AT_type") == 0){
 986           type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
 987           xbt_str_ltrim(type_origin, "<0x");
 988           xbt_str_rtrim(type_origin, ">");
 989         }
 990
 991         read = xbt_getline(&line, &n, fp);
 992       }
 993
 994       dw_type_t type = xbt_new0(s_dw_type_t, 1);
 995       type->type = type_type;
 996       if(name)
 997         type->name = xbt_strdup(name);
 998       else
 999         type->name = xbt_strdup("undefined");
1000       type->is_pointer_type = is_pointer;
1001       type->id = (void *)strtoul(origin, NULL, 16);
1002       if(type_origin)
1003         type->dw_type_id = xbt_strdup(type_origin);
1004       if(type_type == e_dw_enumerator) {
1005         type->element_count = enumeration_size;
1006         type->byte_size = size;
1007       }
1008       else {
1009         type->byte_size = size;
1010         // Not relevant:
1011         type->element_count = -1;
1012       }
1013       type->members = NULL;
1014
1015       xbt_dict_set(*types, origin, type, NULL);
1016
1017       xbt_free(name);
1018       name = NULL;
1019       xbt_free(type_origin);
1020       type_origin = NULL;
1021       xbt_free(end);
1022       end = NULL;
1023
1024       is_pointer = 0;
1025       size = 0;
1026       xbt_free(origin);
1027
1028     }else if(strcmp(node_type, "(DW_TAG_structure_type)") == 0 || strcmp(node_type, "(DW_TAG_union_type)") == 0){
1029
1030       if(strcmp(node_type, "(DW_TAG_structure_type)") == 0)
1031         struct_decl = 1;
1032       else
1033         union_decl = 1;
1034
1035       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1036       origin = strdup(strtok(NULL, "<"));
1037       xbt_str_rtrim(origin, ">:");
1038
1039       read = xbt_getline(&line, &n, fp);
1040
1041       dw_type_t type = NULL;
1042
1043       while(read != -1){
1044
1045         while(read != -1){
1046
1047           /* Wipeout the new line character */
1048           line[read - 1] = '\0';
1049
1050           if(n == 0 || strlen(line) == 0){
1051             read = xbt_getline(&line, &n, fp);
1052             continue;
1053           }
1054
1055           xbt_dynar_free(&split);
1056           xbt_str_rtrim(line, NULL);
1057           xbt_str_strip_spaces(line);
1058           split = xbt_str_split(line, " ");
1059
1060           node_type = xbt_dynar_get_as(split, 1, char *);
1061
1062           if(strncmp(node_type, "DW_AT_", 6) != 0){
1063             member_end = 1;
1064             break;
1065           }
1066
1067           if(strcmp(node_type, "DW_AT_byte_size") == 0){
1068             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1069           }else if(strcmp(node_type, "DW_AT_name") == 0){
1070             xbt_free(end);
1071             end = xbt_str_join(split, " ");
1072             xbt_dynar_free(&split);
1073             split = xbt_str_split(end, "):");
1074             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1075             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1076           }else if(strcmp(node_type, "DW_AT_type") == 0){
1077             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1078             xbt_str_ltrim(type_origin, "<0x");
1079             xbt_str_rtrim(type_origin, ">");
1080           }else if(strcmp(node_type, "DW_AT_data_member_location:") == 0){
1081             xbt_free(end);
1082             end = xbt_str_join(split, " ");
1083             xbt_dynar_free(&split);
1084             split = xbt_str_split(end, "DW_OP_plus_uconst:");
1085             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), NULL);
1086             xbt_str_rtrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), ")");
1087             offset = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1088           }
1089
1090           read = xbt_getline(&line, &n, fp);
1091
1092         }
1093
1094         if(member_end && type){
1095           member_end = 0;
1096
1097           // Why are we not simply referencing, the DW_AT_type?
1098           dw_type_t member_type = xbt_new0(s_dw_type_t, 1);
1099           member_type->name = xbt_strdup(name);
1100           member_type->byte_size = size;
1101           member_type->element_count = -1;
1102           member_type->is_pointer_type = is_pointer;
1103           member_type->id = (void *)strtoul(origin, NULL, 16);
1104           member_type->offset = offset;
1105           if(type_origin)
1106             member_type->dw_type_id = xbt_strdup(type_origin);
1107
1108           xbt_dynar_push(type->members, &member_type);
1109
1110           xbt_free(name);
1111           name = NULL;
1112           xbt_free(end);
1113           end = NULL;
1114           xbt_free(type_origin);
1115           type_origin = NULL;
1116           size = 0;
1117           offset = 0;
1118
1119           xbt_free(origin);
1120           origin = NULL;
1121           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1122           origin = strdup(strtok(NULL, "<"));
1123           xbt_str_rtrim(origin, ">:");
1124
1125         }
1126
1127         if(struct_decl || union_decl){
1128           type = xbt_new0(s_dw_type_t, 1);
1129           if(struct_decl)
1130             type->type = e_dw_structure_type;
1131           else
1132             type->type = e_dw_union_type;
1133           type->name = xbt_strdup(name);
1134           type->byte_size = size;
1135           type->element_count = -1;
1136           type->is_pointer_type = is_pointer;
1137           type->id = (void *)strtoul(origin, NULL, 16);
1138           if(type_origin)
1139             type->dw_type_id = xbt_strdup(type_origin);
1140           type->members = xbt_dynar_new(sizeof(dw_type_t), dw_type_free_voidp);
1141
1142           xbt_dict_set(*types, origin, type, NULL);
1143
1144           xbt_free(name);
1145           name = NULL;
1146           xbt_free(end);
1147           end = NULL;
1148           xbt_free(type_origin);
1149           type_origin = NULL;
1150           size = 0;
1151           struct_decl = 0;
1152           union_decl = 0;
1153
1154         }
1155
1156         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_member)") != 0)
1157           break;
1158
1159         read = xbt_getline(&line, &n, fp);
1160
1161       }
1162
1163       xbt_free(origin);
1164       origin = NULL;
1165
1166     }else if(strcmp(node_type, "(DW_TAG_array_type)") == 0){
1167
1168       strtok(xbt_dynar_get_as(split, 0, char *), "<");
1169       origin = strdup(strtok(NULL, "<"));
1170       xbt_str_rtrim(origin, ">:");
1171
1172       read = xbt_getline(&line, &n, fp);
1173
1174       dw_type_t type = NULL;
1175
1176       // Read DW_TAG_subrange_type children:
1177       while(read != -1){
1178
1179         // Read attributes of the DW_TAG_subrange_type:
1180         while(read != -1){
1181
1182           /* Wipeout the new line character */
1183           line[read - 1] = '\0';
1184
1185           if(n == 0 || strlen(line) == 0){
1186             read = xbt_getline(&line, &n, fp);
1187             continue;
1188           }
1189
1190           xbt_dynar_free(&split);
1191           xbt_str_rtrim(line, NULL);
1192           xbt_str_strip_spaces(line);
1193           split = xbt_str_split(line, " ");
1194
1195           node_type = xbt_dynar_get_as(split, 1, char *);
1196
1197           if(strncmp(node_type, "DW_AT_", 6) != 0)
1198             break;
1199
1200           if(strcmp(node_type, "DW_AT_upper_bound") == 0){
1201             size = strtol(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL, 10);
1202           }else if(strcmp(node_type, "DW_AT_name") == 0){
1203             end = xbt_str_join(split, " ");
1204             xbt_dynar_free(&split);
1205             split = xbt_str_split(end, "):");
1206             xbt_str_ltrim(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*), NULL);
1207             name = xbt_strdup(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char*));
1208           }else if(strcmp(node_type, "DW_AT_type") == 0){
1209             type_origin = xbt_strdup(xbt_dynar_get_as(split, 3, char *));
1210             xbt_str_ltrim(type_origin, "<0x");
1211             xbt_str_rtrim(type_origin, ">");
1212           }
1213
1214           read = xbt_getline(&line, &n, fp);
1215
1216         }
1217
1218         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") == 0){
1219           subrange = 1;
1220         }
1221
1222         if(subrange && type){
1223           type->element_count = size;
1224
1225           xbt_free(name);
1226           name = NULL;
1227           xbt_free(end);
1228           end = NULL;
1229           xbt_free(type_origin);
1230           type_origin = NULL;
1231           size = 0;
1232
1233           xbt_free(origin);
1234           origin = NULL;
1235           strtok(xbt_dynar_get_as(split, 0, char *), "<");
1236           origin = strdup(strtok(NULL, "<"));
1237           xbt_str_rtrim(origin, ">:");
1238
1239         }else {
1240
1241           type = xbt_new0(s_dw_type_t, 1);
1242           type->type = e_dw_array_type;
1243           type->name = xbt_strdup(name);
1244           type->is_pointer_type = is_pointer;
1245           type->id = (void *)strtoul(origin, NULL, 16);
1246           if(type_origin)
1247             type->dw_type_id = xbt_strdup(type_origin);
1248           type->members = NULL;
1249
1250           // Filled in a post processing step:
1251           type-> byte_size = 0;
1252
1253           xbt_dict_set(*types, origin, type, NULL);
1254
1255           xbt_free(name);
1256           name = NULL;
1257           xbt_free(end);
1258           end = NULL;
1259           xbt_free(type_origin);
1260           type_origin = NULL;
1261           size = 0;
1262         }
1263
1264         if(strcmp(xbt_dynar_get_as(split, xbt_dynar_length(split) - 1, char *), "(DW_TAG_subrange_type)") != 0)
1265           break;
1266
1267         read = xbt_getline(&line, &n, fp);
1268
1269       }
1270
1271       xbt_free(origin);
1272       origin = NULL;
1273
1274     }else{
1275
1276       read = xbt_getline(&line, &n, fp);
1277
1278     }
1279
1280   }
1281
1282   xbt_dynar_free(&split);
1283   xbt_dict_free(&variables_origin);
1284   xbt_dict_free(&subprograms_origin);
1285   xbt_free(line);
1286   xbt_free(command);
1287   xbt_dict_free(&location_list);
1288
1289   pclose(fp);
1290
1291   MC_post_process_types(info);
1292 }
1293
1294 static void MC_post_process_types(mc_object_info_t info) {
1295   xbt_dict_cursor_t cursor;
1296   char *origin;
1297   dw_type_t type;
1298   xbt_dict_foreach(info->types, cursor, origin, type){
1299     if(type->type==e_dw_array_type) {
1300       xbt_assert(type->dw_type_id, "No base type for array %s %s", type->id, type->name);
1301       dw_type_t subtype = xbt_dict_get_or_null(info->types, type->dw_type_id);
1302           xbt_assert(subtype, "Unkown base type for array %s %s", type->id, type->name);
1303       type->byte_size = type->element_count*subtype->byte_size;
1304     }
1305   }
1306 }
1307
1308 /*******************************  Ignore mechanism *******************************/
1309 /*********************************************************************************/
1310
1311 xbt_dynar_t mc_checkpoint_ignore;
1312
1313 typedef struct s_mc_stack_ignore_variable{
1314   char *var_name;
1315   char *frame;
1316 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
1317
1318 typedef struct s_mc_data_bss_ignore_variable{
1319   char *name;
1320 }s_mc_data_bss_ignore_variable_t, *mc_data_bss_ignore_variable_t;
1321
1322 /**************************** Free functions ******************************/
1323
1324 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
1325   xbt_free(v->var_name);
1326   xbt_free(v->frame);
1327   xbt_free(v);
1328 }
1329
1330 static void stack_ignore_variable_free_voidp(void *v){
1331   stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
1332 }
1333
1334 void heap_ignore_region_free(mc_heap_ignore_region_t r){
1335   xbt_free(r);
1336 }
1337
1338 void heap_ignore_region_free_voidp(void *r){
1339   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
1340 }
1341
1342 static void data_bss_ignore_variable_free(mc_data_bss_ignore_variable_t v){
1343   xbt_free(v->name);
1344   xbt_free(v);
1345 }
1346
1347 static void data_bss_ignore_variable_free_voidp(void *v){
1348   data_bss_ignore_variable_free((mc_data_bss_ignore_variable_t) * (void **) v);
1349 }
1350
1351 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
1352   xbt_free(r);
1353 }
1354
1355 static void checkpoint_ignore_region_free_voidp(void *r){
1356   checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
1357 }
1358
1359 /***********************************************************************/
1360
1361 void MC_ignore_heap(void *address, size_t size){
1362
1363   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1364
1365   MC_SET_RAW_MEM;
1366
1367   mc_heap_ignore_region_t region = NULL;
1368   region = xbt_new0(s_mc_heap_ignore_region_t, 1);
1369   region->address = address;
1370   region->size = size;
1371
1372   region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1373
1374   if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
1375     region->fragment = -1;
1376     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
1377   }else{
1378     region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
1379     ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
1380   }
1381
1382   if(mc_heap_comparison_ignore == NULL){
1383     mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
1384     xbt_dynar_push(mc_heap_comparison_ignore, &region);
1385     if(!raw_mem_set)
1386       MC_UNSET_RAW_MEM;
1387     return;
1388   }
1389
1390   unsigned int cursor = 0;
1391   mc_heap_ignore_region_t current_region = NULL;
1392   int start = 0;
1393   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1394
1395   while(start <= end){
1396     cursor = (start + end) / 2;
1397     current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1398     if(current_region->address == address){
1399       heap_ignore_region_free(region);
1400       if(!raw_mem_set)
1401         MC_UNSET_RAW_MEM;
1402       return;
1403     }else if(current_region->address < address){
1404       start = cursor + 1;
1405     }else{
1406       end = cursor - 1;
1407     }
1408   }
1409
1410   if(current_region->address < address)
1411     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, &region);
1412   else
1413     xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, &region);
1414
1415   if(!raw_mem_set)
1416     MC_UNSET_RAW_MEM;
1417 }
1418
1419 void MC_remove_ignore_heap(void *address, size_t size){
1420
1421   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1422
1423   MC_SET_RAW_MEM;
1424
1425   unsigned int cursor = 0;
1426   int start = 0;
1427   int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
1428   mc_heap_ignore_region_t region;
1429   int ignore_found = 0;
1430
1431   while(start <= end){
1432     cursor = (start + end) / 2;
1433     region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
1434     if(region->address == address){
1435       ignore_found = 1;
1436       break;
1437     }else if(region->address < address){
1438       start = cursor + 1;
1439     }else{
1440       if((char * )region->address <= ((char *)address + size)){
1441         ignore_found = 1;
1442         break;
1443       }else{
1444         end = cursor - 1;
1445       }
1446     }
1447   }
1448
1449   if(ignore_found == 1){
1450     xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
1451     MC_remove_ignore_heap(address, size);
1452   }
1453
1454   if(!raw_mem_set)
1455     MC_UNSET_RAW_MEM;
1456
1457 }
1458
1459 void MC_ignore_global_variable(const char *name){
1460
1461   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1462
1463   MC_SET_RAW_MEM;
1464
1465   if(mc_libsimgrid_info){
1466
1467     unsigned int cursor = 0;
1468     dw_variable_t current_var;
1469     int start = 0;
1470     int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
1471
1472     while(start <= end){
1473       cursor = (start + end) /2;
1474       current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
1475       if(strcmp(current_var->name, name) == 0){
1476         xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
1477         start = 0;
1478         end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
1479       }else if(strcmp(current_var->name, name) < 0){
1480         start = cursor + 1;
1481       }else{
1482         end = cursor - 1;
1483       }
1484     }
1485
1486   }else{
1487
1488     if(mc_data_bss_comparison_ignore == NULL)
1489       mc_data_bss_comparison_ignore = xbt_dynar_new(sizeof(mc_data_bss_ignore_variable_t), data_bss_ignore_variable_free_voidp);
1490
1491     mc_data_bss_ignore_variable_t var = NULL;
1492     var = xbt_new0(s_mc_data_bss_ignore_variable_t, 1);
1493     var->name = strdup(name);
1494
1495     if(xbt_dynar_is_empty(mc_data_bss_comparison_ignore)){
1496
1497       xbt_dynar_insert_at(mc_data_bss_comparison_ignore, 0, &var);
1498
1499     }else{
1500
1501       unsigned int cursor = 0;
1502       int start = 0;
1503       int end = xbt_dynar_length(mc_data_bss_comparison_ignore) - 1;
1504       mc_data_bss_ignore_variable_t current_var = NULL;
1505
1506       while(start <= end){
1507         cursor = (start + end) / 2;
1508         current_var = (mc_data_bss_ignore_variable_t)xbt_dynar_get_as(mc_data_bss_comparison_ignore, cursor, mc_data_bss_ignore_variable_t);
1509         if(strcmp(current_var->name, name) == 0){
1510           data_bss_ignore_variable_free(var);
1511           if(!raw_mem_set)
1512             MC_UNSET_RAW_MEM;
1513           return;
1514         }else if(strcmp(current_var->name, name) < 0){
1515           start = cursor + 1;
1516         }else{
1517           end = cursor - 1;
1518         }
1519       }
1520
1521       if(strcmp(current_var->name, name) < 0)
1522         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor + 1, &var);
1523       else
1524         xbt_dynar_insert_at(mc_data_bss_comparison_ignore, cursor, &var);
1525
1526     }
1527   }
1528
1529   if(!raw_mem_set)
1530     MC_UNSET_RAW_MEM;
1531 }
1532
1533 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
1534
1535   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1536
1537   MC_SET_RAW_MEM;
1538
1539   if(mc_libsimgrid_info){
1540     unsigned int cursor = 0;
1541     dw_variable_t current_var;
1542     int start, end;
1543     if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
1544       xbt_dict_cursor_t dict_cursor;
1545       char *current_frame_name;
1546       dw_frame_t frame;
1547       xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
1548         start = 0;
1549         end = xbt_dynar_length(frame->variables) - 1;
1550         while(start <= end){
1551           cursor = (start + end) / 2;
1552           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1553           if(strcmp(current_var->name, var_name) == 0){
1554             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1555             start = 0;
1556             end = xbt_dynar_length(frame->variables) - 1;
1557           }else if(strcmp(current_var->name, var_name) < 0){
1558             start = cursor + 1;
1559           }else{
1560             end = cursor - 1;
1561           }
1562         }
1563       }
1564        xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
1565         start = 0;
1566         end = xbt_dynar_length(frame->variables) - 1;
1567         while(start <= end){
1568           cursor = (start + end) / 2;
1569           current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
1570           if(strcmp(current_var->name, var_name) == 0){
1571             xbt_dynar_remove_at(frame->variables, cursor, NULL);
1572             start = 0;
1573             end = xbt_dynar_length(frame->variables) - 1;
1574           }else if(strcmp(current_var->name, var_name) < 0){
1575             start = cursor + 1;
1576           }else{
1577             end = cursor - 1;
1578           }
1579         }
1580       }
1581     }else{
1582       xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
1583                                       mc_libsimgrid_info->local_variables, frame_name))->variables;
1584       start = 0;
1585       end = xbt_dynar_length(variables_list) - 1;
1586       while(start <= end){
1587         cursor = (start + end) / 2;
1588         current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
1589         if(strcmp(current_var->name, var_name) == 0){
1590           xbt_dynar_remove_at(variables_list, cursor, NULL);
1591           start = 0;
1592           end = xbt_dynar_length(variables_list) - 1;
1593         }else if(strcmp(current_var->name, var_name) < 0){
1594           start = cursor + 1;
1595         }else{
1596           end = cursor - 1;
1597         }
1598       }
1599     }
1600   }else{
1601
1602     if(mc_stack_comparison_ignore == NULL)
1603       mc_stack_comparison_ignore = xbt_dynar_new(sizeof(mc_stack_ignore_variable_t), stack_ignore_variable_free_voidp);
1604
1605     mc_stack_ignore_variable_t var = NULL;
1606     var = xbt_new0(s_mc_stack_ignore_variable_t, 1);
1607     var->var_name = strdup(var_name);
1608     var->frame = strdup(frame_name);
1609
1610     if(xbt_dynar_is_empty(mc_stack_comparison_ignore)){
1611
1612       xbt_dynar_insert_at(mc_stack_comparison_ignore, 0, &var);
1613
1614     }else{
1615
1616       unsigned int cursor = 0;
1617       int start = 0;
1618       int end = xbt_dynar_length(mc_stack_comparison_ignore) - 1;
1619       mc_stack_ignore_variable_t current_var = NULL;
1620
1621       while(start <= end){
1622         cursor = (start + end) / 2;
1623         current_var = (mc_stack_ignore_variable_t)xbt_dynar_get_as(mc_stack_comparison_ignore, cursor, mc_stack_ignore_variable_t);
1624         if(strcmp(current_var->frame, frame_name) == 0){
1625           if(strcmp(current_var->var_name, var_name) == 0){
1626             stack_ignore_variable_free(var);
1627             if(!raw_mem_set)
1628               MC_UNSET_RAW_MEM;
1629             return;
1630           }else if(strcmp(current_var->var_name, var_name) < 0){
1631             start = cursor + 1;
1632           }else{
1633             end = cursor - 1;
1634           }
1635         }else if(strcmp(current_var->frame, frame_name) < 0){
1636           start = cursor + 1;
1637         }else{
1638           end = cursor - 1;
1639         }
1640       }
1641
1642       if(strcmp(current_var->frame, frame_name) == 0){
1643         if(strcmp(current_var->var_name, var_name) < 0){
1644           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1645         }else{
1646           xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1647         }
1648       }else if(strcmp(current_var->frame, frame_name) < 0){
1649         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor + 1, &var);
1650       }else{
1651         xbt_dynar_insert_at(mc_stack_comparison_ignore, cursor, &var);
1652       }
1653     }
1654   }
1655
1656   if(!raw_mem_set)
1657     MC_UNSET_RAW_MEM;
1658
1659 }
1660
1661 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
1662
1663   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1664
1665   MC_SET_RAW_MEM;
1666
1667   if(stacks_areas == NULL)
1668     stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
1669
1670   stack_region_t region = NULL;
1671   region = xbt_new0(s_stack_region_t, 1);
1672   region->address = stack;
1673   region->process_name = strdup(name);
1674   region->context = context;
1675   region->size = size;
1676   region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
1677   xbt_dynar_push(stacks_areas, &region);
1678
1679   if(!raw_mem_set)
1680     MC_UNSET_RAW_MEM;
1681 }
1682
1683 void MC_ignore(void *addr, size_t size){
1684
1685   int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
1686
1687   MC_SET_RAW_MEM;
1688
1689   if(mc_checkpoint_ignore == NULL)
1690     mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
1691
1692   mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
1693   region->addr = addr;
1694   region->size = size;
1695
1696   if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
1697     xbt_dynar_push(mc_checkpoint_ignore, &region);
1698   }else{
1699
1700     unsigned int cursor = 0;
1701     int start = 0;
1702     int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
1703     mc_checkpoint_ignore_region_t current_region = NULL;
1704
1705     while(start <= end){
1706       cursor = (start + end) / 2;
1707       current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
1708       if(current_region->addr == addr){
1709         if(current_region->size == size){
1710           checkpoint_ignore_region_free(region);
1711           if(!raw_mem_set)
1712             MC_UNSET_RAW_MEM;
1713           return;
1714         }else if(current_region->size < size){
1715           start = cursor + 1;
1716         }else{
1717           end = cursor - 1;
1718         }
1719       }else if(current_region->addr < addr){
1720           start = cursor + 1;
1721       }else{
1722         end = cursor - 1;
1723       }
1724     }
1725
1726      if(current_region->addr == addr){
1727        if(current_region->size < size){
1728         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
1729       }else{
1730         xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
1731       }
1732     }else if(current_region->addr < addr){
1733        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, &region);
1734     }else{
1735        xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, &region);
1736     }
1737   }
1738
1739   if(!raw_mem_set)
1740     MC_UNSET_RAW_MEM;
1741 }
1742
1743 /*******************************  Initialisation of MC *******************************/
1744 /*********************************************************************************/
1745
1746 static void MC_dump_ignored_local_variables(void){
1747
1748   if(mc_stack_comparison_ignore == NULL || xbt_dynar_is_empty(mc_stack_comparison_ignore))
1749     return;
1750
1751   unsigned int cursor = 0;
1752   mc_stack_ignore_variable_t current_var;
1753
1754   xbt_dynar_foreach(mc_stack_comparison_ignore, cursor, current_var){
1755     MC_ignore_local_variable(current_var->var_name, current_var->frame);
1756   }
1757
1758   xbt_dynar_free(&mc_stack_comparison_ignore);
1759   mc_stack_comparison_ignore = NULL;
1760
1761 }
1762
1763 static void MC_dump_ignored_global_variables(void){
1764
1765   if(mc_data_bss_comparison_ignore == NULL || xbt_dynar_is_empty(mc_data_bss_comparison_ignore))
1766     return;
1767
1768   unsigned int cursor = 0;
1769   mc_data_bss_ignore_variable_t current_var;
1770
1771   xbt_dynar_foreach(mc_data_bss_comparison_ignore, cursor, current_var){
1772     MC_ignore_global_variable(current_var->name);
1773   }
1774
1775   xbt_dynar_free(&mc_data_bss_comparison_ignore);
1776   mc_data_bss_comparison_ignore = NULL;
1777
1778 }
1779
1780 static void MC_init_debug_info();
1781 static void MC_init_debug_info() {
1782   XBT_INFO("Get debug information ...");
1783
1784   memory_map_t maps = MC_get_memory_map();
1785
1786   /* Get local variables for state equality detection */
1787   mc_binary_info = MC_find_object_info(maps, xbt_binary_name);
1788   mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path);
1789
1790   MC_free_memory_map(maps);
1791   XBT_INFO("Get debug information done !");
1792 }
1793
1794 void MC_init(){
1795
1796   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1797
1798   compare = 0;
1799
1800   /* Initialize the data structures that must be persistent across every
1801      iteration of the model-checker (in RAW memory) */
1802
1803   MC_SET_RAW_MEM;
1804
1805   MC_init_memory_map_info();
1806   MC_init_debug_info();
1807
1808   /* Remove variables ignored before getting list of variables */
1809   MC_dump_ignored_local_variables();
1810   MC_dump_ignored_global_variables();
1811
1812    /* Init parmap */
1813   parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
1814
1815   MC_UNSET_RAW_MEM;
1816
1817    /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
1818   MC_ignore_local_variable("e", "*");
1819   MC_ignore_local_variable("__ex_cleanup", "*");
1820   MC_ignore_local_variable("__ex_mctx_en", "*");
1821   MC_ignore_local_variable("__ex_mctx_me", "*");
1822   MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
1823   MC_ignore_local_variable("_log_ev", "*");
1824   MC_ignore_local_variable("_throw_ctx", "*");
1825   MC_ignore_local_variable("ctx", "*");
1826
1827   MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
1828   MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
1829
1830   /* Ignore local variable about time used for tracing */
1831   MC_ignore_local_variable("start_time", "*");
1832
1833   MC_ignore_global_variable("mc_comp_times");
1834   MC_ignore_global_variable("mc_snapshot_comparison_time");
1835   MC_ignore_global_variable("mc_time");
1836   MC_ignore_global_variable("smpi_current_rank");
1837   MC_ignore_global_variable("counter"); /* Static variable used for tracing */
1838   MC_ignore_global_variable("maestro_stack_start");
1839   MC_ignore_global_variable("maestro_stack_end");
1840
1841   MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
1842   MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
1843   MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
1844   MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
1845
1846   smx_process_t process;
1847   xbt_swag_foreach(process, simix_global->process_list){
1848     MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
1849   }
1850
1851   if(raw_mem_set)
1852     MC_SET_RAW_MEM;
1853
1854 }
1855
1856 static void MC_init_dot_output(){ /* FIXME : more colors */
1857
1858   colors[0] = "blue";
1859   colors[1] = "red";
1860   colors[2] = "green3";
1861   colors[3] = "goldenrod";
1862   colors[4] = "brown";
1863   colors[5] = "purple";
1864   colors[6] = "magenta";
1865   colors[7] = "turquoise4";
1866   colors[8] = "gray25";
1867   colors[9] = "forestgreen";
1868   colors[10] = "hotpink";
1869   colors[11] = "lightblue";
1870   colors[12] = "tan";
1871
1872   dot_output = fopen(_sg_mc_dot_output_file, "w");
1873
1874   if(dot_output == NULL){
1875     perror("Error open dot output file");
1876     xbt_abort();
1877   }
1878
1879   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");
1880
1881 }
1882
1883 /*******************************  Core of MC *******************************/
1884 /**************************************************************************/
1885
1886 void MC_do_the_modelcheck_for_real() {
1887
1888   MC_SET_RAW_MEM;
1889   mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
1890   MC_UNSET_RAW_MEM;
1891
1892   if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
1893     if (mc_reduce_kind==e_mc_reduce_unset)
1894       mc_reduce_kind=e_mc_reduce_dpor;
1895
1896     XBT_INFO("Check a safety property");
1897     MC_modelcheck_safety();
1898
1899   } else  {
1900
1901     if (mc_reduce_kind==e_mc_reduce_unset)
1902       mc_reduce_kind=e_mc_reduce_none;
1903
1904     XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1905     MC_automaton_load(_sg_mc_property_file);
1906     MC_modelcheck_liveness();
1907   }
1908 }
1909
1910 void MC_modelcheck_safety(void)
1911 {
1912   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1913
1914   /* Check if MC is already initialized */
1915   if (initial_state_safety)
1916     return;
1917
1918   mc_time = xbt_new0(double, simix_process_maxpid);
1919
1920   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1921   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1922
1923   /* Initialize the data structures that must be persistent across every
1924      iteration of the model-checker (in RAW memory) */
1925
1926   MC_SET_RAW_MEM;
1927
1928   /* Initialize statistics */
1929   mc_stats = xbt_new0(s_mc_stats_t, 1);
1930   mc_stats->state_size = 1;
1931
1932   /* Create exploration stack */
1933   mc_stack_safety = xbt_fifo_new();
1934
1935   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1936     MC_init_dot_output();
1937
1938   MC_UNSET_RAW_MEM;
1939
1940   if(_sg_mc_visited > 0){
1941     MC_init();
1942   }else{
1943     MC_SET_RAW_MEM;
1944     MC_init_memory_map_info();
1945     MC_init_debug_info();
1946     MC_UNSET_RAW_MEM;
1947   }
1948
1949   MC_dpor_init();
1950
1951   MC_SET_RAW_MEM;
1952   /* Save the initial state */
1953   initial_state_safety = xbt_new0(s_mc_global_t, 1);
1954   initial_state_safety->snapshot = MC_take_snapshot(0);
1955   MC_UNSET_RAW_MEM;
1956
1957   MC_dpor();
1958
1959   if(raw_mem_set)
1960     MC_SET_RAW_MEM;
1961
1962   xbt_abort();
1963   //MC_exit();
1964 }
1965
1966 void MC_modelcheck_liveness(){
1967
1968   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1969
1970   MC_init();
1971
1972   mc_time = xbt_new0(double, simix_process_maxpid);
1973
1974   /* mc_time refers to clock for each process -> ignore it for heap comparison */
1975   MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1976
1977   MC_SET_RAW_MEM;
1978
1979   /* Initialize statistics */
1980   mc_stats = xbt_new0(s_mc_stats_t, 1);
1981   mc_stats->state_size = 1;
1982
1983   /* Create exploration stack */
1984   mc_stack_liveness = xbt_fifo_new();
1985
1986   /* Create the initial state */
1987   initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1988
1989   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1990     MC_init_dot_output();
1991
1992   MC_UNSET_RAW_MEM;
1993
1994   MC_ddfs_init();
1995
1996   /* We're done */
1997   MC_print_statistics(mc_stats);
1998   xbt_free(mc_time);
1999
2000   if(raw_mem_set)
2001     MC_SET_RAW_MEM;
2002
2003 }
2004
2005
2006 void MC_exit(void)
2007 {
2008   xbt_free(mc_time);
2009   MC_memory_exit();
2010   //xbt_abort();
2011 }
2012
2013 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
2014
2015   return simcall->mc_value;
2016 }
2017
2018
2019 int MC_random(int min, int max)
2020 {
2021   /*FIXME: return mc_current_state->executed_transition->random.value;*/
2022   return simcall_mc_random(min, max);
2023 }
2024
2025 /**
2026  * \brief Schedules all the process that are ready to run
2027  */
2028 void MC_wait_for_requests(void)
2029 {
2030   smx_process_t process;
2031   smx_simcall_t req;
2032   unsigned int iter;
2033
2034   while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
2035     SIMIX_process_runall();
2036     xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
2037       req = &process->simcall;
2038       if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
2039         SIMIX_simcall_pre(req, 0);
2040     }
2041   }
2042 }
2043
2044 int MC_deadlock_check()
2045 {
2046   int deadlock = FALSE;
2047   smx_process_t process;
2048   if(xbt_swag_size(simix_global->process_list)){
2049     deadlock = TRUE;
2050     xbt_swag_foreach(process, simix_global->process_list){
2051       if(process->simcall.call != SIMCALL_NONE
2052          && MC_request_is_enabled(&process->simcall)){
2053         deadlock = FALSE;
2054         break;
2055       }
2056     }
2057   }
2058   return deadlock;
2059 }
2060
2061 /**
2062  * \brief Re-executes from the state at position start all the transitions indicated by
2063  *        a given model-checker stack.
2064  * \param stack The stack with the transitions to execute.
2065  * \param start Start index to begin the re-execution.
2066  */
2067 void MC_replay(xbt_fifo_t stack, int start)
2068 {
2069   int raw_mem = (mmalloc_get_current_heap() == raw_heap);
2070
2071   int value, i = 1, count = 1;
2072   char *req_str;
2073   smx_simcall_t req = NULL, saved_req = NULL;
2074   xbt_fifo_item_t item, start_item;
2075   mc_state_t state;
2076   smx_process_t process = NULL;
2077
2078   XBT_DEBUG("**** Begin Replay ****");
2079
2080   if(start == -1){
2081     /* Restore the initial state */
2082     MC_restore_snapshot(initial_state_safety->snapshot);
2083     /* At the moment of taking the snapshot the raw heap was set, so restoring
2084      * it will set it back again, we have to unset it to continue  */
2085     MC_UNSET_RAW_MEM;
2086   }
2087
2088   start_item = xbt_fifo_get_last_item(stack);
2089   if(start != -1){
2090     while (i != start){
2091       start_item = xbt_fifo_get_prev_item(start_item);
2092       i++;
2093     }
2094   }
2095
2096   MC_SET_RAW_MEM;
2097   xbt_dict_reset(first_enabled_state);
2098   xbt_swag_foreach(process, simix_global->process_list){
2099     if(MC_process_is_enabled(process)){
2100       char *key = bprintf("%lu", process->pid);
2101       char *data = bprintf("%d", count);
2102       xbt_dict_set(first_enabled_state, key, data, NULL);
2103       xbt_free(key);
2104     }
2105   }
2106   MC_UNSET_RAW_MEM;
2107
2108
2109   /* Traverse the stack from the state at position start and re-execute the transitions */
2110   for (item = start_item;
2111        item != xbt_fifo_get_first_item(stack);
2112        item = xbt_fifo_get_prev_item(item)) {
2113
2114     state = (mc_state_t) xbt_fifo_get_item_content(item);
2115     saved_req = MC_state_get_executed_request(state, &value);
2116
2117     MC_SET_RAW_MEM;
2118     char *key = bprintf("%lu", saved_req->issuer->pid);
2119     xbt_dict_remove(first_enabled_state, key);
2120     xbt_free(key);
2121     MC_UNSET_RAW_MEM;
2122
2123     if(saved_req){
2124       /* because we got a copy of the executed request, we have to fetch the
2125          real one, pointed by the request field of the issuer process */
2126       req = &saved_req->issuer->simcall;
2127
2128       /* Debug information */
2129       if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2130         req_str = MC_request_to_string(req, value);
2131         XBT_DEBUG("Replay: %s (%p)", req_str, state);
2132         xbt_free(req_str);
2133       }
2134     }
2135
2136     SIMIX_simcall_pre(req, value);
2137     MC_wait_for_requests();
2138
2139     count++;
2140
2141     MC_SET_RAW_MEM;
2142     /* Insert in dict all enabled processes */
2143     xbt_swag_foreach(process, simix_global->process_list){
2144       if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
2145         char *key = bprintf("%lu", process->pid);
2146         if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
2147           char *data = bprintf("%d", count);
2148           xbt_dict_set(first_enabled_state, key, data, NULL);
2149         }
2150         xbt_free(key);
2151       }
2152     }
2153     MC_UNSET_RAW_MEM;
2154
2155     /* Update statistics */
2156     mc_stats->visited_states++;
2157     mc_stats->executed_transitions++;
2158
2159   }
2160
2161   XBT_DEBUG("**** End Replay ****");
2162
2163   if(raw_mem)
2164     MC_SET_RAW_MEM;
2165   else
2166     MC_UNSET_RAW_MEM;
2167
2168
2169 }
2170
2171 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
2172 {
2173
2174   initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2175
2176   int value;
2177   char *req_str;
2178   smx_simcall_t req = NULL, saved_req = NULL;
2179   xbt_fifo_item_t item;
2180   mc_state_t state;
2181   mc_pair_t pair;
2182   int depth = 1;
2183
2184   XBT_DEBUG("**** Begin Replay ****");
2185
2186   /* Restore the initial state */
2187   MC_restore_snapshot(initial_state_liveness->snapshot);
2188
2189   /* At the moment of taking the snapshot the raw heap was set, so restoring
2190    * it will set it back again, we have to unset it to continue  */
2191   if(!initial_state_liveness->raw_mem_set)
2192     MC_UNSET_RAW_MEM;
2193
2194   if(all_stack){
2195
2196     item = xbt_fifo_get_last_item(stack);
2197
2198     while(depth <= xbt_fifo_size(stack)){
2199
2200       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2201       state = (mc_state_t) pair->graph_state;
2202
2203       if(pair->requests > 0){
2204
2205         saved_req = MC_state_get_executed_request(state, &value);
2206         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2207
2208         if(saved_req != NULL){
2209           /* because we got a copy of the executed request, we have to fetch the
2210              real one, pointed by the request field of the issuer process */
2211           req = &saved_req->issuer->simcall;
2212           //XBT_DEBUG("Req->call %u", req->call);
2213
2214           /* Debug information */
2215           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2216             req_str = MC_request_to_string(req, value);
2217             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2218             xbt_free(req_str);
2219           }
2220
2221         }
2222
2223         SIMIX_simcall_pre(req, value);
2224         MC_wait_for_requests();
2225       }
2226
2227       depth++;
2228
2229       /* Update statistics */
2230       mc_stats->visited_pairs++;
2231       mc_stats->executed_transitions++;
2232
2233       item = xbt_fifo_get_prev_item(item);
2234     }
2235
2236   }else{
2237
2238     /* Traverse the stack from the initial state and re-execute the transitions */
2239     for (item = xbt_fifo_get_last_item(stack);
2240          item != xbt_fifo_get_first_item(stack);
2241          item = xbt_fifo_get_prev_item(item)) {
2242
2243       pair = (mc_pair_t) xbt_fifo_get_item_content(item);
2244       state = (mc_state_t) pair->graph_state;
2245
2246       if(pair->requests > 0){
2247
2248         saved_req = MC_state_get_executed_request(state, &value);
2249         //XBT_DEBUG("SavedReq->call %u", saved_req->call);
2250
2251         if(saved_req != NULL){
2252           /* because we got a copy of the executed request, we have to fetch the
2253              real one, pointed by the request field of the issuer process */
2254           req = &saved_req->issuer->simcall;
2255           //XBT_DEBUG("Req->call %u", req->call);
2256
2257           /* Debug information */
2258           if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
2259             req_str = MC_request_to_string(req, value);
2260             XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
2261             xbt_free(req_str);
2262           }
2263
2264         }
2265
2266         SIMIX_simcall_pre(req, value);
2267         MC_wait_for_requests();
2268       }
2269
2270       depth++;
2271
2272       /* Update statistics */
2273       mc_stats->visited_pairs++;
2274       mc_stats->executed_transitions++;
2275     }
2276   }
2277
2278   XBT_DEBUG("**** End Replay ****");
2279
2280   if(initial_state_liveness->raw_mem_set)
2281     MC_SET_RAW_MEM;
2282   else
2283     MC_UNSET_RAW_MEM;
2284
2285 }
2286
2287 /**
2288  * \brief Dumps the contents of a model-checker's stack and shows the actual
2289  *        execution trace
2290  * \param stack The stack to dump
2291  */
2292 void MC_dump_stack_safety(xbt_fifo_t stack)
2293 {
2294
2295   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2296
2297   MC_show_stack_safety(stack);
2298
2299   if(!_sg_mc_checkpoint){
2300
2301     mc_state_t state;
2302
2303     MC_SET_RAW_MEM;
2304     while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
2305       MC_state_delete(state);
2306     MC_UNSET_RAW_MEM;
2307
2308   }
2309
2310   if(raw_mem_set)
2311     MC_SET_RAW_MEM;
2312   else
2313     MC_UNSET_RAW_MEM;
2314
2315 }
2316
2317
2318 void MC_show_stack_safety(xbt_fifo_t stack)
2319 {
2320
2321   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2322
2323   MC_SET_RAW_MEM;
2324
2325   int value;
2326   mc_state_t state;
2327   xbt_fifo_item_t item;
2328   smx_simcall_t req;
2329   char *req_str = NULL;
2330
2331   for (item = xbt_fifo_get_last_item(stack);
2332        (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
2333         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2334     req = MC_state_get_executed_request(state, &value);
2335     if(req){
2336       req_str = MC_request_to_string(req, value);
2337       XBT_INFO("%s", req_str);
2338       xbt_free(req_str);
2339     }
2340   }
2341
2342   if(!raw_mem_set)
2343     MC_UNSET_RAW_MEM;
2344 }
2345
2346 void MC_show_deadlock(smx_simcall_t req)
2347 {
2348   /*char *req_str = NULL;*/
2349   XBT_INFO("**************************");
2350   XBT_INFO("*** DEAD-LOCK DETECTED ***");
2351   XBT_INFO("**************************");
2352   XBT_INFO("Locked request:");
2353   /*req_str = MC_request_to_string(req);
2354     XBT_INFO("%s", req_str);
2355     xbt_free(req_str);*/
2356   XBT_INFO("Counter-example execution trace:");
2357   MC_dump_stack_safety(mc_stack_safety);
2358   MC_print_statistics(mc_stats);
2359 }
2360
2361
2362 void MC_show_stack_liveness(xbt_fifo_t stack){
2363   int value;
2364   mc_pair_t pair;
2365   xbt_fifo_item_t item;
2366   smx_simcall_t req;
2367   char *req_str = NULL;
2368
2369   for (item = xbt_fifo_get_last_item(stack);
2370        (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
2371         : (NULL)); item = xbt_fifo_get_prev_item(item)) {
2372     req = MC_state_get_executed_request(pair->graph_state, &value);
2373     if(req){
2374       if(pair->requests>0){
2375         req_str = MC_request_to_string(req, value);
2376         XBT_INFO("%s", req_str);
2377         xbt_free(req_str);
2378       }else{
2379         XBT_INFO("End of system requests but evolution in Büchi automaton");
2380       }
2381     }
2382   }
2383 }
2384
2385 void MC_dump_stack_liveness(xbt_fifo_t stack){
2386
2387   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2388
2389   mc_pair_t pair;
2390
2391   MC_SET_RAW_MEM;
2392   while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
2393     MC_pair_delete(pair);
2394   MC_UNSET_RAW_MEM;
2395
2396   if(raw_mem_set)
2397     MC_SET_RAW_MEM;
2398
2399 }
2400
2401
2402 void MC_print_statistics(mc_stats_t stats)
2403 {
2404   if(stats->expanded_pairs == 0){
2405     XBT_INFO("Expanded states = %lu", stats->expanded_states);
2406     XBT_INFO("Visited states = %lu", stats->visited_states);
2407   }else{
2408     XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
2409     XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
2410   }
2411   XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
2412   MC_SET_RAW_MEM;
2413   if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
2414     fprintf(dot_output, "}\n");
2415     fclose(dot_output);
2416   }
2417   MC_UNSET_RAW_MEM;
2418 }
2419
2420 void MC_assert(int prop)
2421 {
2422   if (MC_is_active() && !prop){
2423     XBT_INFO("**************************");
2424     XBT_INFO("*** PROPERTY NOT VALID ***");
2425     XBT_INFO("**************************");
2426     XBT_INFO("Counter-example execution trace:");
2427     MC_dump_stack_safety(mc_stack_safety);
2428     MC_print_statistics(mc_stats);
2429     xbt_abort();
2430   }
2431 }
2432
2433 void MC_cut(void){
2434   user_max_depth_reached = 1;
2435 }
2436
2437 void MC_process_clock_add(smx_process_t process, double amount)
2438 {
2439   mc_time[process->pid] += amount;
2440 }
2441
2442 double MC_process_clock_get(smx_process_t process)
2443 {
2444   if(mc_time){
2445     if(process != NULL)
2446       return mc_time[process->pid];
2447     else
2448       return -1;
2449   }else{
2450     return 0;
2451   }
2452 }
2453
2454 void MC_automaton_load(const char *file){
2455
2456   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2457
2458   MC_SET_RAW_MEM;
2459
2460   if (_mc_property_automaton == NULL)
2461     _mc_property_automaton = xbt_automaton_new();
2462
2463   xbt_automaton_load(_mc_property_automaton,file);
2464
2465   MC_UNSET_RAW_MEM;
2466
2467   if(raw_mem_set)
2468     MC_SET_RAW_MEM;
2469
2470 }
2471
2472 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
2473
2474   int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
2475
2476   MC_SET_RAW_MEM;
2477
2478   if (_mc_property_automaton == NULL)
2479     _mc_property_automaton = xbt_automaton_new();
2480
2481   xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);
2482
2483   MC_UNSET_RAW_MEM;
2484
2485   if(raw_mem_set)
2486     MC_SET_RAW_MEM;
2487
2488 }
2489
2490
2491