Merge pull request #1730 from smowton/smowton/feature/remove_returns_per_function

JBMC: Remove-returns per function

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;