config.main is now optionalt<string> [blocks: #4041]

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -249,10 +249,10 @@ bool java_bytecode_languaget::parse(
       java_cp_include_files);
     if(config.java.main_class.empty())
     {
-      const std::string &entry_method = config.main;
       // If we have an entry method, we can derive a main class.
-      if(!entry_method.empty())
+      if(config.main.has_value())
       {
+        const std::string &entry_method = config.main.value();
         const auto last_dot_position = entry_method.find_last_of('.');
         main_class = entry_method.substr(0, last_dot_position);
       }

jbmc/src/java_bytecode/java_entry_point.cpp

@@ -533,14 +533,14 @@ main_function_resultt get_main_symbol(
   messaget message(message_handler);
 
   // find main symbol
-  if(config.main!="")
+  if(config.main.has_value())
   {
     // Add java:: prefix
-    std::string main_identifier="java::"+config.main;
+    std::string main_identifier = "java::" + config.main.value();
 
     std::string error_message;
-    irep_idt main_symbol_id=
-      resolve_friendly_method_name(config.main, symbol_table, error_message);
+    irep_idt main_symbol_id = resolve_friendly_method_name(
+      config.main.value(), symbol_table, error_message);
 
     if(main_symbol_id==irep_idt())
     {

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -171,7 +171,7 @@ SCENARIO("test_value_set_analysis",
   GIVEN("Normal and custom value-set analysis of CustomVSATest::test")
   {
     config.set_arch("none");
-    config.main = "";
+    config.main = {};
 
     // This classpath is the default, but the config object
     // is global and previous unit tests may have altered it

src/ansi-c/ansi_c_entry_point.cpp

@@ -122,12 +122,13 @@ bool ansi_c_entry_point(
 
   irep_idt main_symbol;
 
-  // find main symbol
-  if(config.main!="")
+  // find main symbol, if any is given
+  if(config.main.has_value())
   {
     std::list<irep_idt> matches;
 
-    forall_symbol_base_map(it, symbol_table.symbol_base_map, config.main)
+    forall_symbol_base_map(
+      it, symbol_table.symbol_base_map, config.main.value())
     {
       // look it up
       symbol_tablet::symbolst::const_iterator s_it=
@@ -143,15 +144,15 @@ bool ansi_c_entry_point(
     if(matches.empty())
     {
       messaget message(message_handler);
-      message.error() << "main symbol `" << config.main
-                      << "' not found" << messaget::eom;
+      message.error() << "main symbol `" << config.main.value() << "' not found"
+                      << messaget::eom;
       return true; // give up
     }
 
     if(matches.size()>=2)
     {
       messaget message(message_handler);
-      message.error() << "main symbol `" << config.main
+      message.error() << "main symbol `" << config.main.value()
                       << "' is ambiguous" << messaget::eom;
       return true;
     }

src/goto-instrument/dump_c.cpp

@@ -202,12 +202,14 @@ void dump_ct::operator()(std::ostream &os)
       goto_functionst::function_mapt::const_iterator func_entry=
         goto_functions.function_map.find(symbol.name);
 
-      if(!harness &&
-         func_entry!=goto_functions.function_map.end() &&
-         func_entry->second.body_available() &&
-         (symbol.name==ID_main ||
-          (!config.main.empty() && symbol.name==config.main)))
+      if(
+        !harness && func_entry != goto_functions.function_map.end() &&
+        func_entry->second.body_available() &&
+        (symbol.name == ID_main ||
+         (config.main.has_value() && symbol.name == config.main.value())))
+      {
         skip_function_main=true;
+      }
     }
   }
 

src/goto-instrument/model_argc_argv.cpp

@@ -53,8 +53,8 @@ bool model_argc_argv(
     return true;
   }
 
-  const symbolt &main_symbol=
-    ns.lookup(config.main.empty()?ID_main:config.main);
+  const symbolt &main_symbol =
+    ns.lookup(config.main.has_value() ? config.main.value() : ID_main);
 
   if(main_symbol.mode!=ID_C)
   {

src/jsil/jsil_entry_point.cpp

@@ -55,12 +55,13 @@ bool jsil_entry_point(
 
   irep_idt main_symbol;
 
-  // find main symbol
-  if(config.main!="")
+  // find main symbol, if any is given
+  if(config.main.has_value())
   {
     std::list<irep_idt> matches;
 
-    forall_symbol_base_map(it, symbol_table.symbol_base_map, config.main)
+    forall_symbol_base_map(
+      it, symbol_table.symbol_base_map, config.main.value())
     {
       // look it up
       symbol_tablet::symbolst::const_iterator s_it=
@@ -76,15 +77,15 @@ bool jsil_entry_point(
     if(matches.empty())
     {
       messaget message(message_handler);
-      message.error() << "main symbol `" << config.main
-                      << "' not found" << messaget::eom;
+      message.error() << "main symbol `" << config.main.value() << "' not found"
+                      << messaget::eom;
       return true; // give up
     }
 
     if(matches.size()>=2)
     {
       messaget message(message_handler);
-      message.error() << "main symbol `" << config.main
+      message.error() << "main symbol `" << config.main.value()
                       << "' is ambiguous" << messaget::eom;
       return true;
     }

src/linking/remove_internal_symbols.cpp

@@ -138,8 +138,9 @@ void remove_internal_symbols(
     else if(is_function)
     {
       // body? not local (i.e., "static")?
-      if(has_body &&
-         (!is_file_local || (config.main==symbol.name.c_str())))
+      if(
+        has_body && (!is_file_local || (config.main.has_value() &&
+                                        symbol.name == config.main.value())))
       {
         get_symbols(ns, symbol, exported);
       }

src/util/config.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "ieee_float.h"
 #include "irep.h"
+#include "optional.h"
 
 class cmdlinet;
 class symbol_tablet;
@@ -169,7 +170,7 @@ class configt
   } bv_encoding;
 
   // this is the function to start executing
-  std::string main;
+  optionalt<std::string> main;
 
   void set_arch(const irep_idt &);
 

unit/compound_block_locations.cpp

@@ -277,7 +277,7 @@ void compound_block_locationst::check_compound_block_locations(
   register_language(new_ansi_c_language);
   cmdlinet cmdline;
   cmdline.args.push_back(tmp());
-  config.main = "main";
+  config.main = std::string("main");
   config.set(cmdline);
 
   optionst opts;

unit/json_symbol_table.cpp

@@ -97,7 +97,7 @@ TEST_CASE("json symbol table read/write consistency")
   register_language(new_ansi_c_language);
 
   cmdlinet cmdline;
-  config.main = "main";
+  config.main = std::string("main");
   config.set(cmdline);
 
   goto_modelt goto_model;

unit/path_strategies.cpp

@@ -381,7 +381,7 @@ void _check_with_strategy(
   register_language(new_ansi_c_language);
   cmdlinet cmdline;
   cmdline.args.push_back(tmp());
-  config.main = "main";
+  config.main = std::string("main");
   config.set(cmdline);
 
   optionst options;