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/build_transition_system.cpp

@@ -30,36 +30,29 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <iostream>
 
-int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
+void preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
 {
   messaget message(message_handler);
 
   if(cmdline.args.size() != 1)
-  {
-    message.error() << "please give exactly one file to preprocess"
-                    << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort{}.with_exit_code(1)
+      << "please give exactly one file to preprocess";
 
   const auto &filename = cmdline.args.front();
   std::ifstream infile(widen_if_needed(filename));
 
   if(!infile)
-  {
-    message.error() << "failed to open input file `" << filename << "'"
-                    << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort{}.with_exit_code(1)
+      << "failed to open input file `" << filename << "'";
 
   auto language = get_language_from_filename(filename);
 
   if(language == nullptr)
   {
     source_locationt location;
     location.set_file(filename);
-    message.error().source_location = location;
-    message.error() << "failed to figure out type of file" << messaget::eom;
-    return 1;
+    throw ebmc_errort{}.with_location(location).with_exit_code(1)
+      << "failed to figure out type of file";
   }
 
   optionst options;
@@ -77,12 +70,7 @@ int preprocess(const cmdlinet &cmdline, message_handlert &message_handler)
   language->set_language_options(options, message_handler);
 
   if(language->preprocess(infile, filename, std::cout, message_handler))
-  {
-    message.error() << "PREPROCESSING FAILED" << messaget::eom;
-    return 1;
-  }
-
-  return 0;
+    throw ebmc_errort{}.with_exit_code(1) << "PREPROCESSING FAILED";
 }
 
 static bool parse(
@@ -211,9 +199,6 @@ int get_transition_system(
 {
   messaget message(message_handler);
 
-  if(cmdline.isset("preprocess"))
-    return preprocess(cmdline, message_handler);
-
   //
   // parsing
   //
@@ -349,3 +334,40 @@ int show_symbol_table(
   return get_transition_system(
     cmdline, message_handler, dummy_transition_system);
 }
+
+std::optional<transition_systemt> ebmc_languagest::transition_system()
+{
+  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);
+}

src/ebmc/build_transition_system.h

@@ -9,16 +9,25 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
 #define CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H
 
-class cmdlinet;
-class message_handlert;
-class transition_systemt;
+#include "ebmc_language.h"
 
 transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
 
-int preprocess(const cmdlinet &, message_handlert &);
+void preprocess(const cmdlinet &, message_handlert &);
 int show_parse(const cmdlinet &, message_handlert &);
 int show_modules(const cmdlinet &, message_handlert &);
 int show_module_hierarchy(const cmdlinet &, message_handlert &);
 int show_symbol_table(const cmdlinet &, message_handlert &);
 
+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;
+};
+
 #endif // CPROVER_EBMC_BUILD_TRANSITION_SYSTEM_H

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

@@ -19,6 +19,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"
@@ -108,23 +109,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";
@@ -208,7 +192,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(