use optional for json file name

This is follow-up of #4041.  It avoids the use of an empty string as
indicator of 'no value'.

Author: Daniel Kroening

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<std::string> 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;

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<std::string> &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<std::string> &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<std::string> &json_file_name)
 {
   taint_analysist taint_analysis(message_handler);
   return taint_analysis(

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<std::string> &json_output_file_name = {});
 
 #endif // CPROVER_GOTO_ANALYZER_TAINT_ANALYSIS_H