src/mc/mc_global.c

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