[mc] New message for stack_area

diff --git a/src/include/mc/datatypes.h b/src/include/mc/datatypes.h
index 728bb0e..22c7e4f 100644 (file)
--- a/src/include/mc/datatypes.h
+++ b/src/include/mc/datatypes.h
@@ -31,7 +31,6 @@ typedef struct s_mc_heap_ignore_region{
 
 typedef struct s_stack_region{
   void *address;
-  char *process_name;
   void *context;
   size_t size;
   int block;

diff --git a/src/mc/mc_compare.cpp b/src/mc/mc_compare.cpp
index a764970..55db660 100644 (file)
--- a/src/mc/mc_compare.cpp
+++ b/src/mc/mc_compare.cpp
@@ -60,7 +60,6 @@ extern "C" {
 static void stack_region_free(stack_region_t s)
 {
   if (s) {
-    xbt_free(s->process_name);
     xbt_free(s);
   }
 }

diff --git a/src/mc/mc_ignore.c b/src/mc/mc_ignore.c
index bde464c..d0c2c37 100644 (file)
--- a/src/mc/mc_ignore.c
+++ b/src/mc/mc_ignore.c
@@ -346,6 +346,13 @@ void MC_ignore_local_variable(const char *var_name, const char *frame_name)
 
 }
 
+void MC_stack_area_add(stack_region_t stack_area)
+{
+  if (stacks_areas == NULL)
+    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
+  xbt_dynar_push(stacks_areas, &stack_area);
+}
+
 /** @brief Register a stack in the model checker
  *
  *  The stacks are allocated in the heap. The MC handle them especially
@@ -361,16 +368,10 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t
 {
 
   int raw_mem_set = (mmalloc_get_current_heap() == mc_heap);
-
   MC_SET_MC_HEAP;
 
-  if (stacks_areas == NULL)
-    stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
-
-  stack_region_t region = NULL;
-  region = xbt_new0(s_stack_region_t, 1);
+  stack_region_t region = xbt_new0(s_stack_region_t, 1);
   region->address = stack;
-  region->process_name = process && process->name ? strdup(process->name) : NULL;
   region->context = context;
   region->size = size;
   region->block =
@@ -383,7 +384,14 @@ void MC_new_stack_area(void *stack, smx_process_t process, void *context, size_t
 #endif
   region->process_index = -1;
 
-  xbt_dynar_push(stacks_areas, &region);
+  if (mc_mode == MC_MODE_CLIENT) {
+    s_mc_stack_region_message_t message;
+    message.type = MC_MESSAGE_STACK_REGION;
+    message.stack_region = *region;
+    MC_client_send_message(&message, sizeof(message));
+  }
+
+  MC_stack_area_add(region);
 
   if (!raw_mem_set)
     MC_SET_STD_HEAP;

diff --git a/src/mc/mc_ignore.h b/src/mc/mc_ignore.h
index 35572d4..3f01981 100644 (file)
--- a/src/mc/mc_ignore.h
+++ b/src/mc/mc_ignore.h
@@ -15,7 +15,9 @@ SG_BEGIN_DECL();
 void MC_heap_region_ignore_insert(mc_heap_ignore_region_t region);
 void MC_heap_region_ignore_send(mc_heap_ignore_region_t region);
 void MC_process_ignore_memory(mc_process_t process, void *addr, size_t size);
+void MC_stack_area_add(stack_region_t stack_area);
 
 xbt_dynar_t MC_checkpoint_ignore_new(void);
 
+
 SG_END_DECL();

diff --git a/src/mc/mc_protocol.h b/src/mc/mc_protocol.h
index 9623ec0..a33d00e 100644 (file)
--- a/src/mc/mc_protocol.h
+++ b/src/mc/mc_protocol.h
@@ -43,6 +43,7 @@ typedef enum {
   MC_MESSAGE_IGNORE_HEAP,
   MC_MESSAGE_UNIGNORE_HEAP,
   MC_MESSAGE_IGNORE_MEMORY,
+  MC_MESSAGE_STACK_REGION,
 } e_mc_message_type;
 
 #define MC_MESSAGE_LENGTH 512
@@ -74,6 +75,11 @@ typedef struct s_mc_ignore_memory_message {
   size_t size;
 } s_mc_ignore_memory_message_t, *mc_ignore_memory_message_t;
 
+typedef struct s_mc_stack_region_message {
+  e_mc_message_type type;
+  s_stack_region_t stack_region;
+} s_mc_stack_region_message_t, *mc_stack_region_message_t;
+
 int MC_protocol_send(int socket, void* message, size_t size);
 int MC_protocol_send_simple_message(int socket, int type);
 int MC_protocol_hello(int socket);

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index fb123fa..d9a024f 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -178,6 +178,19 @@ void s_mc_server::handle_events()
         }
         break;
 
+      case MC_MESSAGE_STACK_REGION:
+        {
+          XBT_DEBUG("Received stack area");
+          s_mc_stack_region_message_t message;
+          if (size != sizeof(message))
+            xbt_die("Broken messsage");
+          memcpy(&message, buffer, sizeof(message));
+          stack_region_t stack_region = xbt_new(s_stack_region_t, 1);
+          *stack_region = message.stack_region;
+          MC_stack_area_add(stack_region);
+        }
+        break;
+
       default:
         xbt_die("Unexpected message from model-checked application");