register_languages is now an interface not just a convention

Author: martin

src/cbmc/cbmc_parse_options.h

@@ -114,7 +114,7 @@ class cbmc_parse_optionst : public parse_options_baset
 protected:
   goto_modelt goto_model;
 
-  void register_languages();
+  void register_languages() override;
   void get_command_line_options(optionst &);
   void preprocessing(const optionst &);
   bool set_properties();

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -183,7 +183,7 @@ class goto_analyzer_parse_optionst: public parse_options_baset
 protected:
   goto_modelt goto_model;
 
-  virtual void register_languages();
+  void register_languages() override;
 
   virtual void get_command_line_options(optionst &options);
 

src/goto-diff/goto_diff_parse_options.h

@@ -49,7 +49,7 @@ class goto_diff_parse_optionst : public parse_options_baset
   goto_diff_parse_optionst(int argc, const char **argv);
 
 protected:
-  void register_languages();
+  void register_languages() override;
 
   void get_command_line_options(optionst &options);
 

src/goto-harness/goto_harness_parse_options.cpp

@@ -108,6 +108,9 @@ int goto_harness_parse_optionst::doit()
   // This just sets up the defaults (and would interpret options such as --32).
   config.set(cmdline);
 
+  // Normally we would register language front-ends here but as goto-harness
+  // only works on goto binaries, we don't need to
+
   // Read goto binary into goto-model
   auto read_goto_binary_result =
     read_goto_binary(got_harness_config.in_file, ui_message_handler);

src/goto-instrument/goto_instrument_parse_options.h

@@ -145,7 +145,7 @@ class goto_instrument_parse_optionst : public parse_options_baset
   }
 
 protected:
-  void register_languages();
+  void register_languages() override;
 
   void get_goto_program();
   void instrument_goto_program();

src/memory-analyzer/memory_analyzer_parse_options.cpp

@@ -42,6 +42,13 @@ memory_analyzer_parse_optionst::memory_analyzer_parse_optionst(
 {
 }
 
+void memory_analyzer_parse_optionst::register_languages()
+{
+  // For now only C is supported due to the additional challenges of
+  // mapping source code to debugging symbols in other languages.
+  register_language(new_ansi_c_language);
+}
+
 int memory_analyzer_parse_optionst::doit()
 {
   if(cmdline.isset("version"))
@@ -91,7 +98,7 @@ int memory_analyzer_parse_optionst::doit()
       "--symtab-snapshot");
   }
 
-  register_language(new_ansi_c_language);
+  register_languages();
 
   std::string binary = cmdline.args.front();
 

src/memory-analyzer/memory_analyzer_parse_options.h

@@ -37,6 +37,8 @@ class memory_analyzer_parse_optionst : public parse_options_baset
 
 protected:
   messaget message;
+
+  void register_languages() override;
 };
 
 #endif // CPROVER_MEMORY_ANALYZER_MEMORY_ANALYZER_PARSE_OPTIONS_H

src/symtab2gb/symtab2gb_parse_options.cpp

@@ -94,6 +94,13 @@ static void run_symtab2gb(
   }
 }
 
+void symtab2gb_parse_optionst::register_languages()
+{
+  // As this is a converter and linker it only really needs to support
+  // the JSON symtab front-end.
+  register_language(new_json_symtab_language);
+}
+
 int symtab2gb_parse_optionst::doit()
 {
   if(cmdline.isset("version"))
@@ -112,7 +119,7 @@ int symtab2gb_parse_optionst::doit()
   {
     gb_filename = cmdline.get_value(SYMTAB2GB_OUT_FILE_OPT);
   }
-  register_language(new_json_symtab_language);
+  register_languages();
   config.set(cmdline);
   run_symtab2gb(symtab_filenames, gb_filename);
   return CPROVER_EXIT_SUCCESS;

src/symtab2gb/symtab2gb_parse_options.h

@@ -27,6 +27,9 @@ class symtab2gb_parse_optionst : public parse_options_baset
   symtab2gb_parse_optionst(int argc, const char *argv[]);
   void help() override;
   int doit() override;
+
+protected:
+  void register_languages() override;
 };
 
 #endif // CPROVER_SYMTAB2GB_SYMTAB2GB_PARSE_OPTIONS_H

src/util/parse_options.h

@@ -45,6 +45,10 @@ class parse_options_baset
   ui_message_handlert ui_message_handler;
   messaget log;
 
+  virtual void register_languages()
+  {
+  }
+
 private:
   void unknown_option_msg();
 };