diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index 660e0c16188..2e525a8fa2b 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/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 diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index efea60220bd..ed029d6212b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1328,7 +1328,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 diff --git a/src/goto-programs/goto_check.cpp b/src/goto-programs/goto_check.cpp index c3f5e28576a..e105d98553b 100644 --- a/src/goto-programs/goto_check.cpp +++ b/src/goto-programs/goto_check.cpp @@ -12,45 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_check.h" #include -#include -#include -#include - -#include - -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, diff --git a/src/goto-programs/goto_check.h b/src/goto-programs/goto_check.h index b95e38afd94..91bbaedf264 100644 --- a/src/goto-programs/goto_check.h +++ b/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 diff --git a/src/goto-programs/process_goto_program.cpp b/src/goto-programs/process_goto_program.cpp index 17a8bbf923a..bcde95f76f6 100644 --- a/src/goto-programs/process_goto_program.cpp +++ b/src/goto-programs/process_goto_program.cpp @@ -27,6 +27,8 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk #include #include +#include + #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