Merge pull request #5340 from diffblue/remove-deprecated12

remove deprecated split_string variant

Author: Daniel Kroening

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<std::string> result;
-  split_string(symbol_list, ',', result, true, true);
+  std::vector<std::string> result = split_string(symbol_list, ',', true, true);
 
   auto opt = read_goto_binary(binary, ui_message_handler);
 

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<std::string> result;
+  std::vector<std::string> result = split_string(s, delim, strip);
 
-  split_string(s, delim, result, strip);
   if(result.size() != 2)
   {
     throw deserialization_exceptiont{"expected string '" + s +

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<std::string> &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<std::string> split_string(
   const std::string &s,
   char delim,