+ // Read object from MCed memory:
+ s_smx_synchro_t synchro1, synchro2;
+ if (r1->call == SIMCALL_COMM_WAIT) {
+ MC_process_read_simple(&mc_model_checker->process, &synchro1,
+ simcall_comm_wait__get__comm(r1), sizeof(synchro1));
+ }
+ if (r2->call == SIMCALL_COMM_WAIT) {
+ MC_process_read_simple(&mc_model_checker->process, &synchro2,
+ simcall_comm_wait__get__comm(r2), sizeof(synchro2));
+ }
+ if (r1->call == SIMCALL_COMM_TEST) {
+ MC_process_read_simple(&mc_model_checker->process, &synchro1,
+ simcall_comm_test__get__comm(r1), sizeof(synchro1));
+ }
+ if (r2->call == SIMCALL_COMM_TEST) {
+ MC_process_read_simple(&mc_model_checker->process, &synchro2,
+ simcall_comm_test__get__comm(r2), sizeof(synchro2));
+ }
+
+ if ((r1->call == SIMCALL_COMM_ISEND || r1->call == SIMCALL_COMM_IRECV)
+ && r2->call == SIMCALL_COMM_WAIT) {
+
+ smx_rdv_t rdv =
+ r1->call ==
+ SIMCALL_COMM_ISEND ? simcall_comm_isend__get__rdv(r1) :
+ simcall_comm_irecv__get__rdv(r1);