diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 682cbbc5991..75f535cc141 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/jbmc/src/janalyzer/janalyzer_parse_options.cpp @@ -410,7 +410,9 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options) } else { - std::string json_file = cmdline.get_value("json"); + optionalt json_file; + if(cmdline.isset("json")) + json_file = cmdline.get_value("json"); bool result = taint_analysis( goto_model, taint_file, ui_message_handler, false, json_file); return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS; diff --git a/src/goto-analyzer/taint_analysis.cpp b/src/goto-analyzer/taint_analysis.cpp index 770c771364c..37999f064b8 100644 --- a/src/goto-analyzer/taint_analysis.cpp +++ b/src/goto-analyzer/taint_analysis.cpp @@ -39,7 +39,7 @@ class taint_analysist const symbol_tablet &, goto_functionst &, bool show_full, - const std::string &json_file_name); + const optionalt &json_file_name); protected: messaget log; @@ -224,12 +224,12 @@ bool taint_analysist::operator()( const symbol_tablet &symbol_table, goto_functionst &goto_functions, bool show_full, - const std::string &json_file_name) + const optionalt &json_file_name) { try { json_arrayt json_result; - bool use_json=!json_file_name.empty(); + bool use_json = json_file_name.has_value(); log.status() << "Reading taint file `" << taint_file_name << "'" << messaget::eom; @@ -378,17 +378,17 @@ bool taint_analysist::operator()( if(use_json) { - std::ofstream json_out(json_file_name); + std::ofstream json_out(json_file_name.value()); if(!json_out) { - log.error() << "Failed to open json output `" << json_file_name << "'" - << messaget::eom; + log.error() << "Failed to open json output `" << json_file_name.value() + << "'" << messaget::eom; return true; } - log.status() << "Analysis result is written to `" << json_file_name << "'" - << messaget::eom; + log.status() << "Analysis result is written to `" + << json_file_name.value() << "'" << messaget::eom; json_out << json_result << '\n'; } @@ -418,7 +418,7 @@ bool taint_analysis( const std::string &taint_file_name, message_handlert &message_handler, bool show_full, - const std::string &json_file_name) + const optionalt &json_file_name) { taint_analysist taint_analysis(message_handler); return taint_analysis( diff --git a/src/goto-analyzer/taint_analysis.h b/src/goto-analyzer/taint_analysis.h index 38390ee646e..c753afef0ff 100644 --- a/src/goto-analyzer/taint_analysis.h +++ b/src/goto-analyzer/taint_analysis.h @@ -22,6 +22,6 @@ bool taint_analysis( const std::string &taint_file_name, message_handlert &, bool show_full, - const std::string &json_output_file_name = ""); + const optionalt &json_output_file_name = {}); #endif // CPROVER_GOTO_ANALYZER_TAINT_ANALYSIS_H