static simgrid::config::Flag<std::string> cfg_dot_output_file{
"model-check/dot-output", "Name of dot output file corresponding to graph state", ""};
-Exploration::Exploration(const std::vector<char*>& args) : remote_app_(std::make_unique<RemoteApp>(args))
+Exploration* Exploration::instance_ = nullptr; // singleton instance
+
+Exploration::Exploration(const std::vector<char*>& args, bool need_memory_introspection)
+ : remote_app_(std::make_unique<RemoteApp>(args, need_memory_introspection))
{
- mc_model_checker->set_exploration(this);
+ xbt_assert(instance_ == nullptr, "Cannot have more than one exploration instance");
+ instance_ = this;
if (not cfg_dot_output_file.get().empty()) {
dot_output_ = fopen(cfg_dot_output_file.get().c_str(), "w");
{
if (dot_output_ != nullptr)
fclose(dot_output_);
+ instance_ = nullptr;
}
void Exploration::dot_output(const char* fmt, ...)
}
}
-void Exploration::report_crash(int status)
+XBT_ATTRIB_NORETURN void Exploration::report_crash(int status)
{
XBT_INFO("**************************");
XBT_INFO("** CRASH IN THE PROGRAM **");
if (xbt_log_no_loc) {
XBT_INFO("Stack trace not displayed because you passed --log=no_loc");
} else {
- XBT_INFO("Stack trace:");
- get_remote_app().get_remote_process_memory().dump_stack();
+ const auto* memory = get_remote_app().get_remote_process_memory();
+ if (memory) {
+ XBT_INFO("Stack trace:");
+ memory->dump_stack();
+ } else {
+ XBT_INFO("Stack trace not shown because there is no memory introspection.");
+ }
}
- get_remote_app().get_remote_process_memory().terminate();
system_exit(SIMGRID_MC_EXIT_PROGRAM_CRASH);
}
-void Exploration::report_assertion_failure()
+XBT_ATTRIB_NORETURN void Exploration::report_assertion_failure()
{
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
system_exit(SIMGRID_MC_EXIT_SAFETY);
}
-void Exploration::system_exit(int status)
+void Exploration::system_exit(int status) const
{
- get_remote_app().shutdown();
::exit(status);
}