[mc] Replace some exit() calls by return

diff --git a/src/mc/Server.cpp b/src/mc/Server.cpp
index 7823da3..05902d5 100644 (file)
--- a/src/mc/Server.cpp
+++ b/src/mc/Server.cpp
@@ -106,22 +106,6 @@ void Server::shutdown()
   }
 }
 
-void Server::exit()
-{
-  // Finished:
-  int status = mc_model_checker->process().status();
-  if (WIFEXITED(status))
-    ::exit(WEXITSTATUS(status));
-  else if (WIFSIGNALED(status)) {
-    // Try to uplicate the signal of the model-checked process.
-    // This is a temporary hack so we don't try too hard.
-    kill(mc_model_checker->process().pid(), WTERMSIG(status));
-    abort();
-  } else {
-    xbt_die("Unexpected status from model-checked process");
-  }
-}
-
 void Server::resume(simgrid::mc::Process& process)
 {
   int res = process.send_message(MC_MESSAGE_CONTINUE);

diff --git a/src/mc/Server.hpp b/src/mc/Server.hpp
index 1c82e5a..62f9394 100644 (file)
--- a/src/mc/Server.hpp
+++ b/src/mc/Server.hpp
@@ -30,7 +30,6 @@ public:
   Server(pid_t pid, int socket);
   void start();
   void shutdown();
-  void exit();
   void resume(simgrid::mc::Process& process);
   void loop();
   bool handle_events();

diff --git a/src/mc/mc_comm_determinism.cpp b/src/mc/mc_comm_determinism.cpp
index bfe5e1a..41f27e6 100644 (file)
--- a/src/mc/mc_comm_determinism.cpp
+++ b/src/mc/mc_comm_determinism.cpp
@@ -290,7 +290,7 @@ void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigne
 
 /************************ Main algorithm ************************/
 
-static void MC_modelcheck_comm_determinism_main(void);
+static int MC_modelcheck_comm_determinism_main(void);
 
 static void MC_pre_modelcheck_comm_determinism(void)
 {
@@ -335,7 +335,7 @@ static void MC_pre_modelcheck_comm_determinism(void)
   xbt_fifo_unshift(mc_stack, initial_state);
 }
 
-static void MC_modelcheck_comm_determinism_main(void)
+static int MC_modelcheck_comm_determinism_main(void)
 {
 
   char *req_str = NULL;
@@ -440,7 +440,7 @@ static void MC_modelcheck_comm_determinism_main(void)
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
         MC_show_deadlock(NULL);
-        return;
+        return SIMGRID_MC_EXIT_DEADLOCK;
       }
 
       while ((state = (mc_state_t) xbt_fifo_shift(mc_stack)) != NULL) {
@@ -463,10 +463,10 @@ static void MC_modelcheck_comm_determinism_main(void)
   }
 
   MC_print_statistics(mc_stats);
-  exit(0);
+  return SIMGRID_MC_EXIT_SUCCESS;
 }
 
-void MC_modelcheck_comm_determinism(void)
+int MC_modelcheck_comm_determinism(void)
 {
   XBT_INFO("Check communication determinism");
   mc_reduce_kind = e_mc_reduce_none;
@@ -490,7 +490,7 @@ void MC_modelcheck_comm_determinism(void)
   initial_global_state->recv_diff = NULL;
   initial_global_state->send_diff = NULL;
 
-  MC_modelcheck_comm_determinism_main();
+  return MC_modelcheck_comm_determinism_main();
 }
 
 }

diff --git a/src/mc/mc_comm_pattern.h b/src/mc/mc_comm_pattern.h
index 5b2215b..68f8a10 100644 (file)
--- a/src/mc/mc_comm_pattern.h
+++ b/src/mc/mc_comm_pattern.h
@@ -90,7 +90,7 @@ XBT_PRIVATE void MC_handle_comm_pattern(e_mc_call_type_t call_type, smx_simcall_
 XBT_PRIVATE void MC_comm_pattern_free_voidp(void *p);
 XBT_PRIVATE void MC_list_comm_pattern_free_voidp(void *p);
 XBT_PRIVATE void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking);
-void MC_modelcheck_comm_determinism(void);
+int MC_modelcheck_comm_determinism(void);
 
 XBT_PRIVATE void MC_restore_communications_pattern(mc_state_t state);
 

diff --git a/src/mc/mc_liveness.cpp b/src/mc/mc_liveness.cpp
index d585d5c..9db185c 100644 (file)
--- a/src/mc/mc_liveness.cpp
+++ b/src/mc/mc_liveness.cpp
@@ -167,7 +167,7 @@ static int MC_automaton_evaluate_label(xbt_automaton_exp_label_t l,
   }
 }
 
-static void MC_modelcheck_liveness_main(void);
+static int MC_modelcheck_liveness_main(void);
 
 static void MC_pre_modelcheck_liveness(void)
 {
@@ -208,11 +208,9 @@ static void MC_pre_modelcheck_liveness(void)
       xbt_fifo_unshift(mc_stack, initial_pair);
     }
   }
-
-  MC_modelcheck_liveness_main();
 }
 
-static void MC_modelcheck_liveness_main(void)
+static int MC_modelcheck_liveness_main(void)
 {
   smx_process_t process = NULL;
   mc_pair_t current_pair = NULL;
@@ -252,7 +250,7 @@ static void MC_modelcheck_liveness_main(void)
           MC_dump_stack_liveness(mc_stack);
           MC_print_statistics(mc_stats);
           XBT_INFO("Counter-example depth : %d", counter_example_depth);
-          exit(SIMGRID_MC_EXIT_LIVENESS);
+          return SIMGRID_MC_EXIT_LIVENESS;
         }
       }
 
