[trace] free dicts on TRACE_end.

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

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index b0877f6..6c35380 100644 (file)
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -5,6 +5,7 @@
 
 #include "mc_private.h"
 #include <unistd.h>
+#include <sys/wait.h>
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_liveness, mc,
                                 "Logging specific to algorithms for liveness properties verification");
@@ -33,6 +34,45 @@ unsigned int hash_region(char *str, int str_len){
 
 }
 
+int create_dump(int pair)
+{
+   // Try to enable core dumps
+  struct rlimit core_limit;
+  core_limit.rlim_cur = RLIM_INFINITY;
+  core_limit.rlim_max = RLIM_INFINITY;
+  
+  if(setrlimit(RLIMIT_CORE, &core_limit) < 0)
+    fprintf(stderr, "setrlimit: %s\nWarning: core dumps may be truncated or non-existant\n", strerror(errno));
+  
+  int status;
+  switch(fork()){
+  case 0:
+    // We are the child process -- run the actual program
+    abort();
+    break;
+    
+  case -1:
+    // An error occurred, shouldn't happen
+    perror("fork");
+    return -1;
+    
+  default:
+    // We are the parent process -- wait for the child process to exit
+    if(wait(&status) < 0)
+      perror("wait");
+    printf("child exited with status %d\n", status);
+    if(WIFSIGNALED(status) && WCOREDUMP(status)){
+      printf("got a core dump\n");
+      char *core_name = malloc(20);
+      sprintf(core_name,"mv core core_%d", pair); 
+      system((char *)core_name);
+      free(core_name);
+    }
+  }
+
+  return 0;
+}
+
 int reached(xbt_state_t st){
 
   raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@ -335,6 +375,8 @@ void set_pair_reached(xbt_state_t st){
     MC_SET_RAW_MEM;
   else
     MC_UNSET_RAW_MEM;
+
+  create_dump(xbt_dynar_length(reached_pairs));
     
 }
 
@@ -1268,60 +1310,3 @@ void MC_ddfs(int search_cycle){
     MC_UNSET_RAW_MEM;
 
 }
-
-
-#ifdef SIMGRID_TEST
-
-XBT_TEST_SUITE("mc_liveness", "Model checking liveness properties");
-XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(mc_liveness);
-
-XBT_TEST_UNIT("snapshots_comparison", test_compare_snapshot, "Comparison of snapshots")
-{
-
-  MC_SET_RAW_MEM;
-
-  /* Save first snapshot */
-  mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(snapshot1);
-
-  /* Save second snapshot */
-  mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(snapshot2);
-
-  MC_UNSET_RAW_MEM;
-
-  xbt_test_assert(snapshot_compare(snapshot1, snapshot2) == 0, "Different consecutive snapshot");
-  
-
-}
-
-XBT_TEST_UNIT("snapshots_comparison2", test2_compare_snapshot, "Comparison of snapshots with modification between")
-{
-
-  MC_SET_RAW_MEM;
-
-  /* Save first snapshot */
-  mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(snapshot1);
-
-  MC_UNSET_RAW_MEM;
-
-  void *test = snapshot1;
-  test = (char*)test+1;
-  char* t= strdup("toto");
-  t=strdup("tat");
-
-  MC_SET_RAW_MEM;
-
-  /* Save second snapshot */
-  mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1);
-  MC_take_snapshot_liveness(snapshot2);
-
-  xbt_test_assert(snapshot_compare(snapshot1, snapshot2) != 0, "Same snapshot with new allocations");
-
-  MC_UNSET_RAW_MEM;
-  
-
-}
-
-#endif