From 645bb55622428841aae7d922a783cc10eb1f9c81 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 16 May 2018 18:35:59 +0200
Subject: [PATCH] bin: factor exception-handling code

* bin/common_setup.cc, bin/common_setup.hh: Define a protected_main()
function that deal with exceptions.
* bin/autcross.cc, bin/autfilt.cc, bin/dstar2tgba.cc, bin/genaut.cc,
bin/genltl.cc, bin/ltl2tgba.cc, bin/ltl2tgta.cc, bin/ltlcross.cc,
bin/ltldo.cc, bin/ltlfilt.cc, bin/ltlgrind.cc, bin/ltlsynt.cc,
bin/randaut.cc, bin/randltl.cc: Use it for all tools.
---
 bin/autcross.cc     | 146 +++++++++++++++++------------------
 bin/autfilt.cc      |  27 ++-----
 bin/common_setup.cc |  20 +++++
 bin/common_setup.hh |   9 ++-
 bin/dstar2tgba.cc   |  35 ++++-----
 bin/genaut.cc       |  37 ++++-----
 bin/genltl.cc       |  30 +++-----
 bin/ltl2tgba.cc     |  30 +++-----
 bin/ltl2tgta.cc     |  28 +++----
 bin/ltlcross.cc     | 181 ++++++++++++++++++++++----------------------
 bin/ltldo.cc        |  47 +++++-------
 bin/ltlfilt.cc      |  32 +++-----
 bin/ltlgrind.cc     |  28 +++----
 bin/ltlsynt.cc      |  19 ++---
 bin/randaut.cc      |  21 ++---
 bin/randltl.cc      |  24 ++----
 16 files changed, 328 insertions(+), 386 deletions(-)

diff --git a/bin/autcross.cc b/bin/autcross.cc
index e7defaa89..8aaf2822c 100644
--- a/bin/autcross.cc
+++ b/bin/autcross.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement de
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement de
 // l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -822,97 +822,97 @@ print_stats_csv(const char* filename)
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&]() -> unsigned {
+      const argp ap = { options, parse_opt, "[COMMANDFMT...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[COMMANDFMT...]",
-                    argp_program_doc, children, nullptr, nullptr };
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      check_no_automaton();
 
-  check_no_automaton();
+      auto s = tools.size();
+      if (s == 0)
+        error(2, 0, "No tool to run?  Run '%s --help' for usage.",
+              program_name);
 
-  auto s = tools.size();
-  if (s == 0)
-    error(2, 0, "No tool to run?  Run '%s --help' for usage.",
-          program_name);
-
-  if (s == 1 && !opt_language_preserved && !no_checks)
-    error(2, 0, "Since --language-preserved is not used, you need "
-          "at least two tools to compare.");
+      if (s == 1 && !opt_language_preserved && !no_checks)
+        error(2, 0, "Since --language-preserved is not used, you need "
+              "at least two tools to compare.");
 
 
-  setup_color();
-  setup_sig_handler();
+      setup_color();
+      setup_sig_handler();
 
-  autcross_processor p;
-  if (p.run())
-    return 2;
+      autcross_processor p;
+      if (p.run())
+        return 2;
 
-  if (round_num == 0)
-    {
-      error(2, 0, "no automaton to translate");
-    }
-  else
-    {
-      if (global_error_flag)
+      if (round_num == 0)
         {
-          std::ostream& err = global_error();
-          if (bogus_output)
-            err << ("error: some error was detected during the above runs.\n"
-                    "       Check file ")
-                << bogus_output_filename
-                << " for problematic automata.";
-          else
-            err << ("error: some error was detected during the above runs,\n"
-                    "       please search for 'error:' messages in the above"
-                    " trace.");
-          err << std::endl;
-          end_error();
-        }
-      else if (timeout_count == 0 && ignored_exec_fail == 0)
-        {
-          std::cerr << "No problem detected." << std::endl;
+          error(2, 0, "no automaton to translate");
         }
       else
         {
-          std::cerr << "No major problem detected." << std::endl;
-        }
-
-      unsigned additional_errors = 0U;
-      additional_errors += timeout_count > 0;
-      additional_errors += ignored_exec_fail > 0;
-      if (additional_errors)
-        {
-          std::cerr << (global_error_flag ? "Additionally, " : "However, ");
-          if (timeout_count)
+          if (global_error_flag)
             {
-              if (additional_errors > 1)
-                std::cerr << "\n  - ";
-              if (timeout_count == 1)
-                std::cerr << "1 timeout occurred";
+              std::ostream& err = global_error();
+              if (bogus_output)
+                err << ("error: some error was detected during the above "
+                        "runs.\n       Check file ")
+                    << bogus_output_filename
+                    << " for problematic automata.";
               else
-                std::cerr << timeout_count << " timeouts occurred";
+                err << ("error: some error was detected during the above "
+                        "runs,\n       please search for 'error:' messages"
+                        " in the above trace.");
+              err << std::endl;
+              end_error();
+            }
+          else if (timeout_count == 0 && ignored_exec_fail == 0)
+            {
+              std::cerr << "No problem detected." << std::endl;
+            }
+          else
+            {
+              std::cerr << "No major problem detected." << std::endl;
             }
 
-          if (ignored_exec_fail)
+          unsigned additional_errors = 0U;
+          additional_errors += timeout_count > 0;
+          additional_errors += ignored_exec_fail > 0;
+          if (additional_errors)
             {
-              if (additional_errors > 1)
-                std::cerr << "\n  - ";
-              if (ignored_exec_fail == 1)
-                std::cerr << "1 non-zero exit status was ignored";
-              else
-                std::cerr << ignored_exec_fail
-                          << " non-zero exit statuses were ignored";
+              std::cerr << (global_error_flag ? "Additionally, " : "However, ");
+              if (timeout_count)
+                {
+                  if (additional_errors > 1)
+                    std::cerr << "\n  - ";
+                  if (timeout_count == 1)
+                    std::cerr << "1 timeout occurred";
+                  else
+                    std::cerr << timeout_count << " timeouts occurred";
+                }
+
+              if (ignored_exec_fail)
+                {
+                  if (additional_errors > 1)
+                    std::cerr << "\n  - ";
+                  if (ignored_exec_fail == 1)
+                    std::cerr << "1 non-zero exit status was ignored";
+                  else
+                    std::cerr << ignored_exec_fail
+                              << " non-zero exit statuses were ignored";
+                }
+              if (additional_errors == 1)
+                std::cerr << '.';
+              std::cerr << std::endl;
             }
-          if (additional_errors == 1)
-            std::cerr << '.';
-          std::cerr << std::endl;
         }
-    }
 
-  if (csv_output)
-    print_stats_csv(csv_output);
+      if (csv_output)
+        print_stats_csv(csv_output);
 
-  return global_error_flag;
+      return global_error_flag;
+    });
 }
