From: Marion Guthmuller Date: Tue, 18 Sep 2012 17:05:59 +0000 (+0200) Subject: model-checker : first part to retrieve local variables of the application with dwarfdump X-Git-Tag: v3_8~146^2~47 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/784572a76e39c6c96db202387abe118658465d73?hp=2b32ae3f9b6b6e55062991921ba4b7f1af126f6a model-checker : first part to retrieve local variables of the application with dwarfdump --- diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index fa4725353d..fa16d65291 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -73,6 +73,8 @@ mc_stats_pair_t mc_stats_pair = NULL; xbt_fifo_t mc_stack_liveness = NULL; mc_snapshot_t initial_snapshot_liveness = NULL; int compare; +xbt_dynar_t mc_binary_local_variables = NULL; + extern xbt_dynar_t mmalloc_ignore; xbt_automaton_t _mc_property_automaton = NULL; @@ -175,6 +177,8 @@ void MC_modelcheck_liveness(){ MC_SET_RAW_MEM; + mc_binary_local_variables = xbt_dynar_new(sizeof(dw_frame_t), NULL); + /* Initialize statistics */ mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1); @@ -185,6 +189,8 @@ 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(); @@ -640,6 +646,8 @@ void MC_automaton_new_propositional_symbol(const char* id, void* fct) { } +/************ MC_ignore ***********/ + void MC_ignore_init(){ MC_SET_RAW_MEM; mmalloc_ignore = xbt_dynar_new(sizeof(mc_ignore_region_t), NULL); @@ -673,3 +681,537 @@ void MC_ignore(void *address, size_t size){ MC_UNSET_RAW_MEM; } + +/************ DWARF ***********/ + +static e_dw_location_type get_location(char *expr, dw_location_t entry); + +void MC_get_binary_local_variables(){ + + 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; + 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; + xbt_dynar_t split = NULL; + + read = getline(&line, &n, fp); + + while (read != -1) { + + if(n == 0) + continue; + + /* Wipeout the new line character */ + line[read - 1] = '\0'; + + if(line[0] == '<'){ + + /* Get node type */ + strtok(line, " "); + strtok(NULL, " "); + node_type = strtok(NULL, " "); + + if(strcmp(node_type, "DW_TAG_subprogram") == 0){ /* New frame */ + + read = getline(&line, &n, fp); + + while(read != -1 && line[0] != '<'){ + + if(n == 0) + continue; + + node_type = strtok(line, " "); + + if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){ + + frame_name = strdup(strtok(NULL, " ")); + read = getline(&line, &n, fp); + + }else if(node_type != NULL && strcmp(node_type, "DW_AT_frame_base") == 0){ + + if(valid_frame == 1){ + + dw_frame_t frame = xbt_new0(s_dw_frame_t, 1); + 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); + + location_type = strtok(NULL, " "); + + if(strcmp(location_type, "location->type = e_dw_loclist; + frame->location->location.loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL); + + read = getline(&line, &n, fp); + xbt_str_ltrim(line, NULL); + + while(read != -1 && line[0] == '['){ + + strtok(line, "<"); + lowpc = strdup(strtok(NULL, "<")); + highpc = strdup(strtok(NULL, ">")); + tmp_location = strdup(strtok(NULL, ">")); + lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */ + + dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1); + + strtok(lowpc, "="); + new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); + strtok(highpc, "="); + new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); + + new_entry->location = xbt_new0(s_dw_location_t, 1); + + get_location(tmp_location, new_entry->location); + + xbt_dynar_push(frame->location->location.loclist, &new_entry); + + read = getline(&line, &n, fp); + xbt_str_ltrim(line, NULL); + } + + }else{ + read = getline(&line, &n, fp); + frame->location->type = get_location(location_type, frame->location); + + } + + xbt_dynar_push(mc_binary_local_variables, &frame); + + }else{ + + read = getline(&line, &n, fp); + + } + + }else if(node_type != NULL && (strcmp(node_type, "DW_AT_declaration") == 0 || strcmp(node_type, "DW_AT_abstract_origin") == 0 || strcmp(node_type, "DW_AT_artificial") == 0)){ + + read = getline(&line, &n, fp); + valid_frame = 0; + + }else{ + + read = getline(&line, &n, fp); + + } + + } + + valid_frame = 1; + + }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] != '<'){ + + if(n == 0) + continue; + + tmp_line = strdup(line); + + node_type = strtok(line, " "); + + if(node_type != NULL && strcmp(node_type, "DW_AT_name") == 0){ + + variable_name = strdup(strtok(NULL, " ")); + read = getline(&line, &n, fp); + + }else if(node_type != NULL && strcmp(node_type, "DW_AT_location") == 0){ + + if(valid_variable == 1){ + + location_type = strdup(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); + + if(strcmp(location_type, "location->type = e_dw_loclist; + variable->location->location.loclist = xbt_dynar_new(sizeof(dw_location_entry_t), NULL); + + read = getline(&line, &n, fp); + xbt_str_ltrim(line, NULL); + + while(read != -1 && line[0] == '['){ + + strtok(line, "<"); + lowpc = strdup(strtok(NULL, "<")); + highpc = strdup(strtok(NULL, ">")); + tmp_location = strdup(strtok(NULL, ">")); + lowpc[strlen(lowpc) - 1] = '\0'; /* Remove last character '>' */ + + dw_location_entry_t new_entry = xbt_new0(s_dw_location_entry_t, 1); + + strtok(lowpc, "="); + new_entry->lowpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); + strtok(highpc, "="); + new_entry->highpc = (void *) strtoul(strtok(NULL, "="), NULL, 16); + + new_entry->location = xbt_new0(s_dw_location_t, 1); + + get_location(tmp_location, new_entry->location); + + xbt_dynar_push(variable->location->location.loclist, &new_entry); + + read = getline(&line, &n, fp); + xbt_str_ltrim(line, NULL); + } + + }else{ + + xbt_str_strip_spaces(tmp_line); + split = xbt_str_split(tmp_line, " "); + xbt_dynar_remove_at(split, 0, NULL); + location_type = xbt_str_join(split, " "); + + variable->location->type = get_location(location_type, variable->location); + read = getline(&line, &n, fp); + + } + + 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); + + }else{ + + read = getline(&line, &n, fp); + + } + + }else if(node_type != NULL && (strcmp(node_type, "DW_AT_artificial") == 0 || strcmp(node_type, "DW_AT_external") == 0)){ + + valid_variable = 0; + read = getline(&line, &n, fp); + + }else{ + + read = getline(&line, &n, fp); + + } + + } + + valid_variable = 1; + + }else{ + + read = getline(&line, &n, fp); + + } + + }else{ + + read = getline(&line, &n, fp); + + } + + } + + 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){ + + dw_frame_t frame; + dw_local_variable_t variable; + dw_location_entry_t entry; + dw_location_t location_entry; + unsigned int cursor = 0, cursor2 = 0, cursor3 = 0, cursor4 = 0; + + xbt_dynar_foreach(list, cursor, frame){ + fprintf(stderr, "Frame name : %s", frame->name); + fprintf(stderr, "Location type : %d\n", frame->location->type); + fprintf(stderr, "Variables : (%lu)\n", xbt_dynar_length(frame->variables)); + xbt_dynar_foreach(frame->variables, cursor2, variable){ + fprintf(stderr, "Name : %s", variable->name); + fprintf(stderr, "Location type : %d\n", variable->location->type); + switch(variable->location->type){ + case e_dw_loclist : + xbt_dynar_foreach(variable->location->location.loclist, cursor3, entry){ + fprintf(stderr, "Lowpc : %p, Highpc : %p,", entry->lowpc, entry->highpc); + switch(entry->location->type){ + case e_dw_register : + fprintf(stderr, " Location : in register %d\n", entry->location->location.reg); + break; + case e_dw_bregister_op: + fprintf(stderr, " Location : Add %d to the value in register %d\n", entry->location->location.breg_op.offset, entry->location->location.breg_op.reg); + break; + case e_dw_lit: + fprintf(stderr, "Value already kwnown : %d\n", entry->location->location.lit); + break; + case e_dw_fbregister_op: + fprintf(stderr, " Location : %d bytes from logical frame pointer\n", entry->location->location.fbreg_op); + break; + case e_dw_compose: + fprintf(stderr, " Location :\n"); + xbt_dynar_foreach(entry->location->location.compose, cursor4, location_entry){ + switch(location_entry->type){ + case e_dw_register : + fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg); + break; + case e_dw_bregister_op: + fprintf(stderr, " %d) add %d to the value in register %d\n", cursor4 + 1, location_entry->location.breg_op.offset, location_entry->location.breg_op.reg); + break; + case e_dw_lit: + fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit); + break; + case e_dw_fbregister_op: + fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op); + break; + case e_dw_deref: + fprintf(stderr, " %d) Pop the stack entry and treats it as an address (size of data %d)\n", cursor4 + 1, location_entry->location.deref_size); + break; + case e_dw_arithmetic : + fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic); + break; + case e_dw_piece: + fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece); + break; + case e_dw_constant : + fprintf(stderr, "%d) Constant %d\n", cursor4 + 1, location_entry->location.constant.value); + break; + default : + fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1); + break; + } + } + break; + default: + fprintf(stderr, "Location type not supported\n"); + break; + } + } + break; + case e_dw_compose: + cursor4 = 0; + fprintf(stderr, "Location :\n"); + xbt_dynar_foreach(variable->location->location.compose, cursor4, location_entry){ + switch(location_entry->type){ + case e_dw_register : + fprintf(stderr, " %d) in register %d\n", cursor4 + 1, location_entry->location.reg); + break; + case e_dw_bregister_op: + fprintf(stderr, " %d) add %d to the value in register %d\n", cursor4 + 1, location_entry->location.breg_op.offset, location_entry->location.breg_op.reg); + break; + case e_dw_lit: + fprintf(stderr, "%d) Value already kwnown : %d\n", cursor4 + 1, location_entry->location.lit); + break; + case e_dw_fbregister_op: + fprintf(stderr, " %d) %d bytes from logical frame pointer\n", cursor4 + 1, location_entry->location.fbreg_op); + break; + case e_dw_deref: + fprintf(stderr, " %d) Pop the stack entry and treats it as an address (size of data %d)\n", cursor4 + 1, location_entry->location.deref_size); + break; + case e_dw_arithmetic : + fprintf(stderr, "%d) arithmetic operation : %s\n", cursor4 + 1, location_entry->location.arithmetic); + break; + case e_dw_piece: + fprintf(stderr, "%d) The %d byte(s) previous value\n", cursor4 + 1, location_entry->location.piece); + break; + case e_dw_constant : + fprintf(stderr, "%d) Constant %d\n", cursor4 + 1, location_entry->location.constant.value); + break; + default : + fprintf(stderr, "%d) Location type not supported\n", cursor4 + 1); + break; + } + } + break; + default : + fprintf(stderr, "Location type not supported\n"); + break; + } + } + } + +} + +static e_dw_location_type get_location(char *expr, dw_location_t entry){ + + int cursor = 0; + char *tok = NULL, *tmp_tok = NULL; + + xbt_dynar_t tokens = xbt_str_split(expr, NULL); + xbt_dynar_remove_at(tokens, xbt_dynar_length(tokens) - 1, NULL); + + if(xbt_dynar_length(tokens) > 1){ + + entry->type = e_dw_compose; + entry->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL); + + while(cursor < xbt_dynar_length(tokens)){ + + tok = xbt_dynar_get_as(tokens, cursor, char*); + + if(strncmp(tok, "DW_OP_reg", 9) == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_register; + if(tok[9] == 'x'){ + new_element->location.reg = atoi(xbt_dynar_get_as(tokens, ++cursor, char*)); + }else{ + new_element->location.reg = atoi(strtok(tok, "DW_OP_reg")); + } + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "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(tokens, ++cursor, char*)); + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strncmp(tok, "DW_OP_breg", 10) == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_bregister_op; + if(tok[10] == 'x'){ + new_element->location.breg_op.reg = atoi(xbt_dynar_get_as(tokens, ++cursor, char*)); + new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens, ++cursor, char*)); + }else{ + if(strchr(tok,'+') != NULL){ + tmp_tok = strtok(tok,"DW_OP_breg"); + new_element->location.breg_op.reg = atoi(strtok(tmp_tok,"+")); + new_element->location.breg_op.offset = atoi(strtok(NULL,"+")); + }else{ + new_element->location.breg_op.reg = atoi(strtok(tok, "DW_OP_breg")); + new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens, ++cursor, char*)); + } + } + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strncmp(tok, "DW_OP_lit", 9) == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_lit; + new_element->location.lit = atoi(strtok(tok, "DW_OP_lit")); + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_piece") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_piece; + if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1) + new_element->location.piece = atoi(xbt_dynar_get_as(tokens, cursor, char*)); + else + new_element->location.piece = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0'; + xbt_dynar_push(entry->location.compose, &new_element); + + }else if(strcmp(tok, "DW_OP_abs") == 0 || + strcmp(tok, "DW_OP_and") == 0 || + strcmp(tok, "DW_OP_div") == 0 || + strcmp(tok, "DW_OP_minus") == 0 || + strcmp(tok, "DW_OP_mod") == 0 || + strcmp(tok, "DW_OP_mul") == 0 || + strcmp(tok, "DW_OP_neg") == 0 || + strcmp(tok, "DW_OP_not") == 0 || + strcmp(tok, "DW_OP_or") == 0 || + strcmp(tok, "DW_OP_plus") == 0 || + strcmp(tok, "DW_OP_plus_uconst") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_arithmetic; + new_element->location.arithmetic = strdup(strtok(tok, "DW_OP_")); + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_stack_value") == 0){ + cursor++; + }else if(strcmp(tok, "DW_OP_deref_size") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_deref; + if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1) + new_element->location.deref_size = atoi(xbt_dynar_get_as(tokens, cursor, char*)); + else + new_element->location.deref_size = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0'; + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_deref") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_deref; + new_element->location.deref_size = sizeof(void *); + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_constu") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_constant; + new_element->location.constant.is_signed = 0; + new_element->location.constant.bytes = 1; + if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1) + new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*)); + else + new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0'; + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_consts") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_constant; + new_element->location.constant.is_signed = 1; + new_element->location.constant.bytes = 1; + new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, ++cursor, char*)); + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_const1u") == 0 || + strcmp(tok, "DW_OP_const2u") == 0 || + strcmp(tok, "DW_OP_const4u") == 0 || + strcmp(tok, "DW_OP_const8u") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_constant; + new_element->location.constant.is_signed = 0; + new_element->location.constant.bytes = tok[11] - '0'; + if(strlen(xbt_dynar_get_as(tokens, ++cursor, char*)) > 1) + new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, cursor, char*)); + else + new_element->location.constant.value = xbt_dynar_get_as(tokens, cursor, char*)[0] - '0'; + xbt_dynar_push(entry->location.compose, &new_element); + }else if(strcmp(tok, "DW_OP_const1s") == 0 || + strcmp(tok, "DW_OP_const2s") == 0 || + strcmp(tok, "DW_OP_const4s") == 0 || + strcmp(tok, "DW_OP_const8s") == 0){ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_constant; + new_element->location.constant.is_signed = 1; + new_element->location.constant.bytes = tok[11] - '0'; + new_element->location.constant.value = atoi(xbt_dynar_get_as(tokens, ++cursor, char*)); + xbt_dynar_push(entry->location.compose, &new_element); + }else{ + dw_location_t new_element = xbt_new0(s_dw_location_t, 1); + new_element->type = e_dw_unsupported; + xbt_dynar_push(entry->location.compose, &new_element); + } + + cursor++; + + } + + free(tok); + free(tmp_tok); + /*xbt_dynar_free(&tokens);*/ + + return e_dw_compose; + + }else{ + + if(strncmp(expr, "DW_OP_reg", 9) == 0){ + entry->type = e_dw_register; + entry->location.reg = atoi(strtok(expr,"DW_OP_reg")); + }else if(strncmp(expr, "DW_OP_breg", 10) == 0){ + entry->type = e_dw_bregister_op; + tok = strtok(expr, "+"); + entry->location.breg_op.offset = atoi(strtok(NULL, "+")); + entry->location.breg_op.reg = atoi(strtok(tok, "DW_OP_breg")); + }else{ + entry->type = e_dw_unsupported; + } + + free(tok); + free(tmp_tok); + + return entry->type; + + } + +} diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index f7f8a366dc..5c64d95c66 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -191,6 +191,7 @@ typedef enum { e_mc_reduce_none, e_mc_reduce_dpor } e_mc_reduce_t; + extern e_mc_reduce_t mc_reduce_kind; void MC_dpor_init(void); @@ -201,6 +202,7 @@ void MC_init_safety(void); /********************************** Double-DFS for liveness property**************************************/ +extern xbt_fifo_t mc_stack_liveness; extern mc_snapshot_t initial_snapshot_liveness; extern xbt_automaton_t _mc_property_automaton; extern int compare; @@ -236,8 +238,6 @@ typedef struct s_mc_pair_stateless{ int requests; }s_mc_pair_stateless_t, *mc_pair_stateless_t; -extern xbt_fifo_t mc_stack_liveness; - mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st, int r); void MC_ddfs_init(void); void MC_ddfs(int search_cycle); @@ -255,5 +255,78 @@ extern char* _surf_mc_property_file; int create_dump(int pair); +/****** Local variables with DWARF ******/ + +typedef enum { + e_dw_loclist, + e_dw_register, + e_dw_bregister_op, + e_dw_lit, + e_dw_fbregister_op, + e_dw_piece, + e_dw_arithmetic, + e_dw_compose, + e_dw_deref, + e_dw_constant, + e_dw_unsupported +} e_dw_location_type; + +typedef struct s_dw_location{ + e_dw_location_type type; + union{ + + xbt_dynar_t loclist; + + int reg; + + struct{ + int reg; + int offset; + }breg_op; + + unsigned lit; + + int fbreg_op; + + int piece; + + int deref_size; + + xbt_dynar_t compose; + + char *arithmetic; + + struct{ + int is_signed; + int bytes; + int value; + }constant; + + }location; +}s_dw_location_t, *dw_location_t; + +typedef struct s_dw_location_entry{ + void *lowpc; + void *highpc; + dw_location_t location; +}s_dw_location_entry_t, *dw_location_entry_t; + +typedef struct s_dw_local_variable{ + char *name; + dw_location_t location; +}s_dw_local_variable_t, *dw_local_variable_t; + +typedef struct s_dw_frame{ + char *name; + dw_location_t location; + xbt_dynar_t variables; +}s_dw_frame_t, *dw_frame_t; + +/* FIXME : implement free functions for each strcuture */ + +extern xbt_dynar_t mc_binary_local_variables; + +void MC_get_binary_local_variables(void); +void print_local_variables(xbt_dynar_t list); #endif