From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Tue, 3 Jul 2012 13:42:08 +0000 (+0200)
Subject: model-checker : create core dump without termination for each acceptance pair
X-Git-Tag: v3_8~368
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d0d59f5fddb48acb3ce7315d3a992c8d3669afcd

model-checker : create core dump without termination for each acceptance pair
---

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index c0012eeb96..c841a9663b 100644
--- 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
+    *(int *)1 = 2;  // segfault
+    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));
     
 }
 
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index d9b9f7f5d8..519e7088a2 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -280,5 +280,9 @@ extern xbt_fifo_t mc_stack_safety;
 extern int _surf_mc_checkpoint;
 extern char* _surf_mc_property_file;
 
+/****** Core dump ******/
+
+int create_dump(int pair);
+
 
 #endif