model-checker : fix index of dynar in get_location

[simgrid.git] / src / mc / mc_global.c

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index 461e0b5..ff19ead 100644 (file)
--- a/src/mc/mc_global.c
+++ b/src/mc/mc_global.c
@@ -122,8 +122,6 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr);
 static dw_frame_t get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset);
 static size_t data_bss_ignore_size(void *address);
 static void MC_get_global_variables(char *elf_file);
-static void heap_ignore_region_free(mc_heap_ignore_region_t r);
-static void heap_ignore_region_free_voidp(void *r);
 
 void MC_do_the_modelcheck_for_real() {
 
@@ -191,7 +189,6 @@ void MC_init(){
   get_libsimgrid_plt_section();
   get_binary_plt_section();
 
-  MC_ignore_data_bss(&end_raw_heap, sizeof(end_raw_heap));
   MC_ignore_data_bss(&mc_comp_times, sizeof(mc_comp_times));
   MC_ignore_data_bss(&mc_snapshot_comparison_time, sizeof(mc_snapshot_comparison_time)); 
 
@@ -746,12 +743,12 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
 
 /************ MC_ignore ***********/ 
 
-static void heap_ignore_region_free(mc_heap_ignore_region_t r){
+void heap_ignore_region_free(mc_heap_ignore_region_t r){
   if(r)
     xbt_free(r);
 }
 
-static void heap_ignore_region_free_voidp(void *r){
+void heap_ignore_region_free_voidp(void *r){
   heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
 }
 
@@ -999,6 +996,7 @@ void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
   region->process_name = strdup(name);
   region->context = context;
   region->size = size;
+  region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
   xbt_dynar_push(stacks_areas, &region);
   
   MC_UNSET_RAW_MEM;
@@ -1515,13 +1513,13 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_fbregister_op;
-        new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_bregister_op;
         new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
-        new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
@@ -1531,7 +1529,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_piece:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_piece;
-        new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         /*if(strlen(xbt_dynar_get_as(tokens2, 1, char*)) > 1)
           new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, 1, char*));
         else
@@ -1540,7 +1538,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_plus_uconst;
-        new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, 1, char *));
+        new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strcmp(tok, "DW_OP_abs") == 0 || 
                strcmp(tok, "DW_OP_and") == 0 ||
@@ -1560,7 +1558,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
       }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_deref;
-        new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, 1, char*));
+        new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
           new_element->location.deref_size = atoi(xbt_dynar_get_as(tokens, cursor, char*));
         else
@@ -1575,7 +1573,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_uconstant;
         new_element->location.uconstant.bytes = 1;
-        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
           new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens, cursor, char*)));
         else
@@ -1585,7 +1583,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_sconstant;
         new_element->location.sconstant.bytes = 1;
-        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
                strcmp(tok2, "DW_OP_const2u:") == 0 ||
@@ -1594,7 +1592,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_uconstant;
         new_element->location.uconstant.bytes = tok2[11] - '0';
-        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         /*if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1)
           new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*));
         else
@@ -1607,7 +1605,7 @@ static dw_location_t get_location(xbt_dict_t location_list, char *expr){
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
         new_element->type = e_dw_sconstant;
         new_element->location.sconstant.bytes = tok2[11] - '0';
-        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, 1, char*)));
+        new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
         xbt_dynar_push(loc->location.compose, &new_element);
       }else{
         dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
@@ -1802,6 +1800,17 @@ static void MC_get_global_variables(char *elf_file){
        || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), ".bss") == 0)
        || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "stderr", 6) == 0)
        || (strncmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "counter", 7) == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapinfo1") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapinfo2") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapbase1") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapbase2") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapsize1") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heapsize2") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "heaplimit") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "ignore_done") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "s_heap") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "to_ignore1") == 0)
+       || (strcmp(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 1, char*), "to_ignore2") == 0)
        || ((size_t)strtoul(xbt_dynar_get_as(line_tokens, xbt_dynar_length(line_tokens) - 2, char*), NULL, 16) == 0))
       continue;