diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 6d98ee0cbee..19213c2b2c5 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -588,7 +588,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) if(options.get_bool_option("show")) { result = static_show_domain( - goto_model, *analyzer, options, get_message_handler(), out); + goto_model, *analyzer, options, out); } else if(options.get_bool_option("verify")) { @@ -603,17 +603,17 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) else if(options.get_bool_option("unreachable-instructions")) { result = static_unreachable_instructions( - goto_model, *analyzer, options, get_message_handler(), out); + goto_model, *analyzer, options, out); } else if(options.get_bool_option("unreachable-functions")) { result = static_unreachable_functions( - goto_model, *analyzer, options, get_message_handler(), out); + goto_model, *analyzer, options, out); } else if(options.get_bool_option("reachable-functions")) { result = static_reachable_functions( - goto_model, *analyzer, options, get_message_handler(), out); + goto_model, *analyzer, options, out); } else { diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 4593d3eb642..7f8f34fc694 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -629,7 +629,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) result = static_show_domain(goto_model, *analyzer, options, - get_message_handler(), out); } else if(options.get_bool_option("verify")) @@ -653,7 +652,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) result = static_unreachable_instructions(goto_model, *analyzer, options, - get_message_handler(), out); } else if(options.get_bool_option("unreachable-functions")) @@ -661,7 +659,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) result = static_unreachable_functions(goto_model, *analyzer, options, - get_message_handler(), out); } else if(options.get_bool_option("reachable-functions")) @@ -669,7 +666,6 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) result = static_reachable_functions(goto_model, *analyzer, options, - get_message_handler(), out); } else diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index 835311faf09..8f357cdfb7f 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -16,14 +16,12 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk /// \param goto_model: the program analyzed /// \param ai: the abstract interpreter after it has been run to fix point /// \param options: the parsed user options -/// \param message_handler: the system message handler /// \param out: output stream for the printing /// \return: false on success with the domain printed to out bool static_show_domain( const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, - message_handlert &message_handler, std::ostream &out) { if(options.get_bool_option("json")) diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h index 71a6e90ef92..499b3f7e111 100644 --- a/src/goto-analyzer/static_show_domain.h +++ b/src/goto-analyzer/static_show_domain.h @@ -20,7 +20,6 @@ bool static_show_domain( const goto_modelt &, const ai_baset &, const optionst &, - message_handlert &, std::ostream &); #endif // CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 760aceae75e..7f2c42a34a5 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -84,7 +84,6 @@ static void output_dead_plain( } static void add_to_xml( - const namespacet &ns, const goto_programt &goto_program, const dead_mapt &dead_map, xmlt &dest) @@ -206,7 +205,6 @@ bool static_unreachable_instructions( const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, - message_handlert &message_handler, std::ostream &out) { json_arrayt json_result; @@ -231,7 +229,7 @@ bool static_unreachable_instructions( } else if(options.get_bool_option("xml")) { - add_to_xml(ns, f_it->second.body, dead_map, xml_result); + add_to_xml(f_it->second.body, dead_map, xml_result); } else { @@ -431,7 +429,6 @@ bool static_unreachable_functions( const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, - message_handlert &message_handler, std::ostream &out) { std::unordered_set called = @@ -446,7 +443,6 @@ bool static_reachable_functions( const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, - message_handlert &message_handler, std::ostream &out) { std::unordered_set called = diff --git a/src/goto-analyzer/unreachable_instructions.h b/src/goto-analyzer/unreachable_instructions.h index eeee658ea52..15b410b2cd3 100644 --- a/src/goto-analyzer/unreachable_instructions.h +++ b/src/goto-analyzer/unreachable_instructions.h @@ -40,21 +40,18 @@ bool static_unreachable_instructions( const goto_modelt &, const ai_baset &, const optionst &, - message_handlert &, std::ostream &); bool static_unreachable_functions( const goto_modelt &, const ai_baset &, const optionst &, - message_handlert &, std::ostream &); bool static_reachable_functions( const goto_modelt &, const ai_baset &, const optionst &, - message_handlert &, std::ostream &); #endif // CPROVER_GOTO_ANALYZER_UNREACHABLE_INSTRUCTIONS_H