- unsigned int index = 0;
- // TODO, add support for the subtypes?
-
- switch (req->call) {
- case SIMCALL_NONE:
- return false;
-
- case SIMCALL_SEM_ACQUIRE:
- xbt_die("Don't use semaphores in model-checked code, it's not supported yet");
- case SIMCALL_COND_WAIT:
- xbt_die("Don't use condition variables in model-checked code, it's not supported yet");
-
- case SIMCALL_COMM_WAIT:
- {
- /* FIXME: check also that src and dst processes are not suspended */
- simgrid::kernel::activity::Comm *act =
- static_cast<simgrid::kernel::activity::Comm*>(simcall_comm_wait__get__comm(req));
-
-#if SIMGRID_HAVE_MC
- // Fetch from MCed memory:
- // HACK, type puning
- if (mc_model_checker != nullptr) {
- simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
- mc_model_checker->process().read(temp_comm, remote(act));
- act = static_cast<simgrid::kernel::activity::Comm*>(temp_comm.getBuffer());
- }
-#endif
-
- if (simcall_comm_wait__get__timeout(req) >= 0) {
- /* If it has a timeout it will be always be enabled, because even if the
- * communication is not ready, it can timeout and won't block. */
- if (_sg_mc_timeout == 1)
- return true;
- }
- /* On the other hand if it hasn't a timeout, check if the comm is ready.*/
- else if (act->detached && act->src_proc == nullptr
- && act->type == SIMIX_COMM_READY)
- return (act->dst_proc != nullptr);
- return (act->src_proc && act->dst_proc);
- }
-
- case SIMCALL_COMM_WAITANY: {
- xbt_dynar_t comms;
- simgrid::kernel::activity::Comm *act =
- static_cast<simgrid::kernel::activity::Comm*>(simcall_comm_wait__get__comm(req));