X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/684199641c75ec4ee775b8dda71982e8fe6d3fb8..3f66b3759acbaa15aac6aa9a80a78563031abd74:/src/mc/mc_global.c diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index f6bed22315..03d05a0a48 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -81,6 +81,10 @@ extern xbt_dynar_t stacks_areas; xbt_automaton_t _mc_property_automaton = NULL; static void MC_assert_pair(int prop); +static e_dw_location_type get_location(char *expr, dw_location_t entry); + +static void MC_get_binary_local_variables(void); +static void print_local_variables(xbt_dynar_t list); void MC_do_the_modelcheck_for_real() { if (!_surf_mc_property_file || _surf_mc_property_file[0]=='\0') { @@ -177,8 +181,9 @@ void MC_modelcheck_liveness(){ iteration of the model-checker (in RAW memory) */ MC_SET_RAW_MEM; - - mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL); + + /* Get local variables in binary for state equality detection */ + MC_get_binary_local_variables(); /* Initialize statistics */ mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1); @@ -190,9 +195,6 @@ void MC_modelcheck_liveness(){ MC_UNSET_RAW_MEM; - /* Get local variables in binary for state equality detection */ - MC_get_binary_local_variables(); - MC_ddfs_init(); /* We're done */ @@ -696,22 +698,22 @@ void MC_new_stack_area(void *stack, char *name){ /************ DWARF ***********/ -static e_dw_location_type get_location(char *expr, dw_location_t entry); +static void MC_get_binary_local_variables(){ -void MC_get_binary_local_variables(){ + mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL); - char *command = bprintf("dwarfdump -i %s", xbt_binary_name); + char *command = bprintf("dwarfdump -i %s", xbt_binary_name); FILE* fp = popen(command, "r"); if(fp == NULL) perror("popen failed"); - char *line = NULL, *tmp_line = NULL, *tmp_location = NULL, *frame_name = NULL; + char *line = NULL, *tmp_line = NULL, *tmp_location, *frame_name = NULL; ssize_t read; size_t n = 0; int valid_variable = 1, valid_frame = 1; - char *node_type = NULL, *location_type = NULL, *variable_name = NULL, *lowpc = NULL, *highpc = NULL; + char *node_type, *location_type, *variable_name = NULL, *lowpc, *highpc; xbt_dynar_t split = NULL; void *low_pc = NULL, *old_low_pc = NULL; @@ -764,6 +766,7 @@ void MC_get_binary_local_variables(){ frame->name = strdup(frame_name); frame->variables = xbt_dynar_new(sizeof(dw_local_variable_t), NULL); frame->location = xbt_new0(s_dw_location_t, 1); + free(frame_name); location_type = strtok(NULL, " "); @@ -778,9 +781,9 @@ void MC_get_binary_local_variables(){ while(read != -1 && line[0] == '['){ strtok(line, "<"); - lowpc = strdup(strtok(NULL, "<")); - highpc = strdup(strtok(NULL, ">")); - tmp_location = strdup(strtok(NULL, ">")); + lowpc = strtok(NULL, "<"); + highpc = strtok(NULL, ">"); + tmp_location = strtok(NULL, ">"); lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */ dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1); @@ -789,7 +792,7 @@ void MC_get_binary_local_variables(){ strtok(lowpc, "="); new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); strtok(highpc, "="); - new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); + new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); }else{ strtok(lowpc, "="); old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16); @@ -806,6 +809,7 @@ void MC_get_binary_local_variables(){ read = getline(&line, &n, fp); xbt_str_ltrim(line, NULL); + } }else{ @@ -831,7 +835,7 @@ void MC_get_binary_local_variables(){ read = getline(&line, &n, fp); - } + } } @@ -839,9 +843,6 @@ void MC_get_binary_local_variables(){ }else if(strcmp(node_type, "DW_TAG_variable") == 0){ /* New variable */ - variable_name = NULL; - location_type = NULL; - read = getline(&line, &n, fp); while(read != -1 && line[0] != '<'){ @@ -864,11 +865,12 @@ void MC_get_binary_local_variables(){ if(valid_variable == 1){ - location_type = strdup(strtok(NULL, " ")); + location_type = strtok(NULL, " "); dw_local_variable_t variable = xbt_new0(s_dw_local_variable_t, 1); variable->name = strdup(variable_name); variable->location = xbt_new0(s_dw_location_t, 1); + free(variable_name); if(strcmp(location_type, "")); - tmp_location = strdup(strtok(NULL, ">")); + lowpc = strtok(NULL, "<"); + highpc = strtok(NULL, ">"); + tmp_location = strtok(NULL, ">"); lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */ dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1); @@ -892,7 +894,7 @@ void MC_get_binary_local_variables(){ strtok(lowpc, "="); new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); strtok(highpc, "="); - new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); + new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); }else{ strtok(lowpc, "="); old_low_pc = (void *)strtoul(strtok(NULL, "="), NULL, 16); @@ -909,6 +911,7 @@ void MC_get_binary_local_variables(){ read = getline(&line, &n, fp); xbt_str_ltrim(line, NULL); + } }else{ @@ -921,6 +924,9 @@ void MC_get_binary_local_variables(){ variable->location->type = get_location(location_type, variable->location); read = getline(&line, &n, fp); + xbt_dynar_free(&split); + free(location_type); + } xbt_dynar_push(((dw_frame_t)xbt_dynar_get_as(mc_binary_local_variables, xbt_dynar_length(mc_binary_local_variables) - 1, dw_frame_t))->variables, &variable); @@ -941,6 +947,8 @@ void MC_get_binary_local_variables(){ read = getline(&line, &n, fp); } + + //free(tmp_line); } @@ -970,15 +978,21 @@ void MC_get_binary_local_variables(){ read = getline(&line, &n, fp); } + }else{ read = getline(&line, &n, fp); } + } + free(line); + free(command); + pclose(fp); + if(compile_unit_found == 0){ XBT_INFO("Your program must be compiled with -g"); xbt_abort(); @@ -987,10 +1001,7 @@ void MC_get_binary_local_variables(){ if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) print_local_variables(mc_binary_local_variables); - free(line); free(tmp_line); free(tmp_location); free(frame_name); - free(node_type); free(location_type); free(variable_name); free(lowpc); free(highpc); - free(command); - pclose(fp); + } void print_local_variables(xbt_dynar_t list){ @@ -1251,9 +1262,7 @@ static e_dw_location_type get_location(char *expr, dw_location_t entry){ } - free(tok); - free(tmp_tok); - /*xbt_dynar_free(&tokens);*/ + xbt_dynar_free(&tokens); return e_dw_compose; @@ -1271,8 +1280,7 @@ static e_dw_location_type get_location(char *expr, dw_location_t entry){ entry->type = e_dw_unsupported; } - free(tok); - free(tmp_tok); + xbt_dynar_free(&tokens); return entry->type;