Verify that language options have been initialized

We already had assertions before some of the languaget interface but not
for all of them. This can cause errors for regenerating entry points so
added assertions. This revealed the problem which is for entry function
recreation there is a new languaget that hasn't parsed the cmdline.

Author: thk123

src/cbmc/cbmc_parse_options.cpp

@@ -633,9 +633,10 @@ int cbmc_parse_optionst::get_goto_program(
     {
       const std::string &function_id=cmdline.get_value("function");
       rebuild_goto_start_functiont start_function_rebuilder(
-        get_message_handler(),
-        goto_model.symbol_table,
-        goto_model.goto_functions);
+          get_message_handler(),
+          cmdline,
+          goto_model.symbol_table,
+          goto_model.goto_functions);
 
       if(start_function_rebuilder(function_id))
       {

src/goto-programs/initialize_goto_model.cpp

@@ -138,6 +138,7 @@ bool initialize_goto_model(
       const std::string &function_id=cmdline.get_value("function");
       rebuild_goto_start_functiont start_function_rebuilder(
         msg.get_message_handler(),
+        cmdline,
         goto_model.symbol_table,
         goto_model.goto_functions);
 

src/goto-programs/rebuild_goto_start_function.cpp

@@ -13,6 +13,7 @@
 #include <util/symbol.h>
 #include <util/symbol_table.h>
 #include <util/prefix.h>
+#include <util/cmdline.h>
 #include <langapi/mode.h>
 #include <memory>
 
@@ -25,11 +26,13 @@
 ///   body of the _start function).
 rebuild_goto_start_functiont::rebuild_goto_start_functiont(
   message_handlert &_message_handler,
+  const cmdlinet &cmdline,
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions):
-  messaget(_message_handler),
-  symbol_table(symbol_table),
-  goto_functions(goto_functions)
+    messaget(_message_handler),
+    cmdline(cmdline),
+    symbol_table(symbol_table),
+    goto_functions(goto_functions)
 {
 }
 
@@ -50,6 +53,7 @@ bool rebuild_goto_start_functiont::operator()(
   std::unique_ptr<languaget> language=get_language_from_mode(mode);
   INVARIANT(language, "No language found for mode: "+id2string(mode));
   language->set_message_handler(get_message_handler());
+  language->get_language_options(cmdline);
 
   // To create a new entry point we must first remove the old one
   remove_existing_entry_point();

src/goto-programs/rebuild_goto_start_function.h

@@ -10,6 +10,7 @@
 #define CPROVER_GOTO_PROGRAMS_REBUILD_GOTO_START_FUNCTION_H
 
 #include <util/message.h>
+class cmdlinet;
 
 class symbol_tablet;
 class goto_functionst;
@@ -25,6 +26,7 @@ class rebuild_goto_start_functiont: public messaget
 public:
   rebuild_goto_start_functiont(
     message_handlert &_message_handler,
+    const cmdlinet &cmdline,
     symbol_tablet &symbol_table,
     goto_functionst &goto_functions);
 
@@ -35,6 +37,7 @@ class rebuild_goto_start_functiont: public messaget
 
   void remove_existing_entry_point();
 
+  const cmdlinet &cmdline;
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
 };

src/java_bytecode/java_bytecode_language.cpp

@@ -116,6 +116,7 @@ bool java_bytecode_languaget::generate_start_function(
   const irep_idt &entry_function_symbol_id,
   symbol_tablet &symbol_table)
 {
+  PRECONDITION(language_options_initialized);
   const auto res=
     get_main_symbol(
       symbol_table, entry_function_symbol_id, get_message_handler());
@@ -200,6 +201,8 @@ bool java_bytecode_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
+  PRECONDITION(language_options_initialized);
+
   if(string_refinement_enabled)
     string_preprocess.initialize_conversion_table();
 
@@ -385,6 +388,7 @@ void java_bytecode_languaget::replace_string_methods(
 
 bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
 {
+  PRECONDITION(language_options_initialized);
   java_internal_additions(symbol_table);
 
   // replace code of String methods calls by code we generate