[mc] MCed memory access in MC_state_get_request()

diff --git a/src/mc/mc_process.c b/src/mc/mc_process.c
index 7e047ab..ba3968c 100644 (file)
--- a/src/mc/mc_process.c
+++ b/src/mc/mc_process.c
@@ -530,6 +530,16 @@ void MC_process_write(mc_process_t process, const void* local, void* remote, siz
   }
 }
 
+unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar)
+{
+  if (!remote_dynar)
+    return 0;
+  unsigned long res;
+  MC_process_read_simple(process, &res,
+    &((xbt_dynar_t)remote_dynar)->used, sizeof(res));
+  return res;
+}
+
 static pthread_once_t zero_buffer_flag = PTHREAD_ONCE_INIT;
 static const void* zero_buffer;
 static const int zero_buffer_size = 10 * 4096;

diff --git a/src/mc/mc_process.h b/src/mc/mc_process.h
index 84d90cd..770bf3c 100644 (file)
--- a/src/mc/mc_process.h
+++ b/src/mc/mc_process.h
@@ -159,11 +159,12 @@ const void* MC_process_read(mc_process_t process,
   void* local, const void* remote, size_t len,
   int process_index);
 
+// Simplified versions/wrappers (whould be moved in mc_address_space):
 const void* MC_process_read_simple(mc_process_t process,
   void* local, const void* remote, size_t len);
-
 const void* MC_process_read_dynar_element(mc_process_t process,
   void* local, const void* remote_dynar, size_t i);
+unsigned long MC_process_read_dynar_length(mc_process_t process, const void* remote_dynar);
 
 /** Write data to a process memory
  *

diff --git a/src/mc/mc_state.c b/src/mc/mc_state.c
index d67fe35..02dc8ad 100644 (file)
--- a/src/mc/mc_state.c
+++ b/src/mc/mc_state.c
@@ -233,8 +233,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
         case SIMCALL_COMM_WAITANY:
           *value = -1;
           while (procstate->interleave_count <
-                 xbt_dynar_length(simcall_comm_waitany__get__comms
-                                  (&process->simcall))) {
+                MC_process_read_dynar_length(&mc_model_checker->process,
+                  simcall_comm_waitany__get__comms(&process->simcall))) {
             if (MC_request_is_enabled_by_idx
                 (&process->simcall, procstate->interleave_count++)) {
               *value = procstate->interleave_count - 1;
@@ -243,8 +243,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           }
 
           if (procstate->interleave_count >=
-              xbt_dynar_length(simcall_comm_waitany__get__comms
-                               (&process->simcall)))
+              MC_process_read_dynar_length(&mc_model_checker->process,
+                simcall_comm_waitany__get__comms(&process->simcall)))
             procstate->state = MC_DONE;
 
           if (*value != -1)
@@ -256,8 +256,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           start_count = procstate->interleave_count;
           *value = -1;
           while (procstate->interleave_count <
-                 xbt_dynar_length(simcall_comm_testany__get__comms
-                                  (&process->simcall))) {
+                  MC_process_read_dynar_length(&mc_model_checker->process,
+                    simcall_comm_testany__get__comms(&process->simcall))) {
             if (MC_request_is_enabled_by_idx
                 (&process->simcall, procstate->interleave_count++)) {
               *value = procstate->interleave_count - 1;
@@ -266,8 +266,8 @@ smx_simcall_t MC_state_get_request(mc_state_t state, int *value)
           }
 
           if (procstate->interleave_count >=
-              xbt_dynar_length(simcall_comm_testany__get__comms
-                               (&process->simcall)))
+              MC_process_read_dynar_length(&mc_model_checker->process,
+                simcall_comm_testany__get__comms(&process->simcall)))
             procstate->state = MC_DONE;
 
           if (*value != -1 || start_count == 0)