void ModelChecker::start()
{
- checker_side_.start(
- [](evutil_socket_t sig, short events, void* arg) { ((ModelChecker*)arg)->handle_events(sig, events); });
+ checker_side_.start([](evutil_socket_t sig, short events, void* arg) {
+ auto mc = static_cast<simgrid::mc::ModelChecker*>(arg);
+ if (events == EV_READ) {
+ char buffer[MC_MESSAGE_LENGTH];
+ ssize_t size = mc->checker_side_.get_channel().receive(buffer, sizeof(buffer), false);
+ if (size == -1 && errno != EAGAIN)
+ throw simgrid::xbt::errno_error();
+
+ if (not mc->handle_message(buffer, size))
+ mc->checker_side_.break_loop();
+ } else if (events == EV_SIGNAL) {
+ if (sig == SIGCHLD)
+ mc->handle_waitpid();
+ } else {
+ xbt_die("Unexpected event");
+ }
+ });
XBT_DEBUG("Waiting for the model-checked process");
int status;
void ModelChecker::setup_ignore()
{
- RemoteSimulation& process = this->get_remote_simulation();
+ const RemoteSimulation& process = this->get_remote_simulation();
for (std::pair<const char*, const char*> const& var :
ignored_local_variables)
process.ignore_local_variable(var.first, var.second);
void ModelChecker::shutdown()
{
- XBT_DEBUG("Shuting down model-checker");
+ XBT_DEBUG("Shutting down model-checker");
RemoteSimulation* process = &this->get_remote_simulation();
if (process->running()) {
case MC_MESSAGE_IGNORE_HEAP:
{
s_mc_message_ignore_heap_t message;
- xbt_assert(size == sizeof(message), "Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken message");
memcpy(&message, buffer, sizeof(message));
IgnoredHeapRegion region;
case MC_MESSAGE_UNIGNORE_HEAP:
{
s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken message");
memcpy(&message, buffer, sizeof(message));
get_remote_simulation().unignore_heap((void*)(std::uintptr_t)message.addr, message.size);
break;
case MC_MESSAGE_IGNORE_MEMORY:
{
s_mc_message_ignore_memory_t message;
- xbt_assert(size == sizeof(message), "Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken message");
memcpy(&message, buffer, sizeof(message));
this->get_remote_simulation().ignore_region(message.addr, message.size);
break;
case MC_MESSAGE_STACK_REGION:
{
s_mc_message_stack_region_t message;
- xbt_assert(size == sizeof(message), "Broken messsage");
+ xbt_assert(size == sizeof(message), "Broken message");
memcpy(&message, buffer, sizeof(message));
this->get_remote_simulation().stack_areas().push_back(message.stack_region);
}
::exit(status);
}
-void ModelChecker::handle_events(int sig, short events)
-{
- if (events == EV_READ) {
- char buffer[MC_MESSAGE_LENGTH];
- ssize_t size = checker_side_.get_channel().receive(buffer, sizeof(buffer), false);
- if (size == -1 && errno != EAGAIN)
- throw simgrid::xbt::errno_error();
-
- if (not handle_message(buffer, size))
- checker_side_.break_loop();
- }
- else if (events == EV_SIGNAL) {
- if (sig == SIGCHLD)
- this->handle_waitpid();
- }
- else {
- xbt_die("Unexpected event");
- }
-}
-
void ModelChecker::handle_waitpid()
{
XBT_DEBUG("Check for wait event");
#ifdef __linux__
ptrace(PTRACE_CONT, remote_simulation_->pid(), 0, WSTOPSIG(status));
#elif defined BSD
- ptrace(PT_CONTINUE, app_remote_mem_.pid(), (caddr_t)1, WSTOPSIG(status));
+ ptrace(PT_CONTINUE, remote_simulation_->pid(), (caddr_t)1, WSTOPSIG(status));
#endif
xbt_assert(errno == 0, "Could not PTRACE_CONT");
}