simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo) const
{
- auto session = new simgrid::mc::Session([argv] {
+ simgrid::mc::session_singleton = std::make_unique<simgrid::mc::Session>([argv] {
int i = 1;
while (argv[i] != nullptr && argv[i][0] == '-')
i++;
simgrid::mc::Exploration* explo;
switch (algo) {
case CheckerAlgorithm::CommDeterminism:
- explo = simgrid::mc::create_communication_determinism_checker(session);
+ explo = simgrid::mc::create_communication_determinism_checker(session_singleton.get());
break;
case CheckerAlgorithm::UDPOR:
- explo = simgrid::mc::create_udpor_checker(session);
+ explo = simgrid::mc::create_udpor_checker(session_singleton.get());
break;
case CheckerAlgorithm::Safety:
- explo = simgrid::mc::create_safety_checker(session);
+ explo = simgrid::mc::create_safety_checker(session_singleton.get());
break;
case CheckerAlgorithm::Liveness:
- explo = simgrid::mc::create_liveness_checker(session);
+ explo = simgrid::mc::create_liveness_checker(session_singleton.get());
break;
default:
THROW_IMPOSSIBLE;
}
- // FIXME: session and checker are never deleted
- simgrid::mc::session_singleton = session;
mc_model_checker->set_exploration(explo);
return explo;
}
void Api::s_close() const
{
session_singleton->close();
+ session_singleton.reset();
if (simgrid::mc::property_automaton != nullptr) {
xbt_automaton_free(simgrid::mc::property_automaton);
simgrid::mc::property_automaton = nullptr;
algo = simgrid::mc::CheckerAlgorithm::Liveness;
int res = SIMGRID_MC_EXIT_SUCCESS;
- auto checker = api::get().initialize(argv_copy.data(), algo);
+ std::unique_ptr<simgrid::mc::Exploration> checker{api::get().initialize(argv_copy.data(), algo)};
try {
checker->run();
} catch (const simgrid::mc::DeadlockError&) {
res = SIMGRID_MC_EXIT_LIVENESS;
}
api::get().s_close();
- // delete checker; SEGFAULT in liveness
+ checker.release(); // FIXME: this line should not exist, but it segfaults in liveness
return res;
}