X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/af72ee01a6a0c01b1a67dc3095f952fd8ab1dd42..5824e3e084f8021554e73ba26124bd5ed2933b59:/src/mc/checker/simgrid_mc.cpp diff --git a/src/mc/checker/simgrid_mc.cpp b/src/mc/checker/simgrid_mc.cpp index 455290e6a7..0cc4ffe173 100644 --- a/src/mc/checker/simgrid_mc.cpp +++ b/src/mc/checker/simgrid_mc.cpp @@ -1,4 +1,4 @@ -/* Copyright (c) 2015-2021. The SimGrid Team. +/* Copyright (c) 2015-2022. The SimGrid Team. * All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it @@ -29,22 +29,9 @@ char** argvdup(int argc, char** argv) return argv_copy; } -static std::unique_ptr create_checker() -{ - if (_sg_mc_comms_determinism || _sg_mc_send_determinism) - return std::unique_ptr(simgrid::mc::createCommunicationDeterminismChecker()); - else if (_sg_mc_unfolding_checker) - return std::unique_ptr(simgrid::mc::createUdporChecker()); - else if (_sg_mc_property_file.get().empty()) - return std::unique_ptr(simgrid::mc::createSafetyChecker()); - else - return std::unique_ptr(simgrid::mc::createLivenessChecker()); -} - int main(int argc, char** argv) { - if (argc < 2) - xbt_die("Missing arguments.\n"); + xbt_assert(argc >= 2, "Missing arguments"); // Currently, we need this before sg_config_init: _sg_do_model_check = 1; @@ -52,16 +39,25 @@ int main(int argc, char** argv) // 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); - api::get().initialize(argv_copy); - delete[] argv_copy; - auto checker = create_checker(); + simgrid::mc::CheckerAlgorithm algo; + if (_sg_mc_comms_determinism || _sg_mc_send_determinism) + algo = simgrid::mc::CheckerAlgorithm::CommDeterminism; + else if (_sg_mc_unfolding_checker) + algo = simgrid::mc::CheckerAlgorithm::UDPOR; + else if (_sg_mc_property_file.get().empty()) + algo = simgrid::mc::CheckerAlgorithm::Safety; + else + algo = simgrid::mc::CheckerAlgorithm::Liveness; + int res = SIMGRID_MC_EXIT_SUCCESS; + auto checker = api::get().initialize(argv_copy, algo); try { checker->run(); } catch (const simgrid::mc::DeadlockError&) { @@ -71,7 +67,8 @@ int main(int argc, char** argv) } catch (const simgrid::mc::LivenessError&) { res = SIMGRID_MC_EXIT_LIVENESS; } - checker = nullptr; api::get().s_close(); + delete[] argv_copy; + delete checker; return res; }