X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/05c280c2e4f419cbeeb3d3d6456d991a70f1edcc..HEAD:/src/mc/checker/simgrid_mc.cpp diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp deleted file mode 100644 index e8c0ca82b2..0000000000 --- a/src/mc/checker/simgrid_mc.cpp +++ /dev/null @@ -1,81 +0,0 @@ -/* Copyright (c) 2015-2019. 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 "simgrid/sg_config.hpp" -#include "src/mc/checker/Checker.hpp" -#include "src/mc/mc_exit.hpp" - -#include -#include - -XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc"); - -static inline -char** argvdup(int argc, char** argv) -{ - char** 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) -{ - 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)); - else - return std::unique_ptr(simgrid::mc::createLivenessChecker(session)); -} - -int main(int argc, char** argv) -{ - using simgrid::mc::Session; - - 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; - } -}