Create a stub for a common process_goto_program

This should not alter observable behaviour.

Author: martin

src/cbmc/cbmc_parse_options.cpp

@@ -55,6 +55,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
+#include <goto-programs/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -912,6 +913,9 @@ bool cbmc_parse_optionst::process_goto_program(
   const optionst &options,
   messaget &log)
 {
+  // Common removal of types and complex constructs
+  ::process_goto_program(goto_model, options, log);
+
   // Remove inline assembler; this needs to happen before
   // adding the library.
   remove_asm(goto_model);

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/goto_inline.h>
 #include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/link_to_library.h>
+#include <goto-programs/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -867,6 +868,9 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 bool goto_analyzer_parse_optionst::process_goto_program(
   const optionst &options)
 {
+  // Common removal of types and complex constructs
+  ::process_goto_program(goto_model, options, log);
+
   {
     #if 0
     // Remove inline assembler; this needs to happen before

src/goto-diff/goto_diff_parse_options.cpp

@@ -32,6 +32,7 @@ Author: Peter Schrammel
 #include <goto-programs/link_to_library.h>
 #include <goto-programs/loop_ids.h>
 #include <goto-programs/mm_io.h>
+#include <goto-programs/process_goto_program.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
 #include <goto-programs/remove_function_pointers.h>
@@ -314,6 +315,9 @@ bool goto_diff_parse_optionst::process_goto_program(
   const optionst &options,
   goto_modelt &goto_model)
 {
+  // Common removal of types and complex constructs
+  ::process_goto_program(goto_model, options, log);
+
   {
     // Remove inline assembler; this needs to happen before
     // adding the library.

src/goto-programs/Makefile

@@ -39,6 +39,7 @@ SRC = add_malloc_may_fail_variable_initializations.cpp \
       parameter_assignments.cpp \
       pointer_arithmetic.cpp \
       printf_formatter.cpp \
+      process_goto_program.cpp \
       read_bin_goto_object.cpp \
       read_goto_binary.cpp \
       rebuild_goto_start_function.cpp \

src/goto-programs/process_goto_program.cpp

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Process a Goto Program
+
+Author: Martin Brain, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Get a Goto Program
+
+#include "process_goto_program.h"
+
+#include <goto-programs/goto_model.h>
+
+#include <util/message.h>
+#include <util/options.h>
+
+bool process_goto_program(
+  goto_modelt &goto_model,
+  const optionst &options,
+  messaget &log)
+{
+  return false;
+}

src/goto-programs/process_goto_program.h

@@ -0,0 +1,29 @@
+/*******************************************************************\
+
+Module: Process a Goto Program
+
+Author: Martin Brain, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Common processing and simplification of goto_programts.
+/// This includes linking libraries and removing a number of
+/// more complex types (vectors, complex, etc.) and constructs
+/// (returns, function pointers, etc.).
+/// This is can be used after initialize_goto_model but before
+/// analysis.  It is not madatory but is used by most tools.
+
+#ifndef CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H
+#define CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H
+
+class goto_modelt;
+class optionst;
+class messaget;
+
+bool process_goto_program(
+  goto_modelt &goto_model,
+  const optionst &options,
+  messaget &log);
+
+#endif // CPROVER_GOTO_PROGRAMS_PROCESS_GOTO_PROGRAM_H