Merge pull request #6716 from tautschnig/cleanup/goto_check_c

Replace the goto_check indirection by direct use of goto_check_c [blocks: #6688]

Author: tautschnig

src/goto-instrument/accelerate/acceleration_utils.cpp

@@ -475,7 +475,7 @@ void acceleration_utilst::ensure_no_overflows(scratch_programt &program)
 
   // goto_functionst::goto_functiont fn;
   // fn.body.instructions.swap(program.instructions);
-  // goto_check(ns, checker_options, fn);
+  // goto_check_c(ns, checker_options, fn);
   // fn.body.instructions.swap(program.instructions);
 
 #ifdef DEBUG

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1337,7 +1337,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   }
 
   // add generic checks, if needed
-  goto_check(options, goto_model, ui_message_handler);
+  goto_check_c(options, goto_model, ui_message_handler);
   transform_assertions_assumptions(options, goto_model);
 
   // check for uninitalized local variables

src/goto-programs/goto_check.cpp

@@ -12,45 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_check.h"
 
 #include <util/options.h>
-#include <util/symbol.h>
 
-#include <goto-programs/goto_model.h>
-#include <goto-programs/remove_skip.h>
-
-#include <ansi-c/goto_check_c.h>
-
-void goto_check(
-  const irep_idt &function_identifier,
-  goto_functionst::goto_functiont &goto_function,
-  const namespacet &ns,
-  const optionst &options,
-  message_handlert &message_handler)
-{
-  const auto &function_symbol = ns.lookup(function_identifier);
-
-  if(function_symbol.mode == ID_C)
-  {
-    goto_check_c(
-      function_identifier, goto_function, ns, options, message_handler);
-  }
-}
-
-void goto_check(
-  const namespacet &ns,
-  const optionst &options,
-  goto_functionst &goto_functions,
-  message_handlert &message_handler)
-{
-  goto_check_c(ns, options, goto_functions, message_handler);
-}
-
-void goto_check(
-  const optionst &options,
-  goto_modelt &goto_model,
-  message_handlert &message_handler)
-{
-  goto_check_c(options, goto_model, message_handler);
-}
+#include "goto_model.h"
+#include "remove_skip.h"
 
 static void transform_assertions_assumptions(
   goto_programt &goto_program,

src/goto-programs/goto_check.h

@@ -12,27 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 #define CPROVER_GOTO_PROGRAMS_GOTO_CHECK_H
 
-#include "goto_functions.h"
-
 class goto_modelt;
-class namespacet;
+class goto_programt;
 class optionst;
-class message_handlert;
-
-void goto_check(
-  const namespacet &,
-  const optionst &,
-  goto_functionst &,
-  message_handlert &);
-
-void goto_check(
-  const irep_idt &function_identifier,
-  goto_functionst::goto_functiont &,
-  const namespacet &,
-  const optionst &,
-  message_handlert &);
-
-void goto_check(const optionst &, goto_modelt &, message_handlert &);
 
 /// Handle the options "assertions", "built-in-assertions", "assumptions" to
 /// remove assertions and assumptions in \p goto_model when these are set to

src/goto-programs/process_goto_program.cpp

@@ -27,6 +27,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
 
+#include <ansi-c/goto_check_c.h>
+
 #include "goto_check.h"
 
 bool process_goto_program(
@@ -73,7 +75,7 @@ bool process_goto_program(
 
   // add generic checks
   log.status() << "Generic Property Instrumentation" << messaget::eom;
-  goto_check(options, goto_model, log.get_message_handler());
+  goto_check_c(options, goto_model, log.get_message_handler());
   transform_assertions_assumptions(options, goto_model);
 
   // checks don't know about adjusted float expressions