model-checker : functions only used in mc_global declared as static and remove unnece...

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

diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c
index a4e94d3..03d05a0 100644 (file)
--- 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, "<loclist") == 0){
 
@@ -881,9 +883,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);
@@ -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,17 +978,18 @@ void MC_get_binary_local_variables(){
         read = getline(&line, &n, fp);
 
       }
+
  
     }else{
 
       read = getline(&line, &n, fp);
 
     }
+    
 
   }
 
-  free(line); free(tmp_line); free(tmp_location); free(frame_name);
-  free(location_type); free(variable_name); free(lowpc); free(highpc);
+  free(line);
   free(command);
   pclose(fp);
 
@@ -1271,8 +1280,6 @@ 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;