deprecate a split_string variant

This deprecates the variant of split_string which uses a parameter to return
the result.  This is no longer appropriate since C++11's rvalue references.

Author: Daniel Kroening

src/goto-harness/memory_snapshot_harness_generator.cpp

@@ -90,8 +90,8 @@ void memory_snapshot_harness_generatort::handle_option(
   }
   else if(option == MEMORY_SNAPSHOT_HARNESS_HAVOC_VARIABLES_OPT)
   {
-    std::vector<std::string> havoc_candidates;
-    split_string(values.front(), ',', havoc_candidates, true);
+    std::vector<std::string> havoc_candidates =
+      split_string(values.front(), ',', true);
     for(const auto &candidate : havoc_candidates)
     {
       variables_to_havoc.insert(candidate);
@@ -431,8 +431,7 @@ memory_snapshot_harness_generatort::entry_goto_locationt
 memory_snapshot_harness_generatort::parse_goto_location(
   const std::string &cmdl_option)
 {
-  std::vector<std::string> start;
-  split_string(cmdl_option, ':', start, true);
+  std::vector<std::string> start = split_string(cmdl_option, ':', true);
 
   if(
     start.empty() || start.front().empty() ||

src/goto-instrument/splice_call.cpp

@@ -31,8 +31,8 @@ static bool parse_caller_callee(
   const std::string &callercallee,
   std::vector<std::string> &result)
 {
-  split_string(callercallee, ',', result);
-  return (result.size()!= 2);
+  result = split_string(callercallee, ',');
+  return result.size() != 2;
 }
 
 bool splice_call(

src/util/string_utils.h

@@ -10,6 +10,8 @@ Author: Daniel Poetzl
 #ifndef CPROVER_UTIL_STRING_UTILS_H
 #define CPROVER_UTIL_STRING_UTILS_H
 
+#include "deprecate.h"
+
 #include <iosfwd>
 #include <string>
 #include <vector>
@@ -26,6 +28,11 @@ std::string strip_string(const std::string &s);
 /// \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,