diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 2ed93d3eac2..6f7a69bf3fe 100644 --- 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 index f71af068e54..e2757600fcd 100644 --- 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/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp b/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp index 82bb8083d56..92e137b409b 100644 --- a/jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp +++ b/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 diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 7b3bc375b13..763de5ed10e 100644 --- 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 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 index c08a97b9759..b89091c33a9 100644 --- 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 index 49f8662a7dc..b63298a4dce 100644 --- 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 index 8ac7034bc7f..ad9aa00929a 100644 --- 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 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 index 16c1e34e3d0..26c0413d83b 100644 --- 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 index b645300ffce..d1873a53306 100644 --- 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 main; void set_arch(const irep_idt &); diff --git a/unit/compound_block_locations.cpp b/unit/compound_block_locations.cpp index e71679b04ba..2d42c290faa 100644 --- 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 index 6a5ba528aee..a72cbb1a7c8 100644 --- 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 index 6d8ddd0248c..fbae3762799 100644 --- 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;