use ebmc_languaget API in ebmc_parse_optionst

This replaces the direct call to get_transition_system(...) by a call to an
implementation of ebmc_languaget, which wraps get_transition_system.

Author: kroening

src/ebmc/ebmc_language.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #define EBMC_LANGUAGE_H
 
 #include <iosfwd>
+#include <optional>
 
 class cmdlinet;
 class message_handlert;
@@ -29,11 +30,9 @@ class ebmc_languaget
 
   virtual ~ebmc_languaget();
 
-  /// produce diagnostic output as specified on the command line
-  virtual void diagnostics() = 0;
-
-  /// produce the transition system, and return it
-  virtual transition_systemt transition_system() = 0;
+  /// Produce the transition system, and return it;
+  /// returns {} when diagnostic output was produced instead.
+  virtual std::optional<transition_systemt> transition_system() = 0;
 
 protected:
   cmdlinet &cmdline;

src/ebmc/ebmc_parse_options.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "diatest.h"
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "ebmc_language.h"
 #include "ebmc_version.h"
 #include "format_hooks.h"
 #include "instrument_buechi.h"
@@ -46,6 +47,52 @@ Author: Daniel Kroening, [email protected]
 #include "coverage/coverage.h"
 #endif
 
+class ebmc_languagest : public ebmc_languaget
+{
+public:
+  ebmc_languagest(cmdlinet &_cmdline, message_handlert &_message_handler)
+    : ebmc_languaget{_cmdline, _message_handler}
+  {
+  }
+
+  std::optional<transition_systemt> transition_system() override
+  {
+    if(cmdline.isset("preprocess"))
+    {
+      preprocess(cmdline, message_handler);
+      return {};
+    }
+
+    if(cmdline.isset("show-parse"))
+    {
+      show_parse(cmdline, message_handler);
+      return {};
+    }
+
+    if(
+      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
+      cmdline.isset("json-modules"))
+    {
+      show_modules(cmdline, message_handler);
+      return {};
+    }
+
+    if(cmdline.isset("show-module-hierarchy"))
+    {
+      show_module_hierarchy(cmdline, message_handler);
+      return {};
+    }
+
+    if(cmdline.isset("show-symbol-table"))
+    {
+      show_symbol_table(cmdline, message_handler);
+      return {};
+    }
+
+    return get_transition_system(cmdline, message_handler);
+  }
+};
+
 /*******************************************************************\
 
 Function: ebmc_parse_optionst::doit
@@ -107,23 +154,6 @@ int ebmc_parse_optionst::doit()
       return 0;
     }
 
-    if(cmdline.isset("preprocess"))
-      return preprocess(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-parse"))
-      return show_parse(cmdline, ui_message_handler);
-
-    if(
-      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-      cmdline.isset("json-modules"))
-      return show_modules(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-module-hierarchy"))
-      return show_module_hierarchy(cmdline, ui_message_handler);
-
-    if(cmdline.isset("show-symbol-table"))
-      return show_symbol_table(cmdline, ui_message_handler);
-
     if(cmdline.isset("coverage"))
     {
       throw ebmc_errort() << "This option is currently disabled";
@@ -207,7 +237,15 @@ int ebmc_parse_optionst::doit()
     }
 
     // get the transition system
-    auto transition_system = get_transition_system(cmdline, ui_message_handler);
+    ebmc_languagest ebmc_languages{cmdline, ui_message_handler};
+
+    auto transition_system_opt = ebmc_languages.transition_system();
+
+    // Did we produce diagnostics instead?
+    if(!transition_system_opt.has_value())
+      return 0;
+
+    auto &transition_system = transition_system_opt.value();
 
     // get the properties
     auto properties = ebmc_propertiest::from_command_line(