src/mc/mc_global.c

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