diff --git a/bin/autfilt.cc b/bin/autfilt.cc
index cff6829c6..2f376afac 100644
--- a/bin/autfilt.cc
+++ b/bin/autfilt.cc
@@ -1496,13 +1496,10 @@ namespace
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
-                    argp_program_doc, children, nullptr, nullptr };
-
-  try
-    {
       // This will ensure that all objects stored in this struct are
       // destroyed before global variables.
       opt_t o;
@@ -1544,19 +1541,11 @@ main(int argc, char** argv)
 
       // Diagnose unused -x options
       extra_options.report_unused_options();
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-  catch (const std::invalid_argument& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
 
-  if (automaton_format == Count)
-    std::cout << match_count << std::endl;
+      if (automaton_format == Count)
+        std::cout << match_count << std::endl;
 
-  check_cout();
-  return !match_count;
+      check_cout();
+      return match_count ? 0 : 1;
+    });
 }
diff --git a/bin/common_setup.cc b/bin/common_setup.cc
index cb953b9ee..6b04be48c 100644
--- a/bin/common_setup.cc
+++ b/bin/common_setup.cc
@@ -169,3 +169,23 @@ const struct argp misc_argp = { options, parse_opt_misc,
 const struct argp misc_argp_hidden = { options_hidden, parse_opt_misc,
                                        nullptr, nullptr, nullptr,
                                        nullptr, nullptr };
+
+
+int protected_main(char** progname, std::function<int()> mainfun)
+{
+  try
+    {
+      setup(progname);
+      return mainfun();
+    }
+  catch (const std::runtime_error& e)
+    {
+      error(2, 0, "%s", e.what());
+    }
+  catch (const std::invalid_argument& e)
+    {
+      error(2, 0, "%s", e.what());
+    }
+  SPOT_UNREACHABLE();
+  return 2;
+}
diff --git a/bin/common_setup.hh b/bin/common_setup.hh
index e8d3ae5ac..41f4a71a2 100644
--- a/bin/common_setup.hh
+++ b/bin/common_setup.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2018 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -21,8 +21,13 @@
 
 #include "common_sys.hh"
 #include "progname.h"
+#include <functional>
 
 void setup(char** progname);
 
 extern const struct argp misc_argp;
 extern const struct argp misc_argp_hidden;
+
+
+// Call setup(progname) then Run mainfun() and handle exceptions.
+int protected_main(char** progname, std::function<int()> mainfun);
diff --git a/bin/dstar2tgba.cc b/bin/dstar2tgba.cc
index 344cddb81..1abe45f23 100644
--- a/bin/dstar2tgba.cc
+++ b/bin/dstar2tgba.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2013-2018 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -136,33 +136,26 @@ namespace
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
-                    argp_program_doc, children, nullptr, nullptr };
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      check_no_automaton();
 
