#include "mc_safety.h"
#include "mc_private.h"
#include "mc_smx.h"
+#include "mc_xbt.hpp"
using simgrid::mc::remote;
type = "iSend";
char* p = pointer_to_string(simcall_comm_isend__get__src_buff(req));
char* bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
- if (issuer->smx_host)
+ if (issuer->host)
args =
bprintf("src=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
MC_smx_process_get_host_name(issuer),
type = "iRecv";
char* p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
char* bs = buff_size_to_string(size);
- if (issuer->smx_host)
+ if (issuer->host)
args =
bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", issuer->pid,
MC_smx_process_get_host_name(issuer),
&comms, sizeof(comms), remote(simcall_comm_waitany__get__comms(req)));
if (!xbt_dynar_is_empty(&comms)) {
smx_synchro_t remote_sync;
- MC_process_read_dynar_element(&mc_model_checker->process(),
- &remote_sync, simcall_comm_waitany__get__comms(req), value,
+ read_element(mc_model_checker->process(),
+ &remote_sync, remote(simcall_comm_waitany__get__comms(req)), value,
sizeof(remote_sync));
char* p = pointer_to_string(remote_sync);
args = bprintf("comm=%s (%d of %lu)",
} else {
type = "TestAny";
args =
- bprintf("(%d of %lu)", value + 1,
- MC_process_read_dynar_length(&mc_model_checker->process(),
+ bprintf("(%d of %zu)", value + 1,
+ read_length(mc_model_checker->process(),
simcall_comm_testany__get__comms(req)));
}
break;
break;
case SIMCALL_COMM_WAITANY: {
- MC_process_read_dynar_element(
- &mc_model_checker->process(), &remote_act, simcall_comm_waitany__get__comms(req),
+ read_element(
+ mc_model_checker->process(), &remote_act,
+ remote(simcall_comm_waitany__get__comms(req)),
idx, sizeof(remote_act));
}
break;
case SIMCALL_COMM_TESTANY: {
- MC_process_read_dynar_element(
- &mc_model_checker->process(), &remote_act, simcall_comm_testany__get__comms(req),
+ read_element(
+ mc_model_checker->process(), &remote_act,
+ remote(simcall_comm_testany__get__comms(req)),
idx, sizeof(remote_act));
}
break;
switch (req->call) {
case SIMCALL_COMM_ISEND:
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] iSend", issuer->pid,
MC_smx_process_get_host_name(issuer));
break;
case SIMCALL_COMM_IRECV:
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] iRecv", issuer->pid,
MC_smx_process_get_host_name(issuer));
case SIMCALL_COMM_WAIT: {
if (value == -1) {
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] WaitTimeout", issuer->pid,
MC_smx_process_get_host_name(issuer));
smx_process_t src_proc = MC_smx_resolve_process(synchro.comm.src_proc);
smx_process_t dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc);
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", issuer->pid,
MC_smx_process_get_host_name(issuer),
mc_model_checker->process().read_bytes(&synchro,
sizeof(synchro), remote(remote_act));
if (synchro.comm.src_proc == NULL || synchro.comm.dst_proc == NULL) {
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] Test FALSE", issuer->pid,
MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] Test FALSE", issuer->pid);
} else {
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] Test TRUE", issuer->pid,
MC_smx_process_get_host_name(issuer));
}
case SIMCALL_COMM_WAITANY: {
- unsigned long comms_size = MC_process_read_dynar_length(
- &mc_model_checker->process(), simcall_comm_waitany__get__comms(req));
- if (issuer->smx_host)
+ unsigned long comms_size = read_length(
+ mc_model_checker->process(), remote(simcall_comm_waitany__get__comms(req)));
+ if (issuer->host)
label =
bprintf("[(%lu)%s] WaitAny [%d of %lu]", issuer->pid,
MC_smx_process_get_host_name(issuer), value + 1,
case SIMCALL_COMM_TESTANY:
if (value == -1) {
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] TestAny FALSE", issuer->pid,
MC_smx_process_get_host_name(issuer));
else
label = bprintf("[(%lu)] TestAny FALSE", issuer->pid);
} else {
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] TestAny TRUE [%d of %lu]", issuer->pid,
MC_smx_process_get_host_name(issuer), value + 1,
break;
case SIMCALL_MC_RANDOM:
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] MC_RANDOM (%d)", issuer->pid,
MC_smx_process_get_host_name(issuer), value);
break;
case SIMCALL_MC_SNAPSHOT:
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] MC_SNAPSHOT", issuer->pid,
MC_smx_process_get_host_name(issuer));
break;
case SIMCALL_MC_COMPARE_SNAPSHOTS:
- if (issuer->smx_host)
+ if (issuer->host)
label =
bprintf("[(%lu)%s] MC_COMPARE_SNAPSHOTS", issuer->pid,
MC_smx_process_get_host_name(issuer));