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