From 80b972bf6dd328bb1462b5449ad87a41c1a21535 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 29 Jan 2018 15:42:35 +0000
Subject: [PATCH] Use split_string in set_classpath

Makes code of this function clearer.
---
 src/util/config.cpp | 38 +++++++++++++-------------------------
 1 file changed, 13 insertions(+), 25 deletions(-)

diff --git a/src/util/config.cpp b/src/util/config.cpp
index 7bff6a30bd5..15680a6c448 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "std_expr.h"
 #include "cprover_prefix.h"
 #include "string2int.h"
+#include "string_utils.h"
 
 configt config;
 
@@ -1286,31 +1287,18 @@ irep_idt configt::this_architecture()
 
 void configt::set_classpath(const std::string &cp)
 {
-  std::string current;
-  for(std::size_t pos=0; pos<cp.size(); pos++)
-  {
-    // These are separated by colons on Unix, and semicolons on
-    // Windows.
-    #ifdef _WIN32
-    const char cp_separator=';';
-    #else
-    const char cp_separator=':';
-    #endif
-
-    if(cp[pos]==cp_separator)
-    {
-      if(!current.empty())
-      {
-        java.classpath.push_back(current);
-        current.clear();
-      }
-    }
-    else
-      current+=cp[pos];
-  }
-
-  if(!current.empty())
-    java.classpath.push_back(current);
+// These are separated by colons on Unix, and semicolons on
+// Windows.
+#ifdef _WIN32
+  const char cp_separator = ';';
+#else
+  const char cp_separator = ':';
+#endif
+
+  std::vector<std::string> class_path;
+  split_string(cp, cp_separator, class_path);
+  java.classpath.insert(
+    java.classpath.end(), class_path.begin(), class_path.end());
 }
 
 irep_idt configt::this_operating_system()