diff --git a/src/memory-analyzer/memory_analyzer_parse_options.cpp b/src/memory-analyzer/memory_analyzer_parse_options.cpp index ff65e633ccc..371292c35c9 100644 --- a/src/memory-analyzer/memory_analyzer_parse_options.cpp +++ b/src/memory-analyzer/memory_analyzer_parse_options.cpp @@ -97,8 +97,7 @@ int memory_analyzer_parse_optionst::doit() std::string binary = cmdline.args.front(); const std::string symbol_list(cmdline.get_value("symbols")); - std::vector result; - split_string(symbol_list, ',', result, true, true); + std::vector result = split_string(symbol_list, ',', true, true); auto opt = read_goto_binary(binary, ui_message_handler); diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index ecd13604c9c..aab98943475 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -99,9 +99,8 @@ void split_string( // delim can't be a space character if using strip PRECONDITION(!std::isspace(delim) || !strip); - std::vector result; + std::vector result = split_string(s, delim, strip); - split_string(s, delim, result, strip); if(result.size() != 2) { throw deserialization_exceptiont{"expected string '" + s + diff --git a/src/util/string_utils.h b/src/util/string_utils.h index 40d3242f58d..a73bd8bd9cd 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -20,35 +20,22 @@ std::string strip_string(const std::string &s); std::string capitalize(const std::string &str); +void split_string( + const std::string &s, + char delim, + std::string &left, + std::string &right, + bool strip = false); + /// Given a string s, split into a sequence of substrings when separated by /// specified delimiter. /// \param s: The string to split up /// \param delim: The character to use as the delimiter -/// \param [out] result: The sub strings. Must be empty. /// \param strip: If true, strip_string will be used on each element, removing /// whitespace from the beginning and end of each element /// \param remove_empty: If true, all empty-string elements will be removed. /// This is applied after strip so whitespace only elements will be removed if /// both are set to true. -DEPRECATED(SINCE( - 2019, - 11, - 14, - "use split_string(s, delim, strip, remove_empty) instead")) -void split_string( - const std::string &s, - char delim, - std::vector &result, - bool strip = false, - bool remove_empty = false); - -void split_string( - const std::string &s, - char delim, - std::string &left, - std::string &right, - bool strip=false); - std::vector split_string( const std::string &s, char delim,