Remove returns: support running per-function

This converts functions from conventional to via-global-variable return style
on a function-by-function basis. It results in some complication, as the globals
are now seen by the language's final pass, meaning it must ignore them for initialisation
purposes, and we must cope with functions not having their "true" type while other functions
are still being loaded.

One test in cbmc-java failed because it was written in C, which we don't adapt to support
incremental loading yet, so it is moved to the cbmc test directory, where it can still achieve
its goal of checking whether uncaught_exceptions_analysist can tolerate CPROVER_assert and
similar builtins, since cbmc also runs the remove_exceptions pass.

Author: smowton

regression/cbmc-java/exceptions25/main.c renamed to regression/cbmc/uncaught_exceptions_analysis1/main.c

@@ -99,6 +99,16 @@ class lazy_goto_functions_mapt final
     return ensure_function_loaded_internal(name).second;
   }
 
+  /// Determines if this lazy GOTO functions map can produce a body for the
+  /// given function
+  /// \param name: function ID to query
+  /// \return true if we can produce a function body, or false if we would leave
+  ///   it a bodyless stub.
+  bool can_produce_function(const key_type &name) const
+  {
+    return language_files.can_convert_lazy_method(name);
+  }
+
   void unload(const key_type &name) const { goto_functions.erase(name); }
 
   void ensure_function_loaded(const key_type &name) const

regression/cbmc-java/exceptions25/test.desc renamed to regression/cbmc/uncaught_exceptions_analysis1/test.desc

@@ -31,7 +31,7 @@ lazy_goto_modelt::lazy_goto_modelt(
       [this] (goto_functionst::goto_functiont &function) -> void
       {
         goto_model_functiont model_function(*goto_model, function);
-        this->post_process_function(model_function);
+        this->post_process_function(model_function, *this);
       },
       message_handler),
     post_process_function(std::move(post_process_function)),
@@ -51,7 +51,7 @@ lazy_goto_modelt::lazy_goto_modelt(lazy_goto_modelt &&other)
       [this] (goto_functionst::goto_functiont &function) -> void
       {
         goto_model_functiont model_function(*goto_model, function);
-        this->post_process_function(model_function);
+        this->post_process_function(model_function, *this);
       },
       other.message_handler),
     language_files(std::move(other.language_files)),
@@ -239,3 +239,8 @@ bool lazy_goto_modelt::finalize()
 
   return post_process_functions(*goto_model);
 }
+
+bool lazy_goto_modelt::can_produce_function(const irep_idt &id) const
+{
+  return goto_functions.can_produce_function(id);
+}

src/goto-programs/lazy_goto_functions_map.h

@@ -15,11 +15,24 @@
 class cmdlinet;
 class optionst;
 
+/// Interface for a provider of function definitions to report whether or not it
+/// can provide a definition (function body) for a given function ID.
+struct can_produce_functiont
+{
+  /// Determines if this function provider can produce a body for the given
+  /// function
+  /// \param id: function ID to query
+  /// \return true if we can produce a function body, or false if we would leave
+  ///   it a bodyless stub.
+  virtual bool can_produce_function(const irep_idt &id) const = 0;
+};
+
 /// Model that holds partially loaded map of functions
-class lazy_goto_modelt
+class lazy_goto_modelt : public can_produce_functiont
 {
 public:
-  typedef std::function<void(goto_model_functiont &function)>
+  typedef std::function<
+    void(goto_model_functiont &function, const can_produce_functiont &)>
     post_process_functiont;
   typedef std::function<bool(goto_modelt &goto_model)> post_process_functionst;
 
@@ -51,12 +64,10 @@ class lazy_goto_modelt
     message_handlert &message_handler)
   {
     return lazy_goto_modelt(
-      [&handler] (goto_model_functiont &function)
-      {
-        handler.process_goto_function(function);
+      [&handler] (goto_model_functiont &fun, const can_produce_functiont &cpf) { // NOLINT(*)
+        handler.process_goto_function(fun, cpf);
       },
-      [&handler, &options] (goto_modelt &goto_model) -> bool
-      {
+      [&handler, &options] (goto_modelt &goto_model) -> bool { // NOLINT(*)
         return handler.process_goto_functions(goto_model, options);
       },
       message_handler);
@@ -88,6 +99,8 @@ class lazy_goto_modelt
     return std::move(model.goto_model);
   }
 
+  virtual bool can_produce_function(const irep_idt &id) const;
+
 private:
   std::unique_ptr<goto_modelt> goto_model;