From 02690c93e202e3c89febc4a4a06350e61a54e191 Mon Sep 17 00:00:00 2001 From: Gabriel Corona Date: Tue, 26 May 2015 14:22:42 +0200 Subject: [PATCH 1/1] [mc] Fix cross-process access to simcall_comm_***any__get__comms The array in an array of smx_synchro_t and not of s_smx_synchro_t. --- src/mc/mc_state.cpp | 20 +++++++++++++------- 1 file changed, 13 insertions(+), 7 deletions(-) diff --git a/src/mc/mc_state.cpp b/src/mc/mc_state.cpp index 208187ed24..7e03998891 100644 --- a/src/mc/mc_state.cpp +++ b/src/mc/mc_state.cpp @@ -105,24 +105,30 @@ void MC_state_set_executed_request(mc_state_t state, smx_simcall_t req, * corresponding communication action so it can be treated later by the dependence * function. */ switch (req->call) { - case SIMCALL_COMM_WAITANY: + case SIMCALL_COMM_WAITANY: { state->internal_req.call = SIMCALL_COMM_WAIT; state->internal_req.issuer = req->issuer; + smx_synchro_t remote_comm; read_element(mc_model_checker->process(), - &state->internal_comm, remote(simcall_comm_waitany__get__comms(req)), - value, sizeof(state->internal_comm)); + &remote_comm, remote(simcall_comm_waitany__get__comms(req)), + value, sizeof(remote_comm)); + mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); simcall_comm_wait__set__comm(&state->internal_req, &state->internal_comm); simcall_comm_wait__set__timeout(&state->internal_req, 0); break; + } case SIMCALL_COMM_TESTANY: state->internal_req.call = SIMCALL_COMM_TEST; state->internal_req.issuer = req->issuer; - if (value > 0) - read_element(mc_model_checker->process(), - &state->internal_comm, remote(simcall_comm_testany__get__comms(req)), - value, sizeof(state->internal_comm)); + if (value > 0) { + smx_synchro_t remote_comm; + read_element(mc_model_checker->process(), + &remote_comm, remote(simcall_comm_testany__get__comms(req)), + value, sizeof(remote_comm)); + mc_model_checker->process().read(&state->internal_comm, remote(remote_comm)); + } simcall_comm_test__set__comm(&state->internal_req, &state->internal_comm); simcall_comm_test__set__result(&state->internal_req, value); -- 2.20.1