case MC_MESSAGE_REGISTER_SYMBOL:
{
- s_mc_register_symbol_message_t message;
- if (size != sizeof(message))
- xbt_die("Broken message");
- memcpy(&message, buffer, sizeof(message));
- if (message.callback)
- xbt_die("Support for client-side function proposition is not implemented.");
- XBT_DEBUG("Received symbol: %s", message.name);
-
- if (simgrid::mc::property_automaton == nullptr)
- simgrid::mc::property_automaton = xbt_automaton_new();
-
- simgrid::mc::RemoteClient* process = &this->process();
- simgrid::mc::RemotePtr<int> address
- = simgrid::mc::remote((int*) message.data);
- simgrid::xbt::add_proposition(simgrid::mc::property_automaton,
- message.name,
- [process, address]() { return process->read(address); }
- );
-
- break;
+ s_mc_message_register_symbol_t message;
+ if (size != sizeof(message))
+ xbt_die("Broken message");
+ memcpy(&message, buffer, sizeof(message));
+ if (message.callback)
+ xbt_die("Support for client-side function proposition is not implemented.");
+ XBT_DEBUG("Received symbol: %s", message.name);
+
+ if (simgrid::mc::property_automaton == nullptr)
+ simgrid::mc::property_automaton = xbt_automaton_new();
+
+ simgrid::mc::RemoteClient* process = &this->process();
+ simgrid::mc::RemotePtr<int> address = simgrid::mc::remote((int*)message.data);
+ simgrid::xbt::add_proposition(simgrid::mc::property_automaton, message.name,
+ [process, address]() { return process->read(address); });
+
+ break;
}
case MC_MESSAGE_WAITING:
}
#if HAVE_SMPI
- // TODO, send a message to implement this in the MCed process
if(snapshot->privatization_index >= 0) {
// Fix the privatization mmap:
- s_mc_message_restore message;
- message.type = MC_MESSAGE_RESTORE;
- message.index = snapshot->privatization_index;
+ s_mc_message_restore message{MC_MESSAGE_RESTORE, snapshot->privatization_index};
mc_model_checker->process().getChannel().send(message);
}
#endif
}
void Client::handleContinue(mc_message_t* msg)
{
+ /* Nothing to do */
}
void Client::handleSimcall(s_mc_message_simcall_handle_t* message)
{
void Client::declareSymbol(const char* name, int* value)
{
- s_mc_register_symbol_message_t message;
+ s_mc_message_register_symbol_t message;
message.type = MC_MESSAGE_REGISTER_SYMBOL;
if (strlen(name) + 1 > sizeof(message.name))
xbt_die("Symbol is too long");
};
typedef struct s_mc_message_int mc_message_int_t;
+/* Client->Server */
struct s_mc_message_ignore_heap {
e_mc_message_type type;
int block;
};
typedef struct s_mc_message_stack_region s_mc_message_stack_region_t;
+struct s_mc_message_register_symbol {
+ e_mc_message_type type;
+ char name[128];
+ int (*callback)(void*);
+ void* data;
+};
+typedef struct s_mc_message_register_symbol s_mc_message_register_symbol_t;
+
+/* Server -> client */
struct s_mc_message_simcall_handle {
e_mc_message_type type;
unsigned long pid;
};
typedef struct s_mc_message_simcall_handle s_mc_message_simcall_handle_t;
-struct s_mc_register_symbol_message {
- e_mc_message_type type;
- char name[128];
- int (*callback)(void*);
- void* data;
-};
-typedef struct s_mc_register_symbol_message s_mc_register_symbol_message_t;
-
struct s_mc_message_restore {
e_mc_message_type type;
int index;