Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : initialize variables
[simgrid.git] / src / mc / mc_dpor.c
index 7c5b998..a8abd69 100644 (file)
@@ -82,11 +82,11 @@ static int is_visited_state(){
       state_test = (mc_visited_state_t)xbt_dynar_get_as(visited_states, cursor, mc_visited_state_t);
       bytes_used_test = state_test->heap_bytes_used;
       nb_processes_test = state_test->nb_processes;
-      if(nb_processes_test < current_nb_processes)
+      if(nb_processes_test < current_nb_processes){
         start = cursor + 1;
-      if(nb_processes_test > current_nb_processes)
-        end = cursor - 1; 
-      if(nb_processes_test == current_nb_processes){
+      }else if(nb_processes_test > current_nb_processes){
+        end = cursor - 1;
+      }else if(nb_processes_test == current_nb_processes){
         if(bytes_used_test < current_bytes_used)
           start = cursor + 1;
         if(bytes_used_test > current_bytes_used)
@@ -246,7 +246,7 @@ void MC_dpor_init()
 void MC_dpor(void)
 {
 
-  char *req_str;
+  char *req_str = NULL;
   int value;
   smx_simcall_t req = NULL, prev_req = NULL;
   mc_state_t state = NULL, prev_state = NULL, next_state = NULL, restore_state=NULL;
@@ -488,6 +488,7 @@ void MC_dpor(void)
           XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety));
           break;
         } else {
+          XBT_DEBUG("Delete state at depth %d",xbt_fifo_size(mc_stack_safety) + 1); 
           MC_state_delete(state);
         }
       }