Remove language_uit dependency from goto-diff

Parsing is encapsulated in initialize_goto_model.

Author: tautschnig

src/goto-diff/goto_diff_languages.cpp

@@ -9,14 +9,14 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Language Registration
 
-#include "goto_diff_languages.h"
+#include "goto_diff_parse_options.h"
 
 #include <langapi/mode.h>
 
 #include <ansi-c/ansi_c_language.h>
 #include <cpp/cpp_language.h>
 
-void goto_diff_languagest::register_languages()
+void goto_diff_parse_optionst::register_languages()
 {
   register_language(new_ansi_c_language);
   register_language(new_cpp_language);

src/goto-diff/goto_diff_languages.h

@@ -27,6 +27,7 @@ Author: Peter Schrammel
 #include <goto-programs/adjust_float_expressions.h>
 #include <goto-programs/goto_convert_functions.h>
 #include <goto-programs/goto_inline.h>
+#include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
@@ -62,20 +63,8 @@ Author: Peter Schrammel
 
 goto_diff_parse_optionst::goto_diff_parse_optionst(int argc, const char **argv)
   : parse_options_baset(GOTO_DIFF_OPTIONS, argc, argv),
-    goto_diff_languagest(cmdline, ui_message_handler),
-    ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
-    languages2(cmdline, ui_message_handler)
-{
-}
-
-::goto_diff_parse_optionst::goto_diff_parse_optionst(
-  int argc,
-  const char **argv,
-  const std::string &extra_options)
-  : parse_options_baset(GOTO_DIFF_OPTIONS + extra_options, argc, argv),
-    goto_diff_languagest(cmdline, ui_message_handler),
-    ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION),
-    languages2(cmdline, ui_message_handler)
+    messaget(ui_message_handler),
+    ui_message_handler(cmdline, std::string("GOTO-DIFF ") + CBMC_VERSION)
 {
 }
 
@@ -252,21 +241,21 @@ int goto_diff_parse_optionst::doit()
     return CPROVER_EXIT_INCORRECT_TASK;
   }
 
-  goto_modelt goto_model1, goto_model2;
+  register_languages();
 
-  int get_goto_program_ret=
-    get_goto_program(options, *this, goto_model1);
-  if(get_goto_program_ret!=-1)
-    return get_goto_program_ret;
-  get_goto_program_ret=
-    get_goto_program(options, languages2, goto_model2);
-  if(get_goto_program_ret!=-1)
-    return get_goto_program_ret;
+  goto_modelt goto_model1 =
+    initialize_goto_model({cmdline.args[0]}, ui_message_handler, options);
+  if(process_goto_program(options, goto_model1))
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  goto_modelt goto_model2 =
+    initialize_goto_model({cmdline.args[1]}, ui_message_handler, options);
+  if(process_goto_program(options, goto_model2))
+    return CPROVER_EXIT_INTERNAL_ERROR;
 
   if(cmdline.isset("show-loops"))
   {
-    show_loop_ids(get_ui(), goto_model1);
-    show_loop_ids(get_ui(), goto_model2);
+    show_loop_ids(ui_message_handler.get_ui(), goto_model1);
+    show_loop_ids(ui_message_handler.get_ui(), goto_model2);
     return CPROVER_EXIT_SUCCESS;
   }
 
@@ -323,65 +312,6 @@ int goto_diff_parse_optionst::doit()
   return CPROVER_EXIT_SUCCESS;
 }
 
-int goto_diff_parse_optionst::get_goto_program(
-  const optionst &options,
-  goto_diff_languagest &languages,
-  goto_modelt &goto_model)
-{
-  status() << "Reading program from `" << cmdline.args[0] << "'" << eom;
-
-  if(is_goto_binary(cmdline.args[0]))
-  {
-    if(read_goto_binary(
-        cmdline.args[0],
-        goto_model.symbol_table,
-        goto_model.goto_functions,
-        languages.get_message_handler()))
-      return CPROVER_EXIT_INCORRECT_TASK;
-
-    config.set(cmdline);
-
-    // This one is done.
-    cmdline.args.erase(cmdline.args.begin());
-  }
-  else
-  {
-    // This is a a workaround to make parse() think that there is only
-    // one source file.
-    std::string arg2("");
-    if(cmdline.args.size()==2)
-    {
-      arg2 = cmdline.args[1];
-      cmdline.args.erase(--cmdline.args.end());
-    }
-
-    if(languages.parse() ||
-       languages.typecheck() ||
-       languages.final())
-      return CPROVER_EXIT_INCORRECT_TASK;
-
-    // we no longer need any parse trees or language files
-    languages.clear_parse();
-
-    status() << "Generating GOTO Program" << eom;
-
-    goto_model.symbol_table=languages.symbol_table;
-    goto_convert(
-      goto_model.symbol_table,
-      goto_model.goto_functions,
-      ui_message_handler);
-
-    if(process_goto_program(options, goto_model))
-      return CPROVER_EXIT_INTERNAL_ERROR;
-
-    // if we had a second argument then we will handle it next
-    if(arg2!="")
-      cmdline.args[0]=arg2;
-  }
-
-  return -1; // no error, continue
-}
-
 bool goto_diff_parse_optionst::process_goto_program(
   const optionst &options,
   goto_modelt &goto_model)

src/goto-diff/goto_diff_parse_options.cpp

@@ -22,8 +22,6 @@ Author: Peter Schrammel
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
-#include "goto_diff_languages.h"
-
 class goto_modelt;
 class optionst;
 
@@ -41,31 +39,20 @@ class optionst;
   "(compact-output)"
 // clang-format on
 
-class goto_diff_parse_optionst:
-  public parse_options_baset,
-  public goto_diff_languagest
+class goto_diff_parse_optionst : public parse_options_baset, public messaget
 {
 public:
   virtual int doit();
   virtual void help();
 
   goto_diff_parse_optionst(int argc, const char **argv);
-  goto_diff_parse_optionst(
-    int argc,
-    const char **argv,
-    const std::string &extra_options);
 
 protected:
   ui_message_handlert ui_message_handler;
-  goto_diff_languagest languages2;
+  void register_languages();
 
   void get_command_line_options(optionst &options);
 
-  virtual int get_goto_program(
-    const optionst &options,
-    goto_diff_languagest &languages,
-    goto_modelt &goto_model);
-
   bool process_goto_program(const optionst &options, goto_modelt &goto_model);
 };