config.main is now optionalt<string>

kroening · kroening · commit 1b650557453f · 2019-04-30T14:05:31.000+01:00
This avoids the use of 'empty string' as indicator of 'no value'
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/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);
       }
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/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())
     {
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/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;
     }
diff --git a/src/goto-instrument/dump_c.cpp b/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;
+      }
     }
   }
 
diff --git a/src/goto-instrument/model_argc_argv.cpp b/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)
   {
diff --git a/src/jsil/jsil_entry_point.cpp b/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;
     }
diff --git a/src/linking/remove_internal_symbols.cpp b/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);
       }
diff --git a/src/util/config.h b/src/util/config.h
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #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 &);
 
diff --git a/unit/compound_block_locations.cpp b/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;
diff --git a/unit/json_symbol_table.cpp b/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;
diff --git a/unit/path_strategies.cpp b/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;

Original file line number	Diff line number	Diff line change
`@@ -249,10 +249,10 @@ bool java_bytecode_languaget::parse(`
`249`	`249`	`java_cp_include_files);`
`250`	`250`	`if(config.java.main_class.empty())`
`251`	`251`	`{`
`252`		`- const std::string &entry_method = config.main;`
`253`	`252`	`// If we have an entry method, we can derive a main class.`
`254`		`- if(!entry_method.empty())`
	`253`	`+ if(config.main.has_value())`
`255`	`254`	`{`
	`255`	`+ const std::string &entry_method = config.main.value();`
`256`	`256`	`const auto last_dot_position = entry_method.find_last_of('.');`
`257`	`257`	`main_class = entry_method.substr(0, last_dot_position);`
`258`	`258`	`}`
Original file line number	Diff line number	Diff line change
`@@ -122,12 +122,13 @@ bool ansi_c_entry_point(`
`122`	`122`
`123`	`123`	`irep_idt main_symbol;`
`124`	`124`
`125`		`- // find main symbol`
`126`		`- if(config.main!="")`
	`125`	`+ // find main symbol, if any is given`
	`126`	`+ if(config.main.has_value())`
`127`	`127`	`{`
`128`	`128`	`std::list<irep_idt> matches;`
`129`	`129`
`130`		`- forall_symbol_base_map(it, symbol_table.symbol_base_map, config.main)`
	`130`	`+ forall_symbol_base_map(`
	`131`	`+ it, symbol_table.symbol_base_map, config.main.value())`
`131`	`132`	`{`
`132`	`133`	`// look it up`
`133`	`134`	`symbol_tablet::symbolst::const_iterator s_it=`
`@@ -143,15 +144,15 @@ bool ansi_c_entry_point(`
`143`	`144`	`if(matches.empty())`
`144`	`145`	`{`
`145`	`146`	`messaget message(message_handler);`
`146`		- message.error() << "main symbol `" << config.main
`147`		`- << "' not found" << messaget::eom;`
	`147`	+ message.error() << "main symbol `" << config.main.value() << "' not found"
	`148`	`+ << messaget::eom;`
`148`	`149`	`return true; // give up`
`149`	`150`	`}`
`150`	`151`
`151`	`152`	`if(matches.size()>=2)`
`152`	`153`	`{`
`153`	`154`	`messaget message(message_handler);`
`154`		- message.error() << "main symbol `" << config.main
	`155`	+ message.error() << "main symbol `" << config.main.value()
`155`	`156`	`<< "' is ambiguous" << messaget::eom;`
`156`	`157`	`return true;`
`157`	`158`	`}`
Original file line number	Diff line number	Diff line change
`@@ -53,8 +53,8 @@ bool model_argc_argv(`
`53`	`53`	`return true;`
`54`	`54`	`}`
`55`	`55`
`56`		`- const symbolt &main_symbol=`
`57`		`- ns.lookup(config.main.empty()?ID_main:config.main);`
	`56`	`+ const symbolt &main_symbol =`
	`57`	`+ ns.lookup(config.main.has_value() ? config.main.value() : ID_main);`
`58`	`58`
`59`	`59`	`if(main_symbol.mode!=ID_C)`
`60`	`60`	`{`
Original file line number	Diff line number	Diff line change
`@@ -55,12 +55,13 @@ bool jsil_entry_point(`
`55`	`55`
`56`	`56`	`irep_idt main_symbol;`
`57`	`57`
`58`		`- // find main symbol`
`59`		`- if(config.main!="")`
	`58`	`+ // find main symbol, if any is given`
	`59`	`+ if(config.main.has_value())`
`60`	`60`	`{`
`61`	`61`	`std::list<irep_idt> matches;`
`62`	`62`
`63`		`- forall_symbol_base_map(it, symbol_table.symbol_base_map, config.main)`
	`63`	`+ forall_symbol_base_map(`
	`64`	`+ it, symbol_table.symbol_base_map, config.main.value())`
`64`	`65`	`{`
`65`	`66`	`// look it up`
`66`	`67`	`symbol_tablet::symbolst::const_iterator s_it=`
`@@ -76,15 +77,15 @@ bool jsil_entry_point(`
`76`	`77`	`if(matches.empty())`
`77`	`78`	`{`
`78`	`79`	`messaget message(message_handler);`
`79`		- message.error() << "main symbol `" << config.main
`80`		`- << "' not found" << messaget::eom;`
	`80`	+ message.error() << "main symbol `" << config.main.value() << "' not found"
	`81`	`+ << messaget::eom;`
`81`	`82`	`return true; // give up`
`82`	`83`	`}`
`83`	`84`
`84`	`85`	`if(matches.size()>=2)`
`85`	`86`	`{`
`86`	`87`	`messaget message(message_handler);`
`87`		- message.error() << "main symbol `" << config.main
	`88`	+ message.error() << "main symbol `" << config.main.value()
`88`	`89`	`<< "' is ambiguous" << messaget::eom;`
`89`	`90`	`return true;`
`90`	`91`	`}`
Original file line number	Diff line number	Diff line change
`@@ -138,8 +138,9 @@ void remove_internal_symbols(`
`138`	`138`	`else if(is_function)`
`139`	`139`	`{`
`140`	`140`	`// body? not local (i.e., "static")?`
`141`		`- if(has_body &&`
`142`		`- (!is_file_local \|\| (config.main==symbol.name.c_str())))`
	`141`	`+ if(`
	`142`	`+ has_body && (!is_file_local \|\| (config.main.has_value() &&`
	`143`	`+ symbol.name == config.main.value())))`
`143`	`144`	`{`
`144`	`145`	`get_symbols(ns, symbol, exported);`
`145`	`146`	`}`