+
+ XBT_ERROR("Could not run the model-checked program");
+ // This is the value used by system() and popen() in this case:
+ return 127;
+}
+
+static
+std::pair<pid_t, int> create_model_checked(char** argv)
+{
+ // Create a AF_LOCAL socketpair used for exchanging messages
+ // bewteen the model-checker process (ourselves) and the model-checked
+ // process:
+ int res;
+ int sockets[2];
+ res = socketpair(AF_LOCAL, SOCK_DGRAM | SOCK_CLOEXEC, 0, sockets);
+ if (res == -1)
+ throw new std::system_error(errno, std::generic_category(), "socketpair");
+
+ pid_t pid = do_fork([&] {
+ close(sockets[1]);
+ int res = exec_model_checked(sockets[0], argv);
+ XBT_DEBUG("Error in the child process creation");
+ exit(res);
+ });
+
+ // Parent (model-checker):
+ close(sockets[0]);
+ return std::make_pair(pid, sockets[1]);
+}
+
+static
+char** argvdup(int argc, char** argv)
+{
+ char** argv_copy = xbt_new(char*, argc+1);
+ std::memcpy(argv_copy, argv, sizeof(char*) * argc);
+ argv_copy[argc] = NULL;
+ return argv_copy;