Moved call to final to lazy_goto_modelt::finalize

Explicitly load any functions added by call to final

Author: NathanJPhillips

src/goto-programs/lazy_goto_functions_map.h

@@ -120,6 +120,11 @@ class lazy_goto_functions_mapt final
 
   void unload(const key_type &name) const { goto_functions.erase(name); }
 
+  void ensure_function_loaded(const key_type &name) const
+  {
+    ensure_function_loaded_internal(name);
+  }
+
 private:
   // This returns a non-const reference, but if you use this method from a
   // const method then you should not return such a reference without making it

src/goto-programs/lazy_goto_model.cpp

@@ -11,6 +11,7 @@
 
 #include <util/cmdline.h>
 #include <util/config.h>
+#include <util/journalling_symbol_table.h>
 #include <util/language.h>
 #include <util/unicode.h>
 
@@ -184,12 +185,6 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
     throw 0;
   }
 
-  if(language_files.final(symbol_table))
-  {
-    msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
-    throw 0;
-  }
-
   // stupid hack
   config.set_object_bits_from_symbol_table(symbol_table);
 }
@@ -203,6 +198,24 @@ void lazy_goto_modelt::load_all_functions() const
 
 bool lazy_goto_modelt::finalize()
 {
+  messaget msg(message_handler);
+  journalling_symbol_tablet symbol_table=
+    journalling_symbol_tablet::wrap(this->symbol_table);
+  if(language_files.final(symbol_table))
+  {
+    msg.error() << "CONVERSION ERROR" << messaget::eom;
+    return true;
+  }
+  for(const irep_idt &updated_symbol_id : symbol_table.get_updated())
+  {
+    if(symbol_table.lookup_ref(updated_symbol_id).is_function())
+    {
+      // Re-convert any that already exist
+      goto_functions.unload(updated_symbol_id);
+      goto_functions.ensure_function_loaded(updated_symbol_id);
+    }
+  }
+
   language_files.clear();
 
   return post_process_functions(*goto_model);

src/util/symbol.h

@@ -109,6 +109,11 @@ class symbolt
   {
     return !is_static_lifetime;
   }
+
+  bool is_function() const
+  {
+    return !is_type && !is_macro && type.id()==ID_code;
+  }
 };
 
 std::ostream &operator<<(std::ostream &out, const symbolt &symbol);