Merge pull request #1117 from mgudemann/fix/ignore_functions_not_in_symbol_table_remove_static_init

Skip functions not in the symbol table in remove <clinit> loops

Author: mgudemann

src/cbmc/cbmc_parse_options.cpp

@@ -506,7 +506,11 @@ int cbmc_parse_optionst::doit()
   // unwinds <clinit> loops to number of enum elements
   // side effect: add this as explicit unwind to unwind set
   if(options.get_bool_option("java-unwind-enum-static"))
-    remove_static_init_loops(symbol_table, goto_functions, options);
+    remove_static_init_loops(
+      symbol_table,
+      goto_functions,
+      options,
+      ui_message_handler);
 
   // get solver
   cbmc_solverst cbmc_solvers(options, symbol_table, ui_message_handler);

src/goto-programs/remove_static_init_loops.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
-#include <util/message.h>
 #include <util/suffix.h>
 #include <util/string2int.h>
 
@@ -27,7 +26,8 @@ class remove_static_init_loopst
 
   void unwind_enum_static(
     const goto_functionst &goto_functions,
-    optionst &options);
+    optionst &options,
+    message_handlert &);
 protected:
   const symbol_tablet &symbol_table;
 };
@@ -38,9 +38,12 @@ class remove_static_init_loopst
 /// \return side effect is adding <clinit> loops to unwindset
 void remove_static_init_loopst::unwind_enum_static(
   const goto_functionst &goto_functions,
-  optionst &options)
+  optionst &options,
+  message_handlert &msg)
 {
   size_t unwind_max=0;
+  messaget message;
+  message.set_message_handler(msg);
   forall_goto_functions(f, goto_functions)
   {
     auto &p=f->second.body;
@@ -53,6 +56,13 @@ void remove_static_init_loopst::unwind_enum_static(
         const std::string java_clinit="<clinit>:()V";
         const std::string &fname=id2string(ins.function);
         size_t class_prefix_length=fname.find_last_of('.');
+        // is the function symbol in the symbol table?
+        if(!symbol_table.has_symbol(ins.function))
+        {
+          message.warning() << "function `" << id2string(ins.function)
+                            << "` is not in symbol table" << messaget::eom;
+          continue;
+        }
         // is Java function and static init?
         const symbolt &function_name=symbol_table.lookup(ins.function);
         if(!(function_name.mode==ID_java && has_suffix(fname, java_clinit)))
@@ -96,8 +106,9 @@ void remove_static_init_loopst::unwind_enum_static(
 void remove_static_init_loops(
   const symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
-  optionst &options)
+  optionst &options,
+  message_handlert &msg)
 {
   remove_static_init_loopst remove_loops(symbol_table);
-  remove_loops.unwind_enum_static(goto_functions, options);
+  remove_loops.unwind_enum_static(goto_functions, options, msg);
 }

src/goto-programs/remove_static_init_loops.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_functions.h>
 
+#include <util/message.h>
 #include <util/options.h>
 #include <util/symbol_table.h>
 
@@ -20,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 void remove_static_init_loops(
   const symbol_tablet &,
   const goto_functionst &,
-  optionst &);
+  optionst &,
+  message_handlert &);
 
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_STATIC_INIT_LOOPS_H