- case SIMCALL_COMM_WAITANY:
- /* Check if it has at least one communication ready */
- xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act)
+ case SIMCALL_COMM_WAITANY: {
+#ifdef HAVE_MC
+ // Read dynar:
+ s_xbt_dynar_t comms;
+ MC_process_read_simple(&mc_model_checker->process,
+ &comms, simcall_comm_waitany__get__comms(req), sizeof(comms));
+ // Read dynar buffer:
+ assert(comms.elmsize == sizeof(act));
+ size_t buffer_size = comms.elmsize * comms.used;
+ char buffer[buffer_size];
+ MC_process_read_simple(&mc_model_checker->process,
+ buffer, comms.data, sizeof(buffer));
+#endif
+
+#ifdef HAVE_MC
+ for (index = 0; index < comms.used; ++index) {
+ memcpy(&act, buffer + comms.elmsize * index, sizeof(act));
+#else
+ xbt_dynar_foreach(simcall_comm_waitany__get__comms(req), index, act) {
+#endif
+
+#ifdef HAVE_MC
+ // Fetch from MCed memory:
+ if (!MC_process_is_self(&mc_model_checker->process)) {
+ MC_process_read(&mc_model_checker->process, MC_PROCESS_NO_FLAG,
+ &temp_synchro, act, sizeof(temp_synchro),
+ MC_PROCESS_INDEX_ANY);
+ act = &temp_synchro;
+ }
+#endif
+