X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/ff420e1906d916322427488153e45bf82d5c03dd..66013c251781d4c2e926377d2e492334aa6e47ea:/src/mc/checker/simgrid_mc.cpp diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp index a6e3159145..b304db5636 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/checker/simgrid_mc.cpp @@ -1,98 +1,77 @@ -/* Copyright (c) 2015-2018. The SimGrid Team. +/* Copyright (c) 2015-2020. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -#include - -#include -#include -#include - -#include - -#include - -#include - #include "simgrid/sg_config.hpp" -#include "src/xbt_modinter.h" - #include "src/mc/Session.hpp" #include "src/mc/checker/Checker.hpp" -#include "src/mc/mc_base.h" -#include "src/mc/mc_comm_pattern.hpp" +#include "src/mc/mc_config.hpp" #include "src/mc/mc_exit.hpp" -#include "src/mc/mc_private.hpp" -#include "src/mc/mc_safety.hpp" -#include "src/mc/remote/mc_protocol.h" +#include "src/internal_config.h" +#include "src/mc/mc_api.hpp" -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); +#if HAVE_SMPI +#include "smpi/smpi.h" +#endif + +#include +#include +#include + +using mcapi = simgrid::mc::mc_api; static inline char** argvdup(int argc, char** argv) { - char** argv_copy = new char*[argc + 1]; + auto* argv_copy = new char*[argc + 1]; std::memcpy(argv_copy, argv, sizeof(char*) * argc); argv_copy[argc] = nullptr; return argv_copy; } -static std::unique_ptr createChecker(simgrid::mc::Session& session) +static std::unique_ptr create_checker(simgrid::mc::Session& session) { if (_sg_mc_comms_determinism || _sg_mc_send_determinism) return std::unique_ptr(simgrid::mc::createCommunicationDeterminismChecker(session)); else if (_sg_mc_property_file.get().empty()) - return std::unique_ptr(simgrid::mc::createSafetyChecker(session)); + return std::unique_ptr(simgrid::mc::createSafetyChecker()); else - return std::unique_ptr(simgrid::mc::createLivenessChecker(session)); + return std::unique_ptr(simgrid::mc::createLivenessChecker()); } int main(int argc, char** argv) { - using simgrid::mc::Session; - + if (argc < 2) + xbt_die("Missing arguments.\n"); + + // Currently, we need this before sg_config_init: + _sg_do_model_check = 1; + + // The initialization function can touch argv. + // We make a copy of argv before modifying it in order to pass the original value to the model-checked application: + char** argv_copy = argvdup(argc, argv); + xbt_log_init(&argc, argv); +#if HAVE_SMPI + smpi_init_options(); // only performed once +#endif + sg_config_init(&argc, argv); + mcapi::get().initialize(argv_copy); + delete[] argv_copy; + + auto checker = create_checker(*simgrid::mc::session); + int res = SIMGRID_MC_EXIT_SUCCESS; try { - if (argc < 2) - xbt_die("Missing arguments.\n"); - - // Currently, we need this before sg_config_init: - _sg_do_model_check = 1; - - // The initialization function can touch argv. - // We make a copy of argv before modifying it in order to pass the original - // value to the model-checked: - char** argv_copy = argvdup(argc, argv); - xbt_log_init(&argc, argv); - sg_config_init(&argc, argv); - - std::unique_ptr session = - std::unique_ptr(Session::spawnvp(argv_copy[1], argv_copy+1)); - delete[] argv_copy; - - simgrid::mc::session = session.get(); - std::unique_ptr checker = createChecker(*session); - int res = SIMGRID_MC_EXIT_SUCCESS; - try { - checker->run(); - } catch (simgrid::mc::DeadlockError& de) { - res = SIMGRID_MC_EXIT_DEADLOCK; - } catch (simgrid::mc::TerminationError& te) { - res = SIMGRID_MC_EXIT_NON_TERMINATION; - } catch (simgrid::mc::LivenessError& le) { - res = SIMGRID_MC_EXIT_LIVENESS; - } - checker = nullptr; - session->close(); - return res; - } - catch(std::exception& e) { - XBT_ERROR("Exception: %s", e.what()); - return SIMGRID_MC_EXIT_ERROR; - } - catch(...) { - XBT_ERROR("Unknown exception"); - return SIMGRID_MC_EXIT_ERROR; + checker->run(); + } catch (const simgrid::mc::DeadlockError&) { + res = SIMGRID_MC_EXIT_DEADLOCK; + } catch (const simgrid::mc::TerminationError&) { + res = SIMGRID_MC_EXIT_NON_TERMINATION; + } catch (const simgrid::mc::LivenessError&) { + res = SIMGRID_MC_EXIT_LIVENESS; } + checker = nullptr; + mcapi::get().s_close(); + return res; }