Merge pull request #6996 from tautschnig/cleanup/comma-separated-command-lines

Use cmdlinet::get_comma_separated_values where possible

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -203,7 +203,10 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("depth", cmdline.get_value("depth"));
 
   if(cmdline.isset("unwindset"))
-    options.set_option("unwindset", cmdline.get_value("unwindset"));
+  {
+    options.set_option(
+      "unwindset", cmdline.get_comma_separated_values("unwindset"));
+  }
 
   // constant propagation
   if(cmdline.isset("no-propagation"))

regression/goto-instrument/unwind-unwindset4/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---unwindset main.0:10,f.0:10,g.0:10,g.1:10 --unwinding-assertions
+--unwindset main.0:10,f.0:10 --unwindset g.0:10,g.1:10 --unwinding-assertions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/memory-analyzer/pointer_05/test.desc

@@ -1,5 +1,5 @@
 CORE
 main.gb
---breakpoint checkpoint --symbols p1,x,p2
+--breakpoint checkpoint --symbols p1,x --symbols p2
 ^EXIT=0$
 ^SIGNAL=0$

src/cbmc/cbmc_parse_options.cpp

@@ -255,7 +255,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   }
 
   if(cmdline.isset("unwindset"))
-    options.set_option("unwindset", cmdline.get_values("unwindset"));
+  {
+    options.set_option(
+      "unwindset", cmdline.get_comma_separated_values("unwindset"));
+  }
 
   // constant propagation
   if(cmdline.isset("no-propagation"))

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -186,7 +186,8 @@ int goto_instrument_parse_optionst::doit()
         if(unwindset_given)
         {
           unwindset.parse_unwindset(
-            cmdline.get_values("unwindset"), ui_message_handler);
+            cmdline.get_comma_separated_values("unwindset"),
+            ui_message_handler);
         }
 
         bool unwinding_assertions=cmdline.isset("unwinding-assertions");

src/goto-instrument/unwindset.cpp

@@ -179,13 +179,7 @@ void unwindsett::parse_unwindset(
   message_handlert &message_handler)
 {
   for(auto &element : unwindset)
-  {
-    std::vector<std::string> unwindset_elements =
-      split_string(element, ',', true, true);
-
-    for(auto &element : unwindset_elements)
-      parse_unwindset_one_loop(element, message_handler);
-  }
+    parse_unwindset_one_loop(element, message_handler);
 }
 
 optionalt<unsigned>

src/memory-analyzer/analyze_symbol.cpp

@@ -106,7 +106,8 @@ mp_integer gdb_value_extractort::get_type_size(const typet &type) const
   return *maybe_size / CHAR_BIT;
 }
 
-void gdb_value_extractort::analyze_symbols(const std::vector<irep_idt> &symbols)
+void gdb_value_extractort::analyze_symbols(
+  const std::list<std::string> &symbols)
 {
   // record addresses of given symbols
   for(const auto &id : symbols)

src/memory-analyzer/analyze_symbol.h

@@ -44,7 +44,7 @@ class gdb_value_extractort
   ///   \ref symbol_exprt (via the `values` map) and then call
   ///   \ref analyze_symbol on it.
   /// \param symbols: names of symbols to be analysed
-  void analyze_symbols(const std::vector<irep_idt> &symbols);
+  void analyze_symbols(const std::list<std::string> &symbols);
 
   /// Get memory snapshot as C code
   /// \return converted block of code with the collected assignments

src/memory-analyzer/memory_analyzer_parse_options.cpp

@@ -15,7 +15,6 @@ Author: Malte Mues <[email protected]>
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/message.h>
-#include <util/string_utils.h>
 #include <util/version.h>
 
 #include <goto-programs/goto_model.h>
@@ -103,9 +102,6 @@ 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, ',', true, true);
-
   auto opt = read_goto_binary(binary, ui_message_handler);
 
   if(!opt.has_value())
@@ -131,12 +127,8 @@ int memory_analyzer_parse_optionst::doit()
     gdb_value_extractor.run_gdb_to_breakpoint(breakpoint);
   }
 
-  std::vector<irep_idt> result_ids(result.size());
-  std::transform(
-    result.begin(), result.end(), result_ids.begin(), [](std::string &name) {
-      return irep_idt{name};
-    });
-  gdb_value_extractor.analyze_symbols(result_ids);
+  gdb_value_extractor.analyze_symbols(
+    cmdline.get_comma_separated_values("symbols"));
 
   std::ofstream file;