Add partial inlining as an optional part of process_goto_program

In CBMC and goto-diff this is dead, in goto-analyze it preserves the
existing behaviour.  It is not 100% clear to me that the existing behaviour
is useful or desirable but it is preserved as the point of this PR is not
changing behaviour unless necessary.

Author: martin

src/cbmc/cbmc_parse_options.cpp

@@ -50,6 +50,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/add_malloc_may_fail_variable_initializations.h>
 #include <goto-programs/adjust_float_expressions.h>
+#include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/instrument_preconditions.h>
 #include <goto-programs/link_to_library.h>
@@ -946,6 +947,13 @@ bool cbmc_parse_optionst::process_goto_program(
   // instrument library preconditions
   instrument_preconditions(goto_model);
 
+  // do partial inlining
+  if(options.get_bool_option("partial-inline"))
+  {
+    log.status() << "Partial Inlining" << messaget::eom;
+    goto_partial_inline(goto_model, log.get_message_handler());
+  }
+
   // remove returns, gcc vectors, complex
   remove_returns(goto_model);
   remove_vector(goto_model);

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -608,6 +608,9 @@ int goto_analyzer_parse_optionst::doit()
 
   goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
+  // Perserve backwards compatability in processing
+  options.set_option("partial-inline", true);
+
   if(process_goto_program(options))
     return CPROVER_EXIT_INTERNAL_ERROR;
 
@@ -906,8 +909,11 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     instrument_preconditions(goto_model);
 
     // do partial inlining
-    log.status() << "Partial Inlining" << messaget::eom;
-    goto_partial_inline(goto_model, ui_message_handler);
+    if(options.get_bool_option("partial-inline"))
+    {
+      log.status() << "Partial Inlining" << messaget::eom;
+      goto_partial_inline(goto_model, ui_message_handler);
+    }
 
     // remove returns, gcc vectors, complex
     remove_returns(goto_model);

src/goto-diff/goto_diff_parse_options.cpp

@@ -302,6 +302,13 @@ bool goto_diff_parse_optionst::process_goto_program(
     // instrument library preconditions
     instrument_preconditions(goto_model);
 
+    // do partial inlining
+    if(options.get_bool_option("partial-inline"))
+    {
+      log.status() << "Partial Inlining" << messaget::eom;
+      goto_partial_inline(goto_model, ui_message_handler);
+    }
+
     // remove returns, gcc vectors, complex
     remove_returns(goto_model);
     remove_vector(goto_model);