-  check_no_automaton();
+      spot::postprocessor post(&extra_options);
+      post.set_pref(pref | comp | sbacc | colored);
+      post.set_type(type);
+      post.set_level(level);
 
-  spot::postprocessor post(&extra_options);
-  post.set_pref(pref | comp | sbacc | colored);
-  post.set_type(type);
-  post.set_level(level);
-
-  try
-    {
       dstar_processor processor(post);
       if (processor.run())
         return 2;
 
       // Diagnose unused -x options
       extra_options.report_unused_options();
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-  return 0;
+      return 0;
+    });
 }
diff --git a/bin/genaut.cc b/bin/genaut.cc
index fca03f540..d76f25b51 100644
--- a/bin/genaut.cc
+++ b/bin/genaut.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -134,29 +134,22 @@ run_jobs()
 int
 main(int argc, char** argv)
 {
-  strcpy(F_doc, "the name of the pattern");
-  strcpy(L_doc, "the argument of the pattern");
-  setup(argv);
+  return protected_main(argv, [&] {
+      strcpy(F_doc, "the name of the pattern");
+      strcpy(L_doc, "the argument of the pattern");
 
-  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
-                    children, nullptr, nullptr };
+      const argp ap = { options, parse_opt, nullptr, argp_program_doc,
+                        children, nullptr, nullptr };
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (jobs.empty())
-    error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
-          program_name);
+      if (jobs.empty())
+        error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
+              program_name);
 
-  try
-    {
       run_jobs();
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-
-  flush_cout();
-  return 0;
+      flush_cout();
+      return 0;
+    });
 }
diff --git a/bin/genltl.cc b/bin/genltl.cc
index 4c37356bd..169b7fbcb 100644
--- a/bin/genltl.cc
+++ b/bin/genltl.cc
@@ -286,27 +286,19 @@ run_jobs()
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, nullptr, argp_program_doc,
+                        children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, nullptr, argp_program_doc,
-                    children, nullptr, nullptr };
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      if (jobs.empty())
+        error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
+              program_name);
 
-  if (jobs.empty())
-    error(1, 0, "Nothing to do.  Try '%s --help' for more information.",
-          program_name);
-
-  try
-    {
       run_jobs();
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-
-  flush_cout();
-  return 0;
+      flush_cout();
+      return 0;
+    });
 }
diff --git a/bin/ltl2tgba.cc b/bin/ltl2tgba.cc
index 073d67150..153bad322 100644
--- a/bin/ltl2tgba.cc
+++ b/bin/ltl2tgba.cc
@@ -158,23 +158,20 @@ namespace
 int
 main(int argc, char** argv)
 {
-  // By default we name automata using the formula.
-  opt_name = "%f";
+  return protected_main(argv, [&] {
+      // By default we name automata using the formula.
+      opt_name = "%f";
 
-  setup(argv);
+      const argp ap = { options, parse_opt, "[FORMULA...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[FORMULA...]",
-                    argp_program_doc, children, nullptr, nullptr };
+      simplification_level = 3;
 
-  simplification_level = 3;
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      check_no_formula();
 
-  check_no_formula();
-
-  try
-    {
       spot::translator trans(&extra_options);
       trans.set_type(type);
       trans.set_pref(pref | comp | sbacc | unambig | colored);
@@ -186,11 +183,6 @@ main(int argc, char** argv)
 
       // Diagnose unused -x options
       extra_options.report_unused_options();
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-
-  return 0;
+      return 0;
+    });
 }
diff --git a/bin/ltl2tgta.cc b/bin/ltl2tgta.cc
index 3c61926c2..717100fb8 100644
--- a/bin/ltl2tgta.cc
+++ b/bin/ltl2tgta.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012-2017 Laboratoire de Recherche et Développement
+// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -224,20 +224,17 @@ namespace
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[FORMULA...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[FORMULA...]",
-                    argp_program_doc, children, nullptr, nullptr };
+      simplification_level = 3;
 
-  simplification_level = 3;
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      check_no_formula();
 
-  check_no_formula();
-
-  try
-    {
       spot::translator trans(&extra_options);
       trans.set_pref(pref | comp | sbacc);
       trans.set_type(type);
@@ -248,11 +245,6 @@ main(int argc, char** argv)
         return 2;
       // Diagnose unused -x options
       extra_options.report_unused_options();
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-
-  return 0;
+      return 0;
+    });
 }
diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc
index 9569694e6..c5591d0f4 100644
--- a/bin/ltlcross.cc
+++ b/bin/ltlcross.cc
@@ -1591,108 +1591,109 @@ print_stats_json(const char* filename)
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&]() -> unsigned {
+      const argp ap = { options, parse_opt, "[COMMANDFMT...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[COMMANDFMT...]",
-                    argp_program_doc, children, nullptr, nullptr };
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      check_no_formula();
 
-  check_no_formula();
+      if (tools.empty())
+        error(2, 0, "No translator to run?  Run '%s --help' for usage.",
+              program_name);
 
-  if (tools.empty())
-    error(2, 0, "No translator to run?  Run '%s --help' for usage.",
-          program_name);
+      setup_color();
+      setup_sig_handler();
 
-  setup_color();
-  setup_sig_handler();
+      processor p;
+      if (p.run())
+        return 2;
 
-  processor p;
-  if (p.run())
-    return 2;
-
-  if (formulas.empty())
-    {
-      error(2, 0, "no formula to translate");
-    }
-  else
-    {
-      if (global_error_flag)
+      if (formulas.empty())
         {
-          std::ostream& err = global_error();
-          if (bogus_output)
-            err << ("error: some error was detected during the above runs.\n"
-                    "       Check file ")
-                << bogus_output_filename
-                << " for problematic formulas.";
-          else
-            err << ("error: some error was detected during the above runs,\n"
-                    "       please search for 'error:' messages in the above"
-                    " trace.");
-          err << std::endl;
-          end_error();
-        }
-      else if (timeout_count == 0 && ignored_exec_fail == 0 && oom_count == 0)
-        {
-          std::cerr << "No problem detected." << std::endl;
+          error(2, 0, "no formula to translate");
         }
       else
         {
-          std::cerr << "No major problem detected." << std::endl;
+          if (global_error_flag)
+            {
+              std::ostream& err = global_error();
+              if (bogus_output)
+                err << ("error: some error was detected during the above "
+                        "runs.\n       Check file ")
+                    << bogus_output_filename
+                    << " for problematic formulas.";
+              else
+                err << ("error: some error was detected during the above "
+                        "runs,\n       please search for 'error:' messages"
+                        " in the above trace.");
+              err << std::endl;
+              end_error();
+            }
+          else if (timeout_count == 0
+                   && ignored_exec_fail == 0 && oom_count == 0)
+            {
+              std::cerr << "No problem detected." << std::endl;
+            }
+          else
+            {
+              std::cerr << "No major problem detected." << std::endl;
+            }
+
+          unsigned additional_errors = 0U;
+          additional_errors += timeout_count > 0;
+          additional_errors += ignored_exec_fail > 0;
+          additional_errors += oom_count > 0;
+          if (additional_errors)
+            {
+              std::cerr << (global_error_flag ? "Additionally, " : "However, ");
+              if (timeout_count)
+                {
+                  if (additional_errors > 1)
+                    std::cerr << "\n  - ";
+                  if (timeout_count == 1)
+                    std::cerr << "1 timeout occurred";
+                  else
+                    std::cerr << timeout_count << " timeouts occurred";
+                }
+
+              if (oom_count)
+                {
+                  if (additional_errors > 1)
+                    std::cerr << "\n  - ";
+                  if (oom_count == 1)
+                    std::cerr << "1 state-space product was";
+                  else
+                    std::cerr << oom_count << "state-space products were";
+                  std::cerr << " skipped by lack of memory";
+                }
+
+              if (ignored_exec_fail)
+                {
+                  if (additional_errors > 1)
+                    std::cerr << "\n  - ";
+                  if (ignored_exec_fail == 1)
+                    std::cerr << "1 non-zero exit status was ignored";
+                  else
+                    std::cerr << ignored_exec_fail
+                              << " non-zero exit statuses were ignored";
+                }
+              if (additional_errors == 1)
+                std::cerr << '.';
+              std::cerr << std::endl;
+            }
         }
 
-      unsigned additional_errors = 0U;
-      additional_errors += timeout_count > 0;
-      additional_errors += ignored_exec_fail > 0;
-      additional_errors += oom_count > 0;
-      if (additional_errors)
-        {
-          std::cerr << (global_error_flag ? "Additionally, " : "However, ");
-          if (timeout_count)
-            {
-              if (additional_errors > 1)
-                std::cerr << "\n  - ";
-              if (timeout_count == 1)
-                std::cerr << "1 timeout occurred";
-              else
-                std::cerr << timeout_count << " timeouts occurred";
-            }
+      delete bogus_output;
+      delete grind_output;
 
-          if (oom_count)
-            {
-              if (additional_errors > 1)
-                std::cerr << "\n  - ";
-              if (oom_count == 1)
-                std::cerr << "1 state-space product was";
-              else
-                std::cerr << oom_count << "state-space products were";
-              std::cerr << " skipped by lack of memory";
-            }
+      if (json_output)
+        print_stats_json(json_output);
+      if (csv_output)
+        print_stats_csv(csv_output);
 
-          if (ignored_exec_fail)
-            {
-              if (additional_errors > 1)
-                std::cerr << "\n  - ";
-              if (ignored_exec_fail == 1)
-                std::cerr << "1 non-zero exit status was ignored";
-              else
-                std::cerr << ignored_exec_fail
-                          << " non-zero exit statuses were ignored";
-            }
-          if (additional_errors == 1)
-            std::cerr << '.';
-          std::cerr << std::endl;
-        }
-    }
-
-  delete bogus_output;
-  delete grind_output;
-
-  if (json_output)
-    print_stats_json(json_output);
-  if (csv_output)
-    print_stats_csv(csv_output);
-
-  return global_error_flag;
+      return global_error_flag;
+    });
 }
