diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 5d25af30b4c..0385ea439ba 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -588,8 +588,8 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) bool result = true; if(options.get_bool_option("show")) { - result = static_show_domain( - goto_model, *analyzer, options, out); + static_show_domain(goto_model, *analyzer, options, out); + return CPROVER_EXIT_SUCCESS; } else if(options.get_bool_option("verify")) { diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index d4cd2452e52..cc392a93697 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -621,13 +621,13 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options) // Perform the task status() << "Performing task" << eom; + bool result = true; + if(options.get_bool_option("show")) { - result = static_show_domain(goto_model, - *analyzer, - options, - out); + static_show_domain(goto_model, *analyzer, options, out); + return CPROVER_EXIT_SUCCESS; } else if(options.get_bool_option("verify")) { diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp index c41dda35e22..3fe68b43495 100644 --- a/src/goto-analyzer/static_show_domain.cpp +++ b/src/goto-analyzer/static_show_domain.cpp @@ -17,8 +17,7 @@ Author: Martin Brain, martin.brain@cs.ox.ac.uk /// \param ai: the abstract interpreter after it has been run to fix point /// \param options: the parsed user options /// \param out: output stream for the printing -/// \return: false on success with the domain printed to out -bool static_show_domain( +void static_show_domain( const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, @@ -48,6 +47,4 @@ bool static_show_domain( // 'text' or console output ai.output(goto_model, out); } - - return false; } diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h index 499b3f7e111..0e107f91fa8 100644 --- a/src/goto-analyzer/static_show_domain.h +++ b/src/goto-analyzer/static_show_domain.h @@ -16,7 +16,7 @@ class goto_modelt; class message_handlert; class optionst; -bool static_show_domain( +void static_show_domain( const goto_modelt &, const ai_baset &, const optionst &,