X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a36e8044de323971221f5da46773d54e312d3b3c..1e83888c1aed0b9146b5ae78ad474f374d28a769:/src/mc/ModelChecker.cpp?ds=sidebyside diff --git a/src/mc/ModelChecker.cpp b/src/mc/ModelChecker.cpp index af0c6668cb..2f443048fe 100644 --- a/src/mc/ModelChecker.cpp +++ b/src/mc/ModelChecker.cpp @@ -14,23 +14,22 @@ #include #include -#include -#include -#include -#include +#include "xbt/automaton.h" +#include "xbt/automaton.hpp" +#include "xbt/log.h" +#include "xbt/system_error.hpp" #include "simgrid/sg_config.h" #include "src/mc/ModelChecker.hpp" -#include "src/mc/PageStore.hpp" #include "src/mc/ModelChecker.hpp" -#include "src/mc/mc_protocol.h" -#include "src/mc/mc_private.h" -#include "src/mc/mc_ignore.h" +#include "src/mc/PageStore.hpp" +#include "src/mc/Transition.hpp" +#include "src/mc/checker/Checker.hpp" #include "src/mc/mc_exit.h" +#include "src/mc/mc_private.h" #include "src/mc/mc_record.h" -#include "src/mc/Transition.hpp" -#include "src/mc/Checker.hpp" +#include "src/mc/remote/mc_protocol.h" XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_ModelChecker, mc, "ModelChecker"); @@ -92,7 +91,7 @@ void ModelChecker::start() // The model-checked process SIGSTOP itself to signal it's ready: pid_t res = waitpid(pid, &status, WAITPID_CHECKED_FLAGS); - if (res < 0 || !WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) + if (res < 0 || not WIFSTOPPED(status) || WSTOPSIG(status) != SIGSTOP) xbt_die("Could not wait model-checked process"); process_->init(); @@ -161,16 +160,6 @@ void ModelChecker::resume(simgrid::mc::Process& process) process.clear_cache(); } -static -void throw_socket_error(int fd) -{ - int error = 0; - socklen_t errlen = sizeof(error); - if (getsockopt(fd, SOL_SOCKET, SO_ERROR, (void *)&error, &errlen) == -1) - error = errno; - throw simgrid::xbt::errno_error(); -} - static void MC_report_crash(int status) { XBT_INFO("**************************"); @@ -193,7 +182,7 @@ static void MC_report_crash(int status) mc_model_checker->process().dumpStack(); } -static void MC_report_assertion_error(void) +static void MC_report_assertion_error() { XBT_INFO("**************************"); XBT_INFO("*** PROPERTY NOT VALID ***"); @@ -316,7 +305,7 @@ void ModelChecker::handle_events(int fd, short events) ssize_t size = process_->getChannel().receive(buffer, sizeof(buffer), false); if (size == -1 && errno != EAGAIN) throw simgrid::xbt::errno_error(); - if (!handle_message(buffer, size)) { + if (not handle_message(buffer, size)) { event_base_loopbreak(base_); } }