diff --git a/bin/ltldo.cc b/bin/ltldo.cc
index 3cf1730d6..d63e4e4ce 100644
--- a/bin/ltldo.cc
+++ b/bin/ltldo.cc
@@ -445,40 +445,33 @@ namespace
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[COMMANDFMT...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[COMMANDFMT...]",
-                    argp_program_doc, children, nullptr, nullptr };
+      // Disable post-processing as much as possible by default.
+      level = spot::postprocessor::Low;
+      pref = spot::postprocessor::Any;
+      type = spot::postprocessor::Generic;
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  // Disable post-processing as much as possible by default.
-  level = spot::postprocessor::Low;
-  pref = spot::postprocessor::Any;
-  type = spot::postprocessor::Generic;
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      check_no_formula();
 
-  check_no_formula();
+      if (tools.empty())
+        error(2, 0, "No translator to run?  Run '%s --help' for usage.",
+              program_name);
 
-  if (tools.empty())
-    error(2, 0, "No translator to run?  Run '%s --help' for usage.",
-          program_name);
+      setup_sig_handler();
 
-  setup_sig_handler();
+      spot::postprocessor post;
+      post.set_pref(pref | comp | sbacc | colored);
+      post.set_type(type);
+      post.set_level(level);
 
-  spot::postprocessor post;
-  post.set_pref(pref | comp | sbacc | colored);
-  post.set_type(type);
-  post.set_level(level);
-
-  try
-    {
       processor p(post);
       if (p.run())
         return 2;
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-  return 0;
+      return 0;
+    });
 }
diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc
index 4df6d1f96..127fc511e 100644
--- a/bin/ltlfilt.cc
+++ b/bin/ltlfilt.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2017 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2012-2018 Laboratoire de Recherche et Développement
+// de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -795,13 +795,10 @@ namespace
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
-                    argp_program_doc, children, nullptr, nullptr };
-
-  try
-    {
       // This will ensure that all objects stored in this struct are
       // destroyed before global variables.
       opt_t o;
@@ -822,19 +819,10 @@ main(int argc, char** argv)
       ltl_processor processor(simpl);
       if (processor.run())
         return 2;
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-  catch (const std::invalid_argument& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
 
-  if (output_format == count_output)
-    std::cout << match_count << std::endl;
-  flush_cout();
-
-  return one_match ? 0 : 1;
+      if (output_format == count_output)
+        std::cout << match_count << '\n';
+      flush_cout();
+      return one_match ? 0 : 1;
+    });
 }
diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc
index 10cc6e24a..e6f9a2f75 100644
--- a/bin/ltlgrind.cc
+++ b/bin/ltlgrind.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et
+// Copyright (C) 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -183,21 +183,21 @@ parse_opt(int key, char* arg, struct argp_state*)
 int
 main(int argc, char* argv[])
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "[FILENAME[/COL]...]",
+                        argp_program_doc, children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "[FILENAME[/COL]...]", argp_program_doc,
-                    children, nullptr, nullptr };
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
 
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
+      mut_opts |= opt_all;
 
-  mut_opts |= opt_all;
+      check_no_formula();
 
-  check_no_formula();
-
-  mutate_processor processor;
-  if (processor.run())
-    return 2;
-  flush_cout();
-  return 0;
+      mutate_processor processor;
+      if (processor.run())
+        return 2;
+      flush_cout();
+      return 0;
+    });
 }
diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index 910bca39c..e04e71a73 100644
--- a/bin/ltlsynt.cc
+++ b/bin/ltlsynt.cc
@@ -416,14 +416,15 @@ parse_opt(int key, char* arg, struct argp_state*)
 int
 main(int argc, char **argv)
 {
-  setup(argv);
-  const argp ap = { options, parse_opt, nullptr,
-                    argp_program_doc, children, nullptr, nullptr };
-  if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
-    exit(err);
-  check_no_formula();
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, nullptr,
+                        argp_program_doc, children, nullptr, nullptr };
+      if (int err = argp_parse(&ap, argc, argv, ARGP_NO_HELP, nullptr, nullptr))
+        exit(err);
+      check_no_formula();
 
-  spot::translator trans;
-  ltl_processor processor(trans, input_aps, output_aps);
-  return processor.run();
+      spot::translator trans;
+      ltl_processor processor(trans, input_aps, output_aps);
+      return processor.run();
+    });
 }
diff --git a/bin/randaut.cc b/bin/randaut.cc
index 38b9e8b5b..eeca8a26e 100644
--- a/bin/randaut.cc
+++ b/bin/randaut.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -276,15 +276,13 @@ parse_opt(int key, char* arg, struct argp_state* as)
 int
 main(int argc, char** argv)
 {
-  strcpy(F_doc, "seed number");
-  strcpy(L_doc, "automaton number");
-  setup(argv);
+  return protected_main(argv, [&] {
+      strcpy(F_doc, "seed number");
+      strcpy(L_doc, "automaton number");
 
-  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
-                    children, nullptr, nullptr };
+      const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
+                        children, nullptr, nullptr };
 
-  try
-    {
       // This will ensure that all objects stored in this struct are
       // destroyed before global variables.
       opt_t o;
@@ -404,9 +402,6 @@ main(int argc, char** argv)
           if (opt_automata > 0 && automaton_num >= opt_automata)
             break;
         }
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
+      return 0;
+    });
 }
diff --git a/bin/randltl.cc b/bin/randltl.cc
index b364e434f..042d9fa74 100644
--- a/bin/randltl.cc
+++ b/bin/randltl.cc
@@ -236,13 +236,10 @@ parse_opt(int key, char* arg, struct argp_state* as)
 int
 main(int argc, char** argv)
 {
-  setup(argv);
+  return protected_main(argv, [&] {
+      const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
+                        children, nullptr, nullptr };
 
-  const argp ap = { options, parse_opt, "N|PROP...", argp_program_doc,
-                    children, nullptr, nullptr };
-
-  try
-    {
       // This will ensure that all objects stored in this struct are
       // destroyed before global variables.
       opt_t o;
@@ -319,16 +316,7 @@ main(int argc, char** argv)
               output_formula_checked(f, nullptr, nullptr, ++count);
             }
         };
-    }
-  catch (const std::runtime_error& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-  catch (const std::invalid_argument& e)
-    {
-      error(2, 0, "%s", e.what());
-    }
-
-  flush_cout();
-  return 0;
+      flush_cout();
+      return 0;
+    });
 }