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