Merge pull request #1409 from thk123/bugfix/lang-args-missing

Verify that language options have been initialised

Author: Thomas Kiley

src/cbmc/cbmc_parse_options.cpp

@@ -634,9 +634,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

@@ -119,6 +119,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());
@@ -202,6 +203,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();
 
@@ -387,6 +390,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