@@ -371,10 +369,13 @@ static void MC_modelcheck_liveness_main(void)
     } /* End of if (current_pair->requests > 0) else ... */
     
   } /* End of while(xbt_fifo_size(mc_stack) > 0) */
-  
+
+  XBT_INFO("No property violation found.");
+  MC_print_statistics(mc_stats);
+  return SIMGRID_MC_EXIT_SUCCESS;
 }
 
-void MC_modelcheck_liveness(void)
+int MC_modelcheck_liveness(void)
 {
   if (mc_reduce_kind == e_mc_reduce_unset)
     mc_reduce_kind = e_mc_reduce_none;
@@ -392,11 +393,12 @@ void MC_modelcheck_liveness(void)
   initial_global_state = xbt_new0(s_mc_global_t, 1);
 
   MC_pre_modelcheck_liveness();
+  int res = MC_modelcheck_liveness_main();
 
   /* We're done */
-  XBT_INFO("No property violation found.");
-  MC_print_statistics(mc_stats);
   xbt_free(mc_time);
+
+  return res;
 }
 
 }

diff --git a/src/mc/mc_liveness.h b/src/mc/mc_liveness.h
index e350c86..a72af0c 100644 (file)
--- a/src/mc/mc_liveness.h
+++ b/src/mc/mc_liveness.h
@@ -49,7 +49,7 @@ XBT_PRIVATE void MC_pair_delete(mc_pair_t);
 XBT_PRIVATE mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions, mc_state_t graph_state);
 XBT_PRIVATE void MC_visited_pair_delete(mc_visited_pair_t p);
 
-void MC_modelcheck_liveness(void);
+int MC_modelcheck_liveness(void);
 XBT_PRIVATE void MC_show_stack_liveness(xbt_fifo_t stack);
 XBT_PRIVATE void MC_dump_stack_liveness(xbt_fifo_t stack);
 

diff --git a/src/mc/mc_safety.cpp b/src/mc/mc_safety.cpp
index 843389b..b00c31e 100644 (file)
--- a/src/mc/mc_safety.cpp
+++ b/src/mc/mc_safety.cpp
@@ -73,7 +73,7 @@ static void MC_pre_modelcheck_safety()
 /** \brief Model-check the application using a DFS exploration
  *         with DPOR (Dynamic Partial Order Reductions)
  */
-void MC_modelcheck_safety(void)
+int MC_modelcheck_safety(void)
 {
   MC_modelcheck_safety_init();
 
@@ -126,7 +126,7 @@ void MC_modelcheck_safety(void)
 
       if(_sg_mc_termination && is_exploration_stack_state(next_state)){
           MC_show_non_termination();
-          exit(SIMGRID_MC_EXIT_NON_TERMINATION);
+          return SIMGRID_MC_EXIT_NON_TERMINATION;
       }
 
       if ((visited_state = is_visited_state(next_state)) == NULL) {
@@ -186,7 +186,7 @@ void MC_modelcheck_safety(void)
       /* Check for deadlocks */
       if (MC_deadlock_check()) {
         MC_show_deadlock(NULL);
-        exit(SIMGRID_MC_EXIT_DEADLOCK);
+        return SIMGRID_MC_EXIT_DEADLOCK;
       }
 
       /* Traverse the stack backwards until a state with a non empty interleave
@@ -259,7 +259,7 @@ void MC_modelcheck_safety(void)
 
   XBT_INFO("No property violation found.");
   MC_print_statistics(mc_stats);
-  exit(SIMGRID_MC_EXIT_SUCCESS);
+  return SIMGRID_MC_EXIT_SUCCESS;
 }
 
 static void MC_modelcheck_safety_init(void)

diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h
index 14bcd4f..adc9d6a 100644 (file)
--- a/src/mc/mc_safety.h
+++ b/src/mc/mc_safety.h
@@ -25,7 +25,7 @@ typedef enum {
 
 extern XBT_PRIVATE e_mc_reduce_t mc_reduce_kind;
 
-void MC_modelcheck_safety(void);
+int MC_modelcheck_safety(void);
 
 typedef struct XBT_PRIVATE s_mc_visited_state{
   mc_snapshot_t system_state;

diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 4dcc0ba..72e32d1 100644 (file)
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -94,19 +94,20 @@ static int do_parent(int socket, pid_t child)
     mc_mode = MC_MODE_SERVER;
     simgrid::mc::server = new simgrid::mc::Server(child, socket);
     simgrid::mc::server->start();
+    int res = 0;
     if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
-      MC_modelcheck_comm_determinism();
+      res = MC_modelcheck_comm_determinism();
     else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
-      MC_modelcheck_safety();
+      res = MC_modelcheck_safety();
     else
-      MC_modelcheck_liveness();
+      res = MC_modelcheck_liveness();
     simgrid::mc::server->shutdown();
-    simgrid::mc::server->exit();
+    return res;
   }
   catch(std::exception& e) {
     XBT_ERROR("Exception: %s", e.what());
+    return SIMGRID_MC_EXIT_ERROR;
   }
-  exit(SIMGRID_MC_EXIT_ERROR);
 }
 
 static char** argvdup(int argc, char** argv)