Fix based on reviews

Author: Petr Bauch

src/cbmc/cbmc_parse_options.cpp

@@ -933,6 +933,7 @@ void cbmc_parse_optionst::help()
     " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
+    HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     "\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1436,7 +1436,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     status() << "Performing a function pointer reachability slice" << eom;
     function_path_reachability_slicer(
-      goto_model, cmdline.get_value("fp-reachability-slice"));
+      goto_model, cmdline.get_comma_separated_values("fp-reachability-slice"));
   }
 
   // full slice?
@@ -1619,10 +1619,7 @@ void goto_instrument_parse_optionst::help()
     " --render-cluster-function    clusterises the dot by functions\n"
     "\n"
     "Slicing:\n"
-    " --fp-reachability-slice <f>  remove instructions that cannot appear on a\n" // NOLINT(*)
-    "                              trace that visits all given functions. The list of functions has to be\n" // NOLINT(*)
-    "                              given as a comma separated list.\n"
-    " --reachability-slice         slice away instructions that can't reach assertions\n" // NOLINT(*)
+    HELP_REACHABILITY_SLICER
     " --full-slice                 slice away instructions that don't affect assertions\n" // NOLINT(*)
     " --property id                slice with respect to specific property only\n" // NOLINT(*)
     " --slice-global-inits         slice away initializations of unused global variables\n" // NOLINT(*)

src/goto-instrument/reachability_slicer.cpp

@@ -245,17 +245,15 @@ void reachability_slicer(
 /// Perform reachability slicing on goto_model for selected functions.
 /// \param goto_model Goto program to slice
 /// \param functions_list The functions relevant for the slicing (i.e. starting
-/// point for the search in the cfg). Anything that is reachable in the CFG
+/// point for the search in the CFG). Anything that is reachable in the CFG
 /// starting from these functions will be kept.
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::string &functions_list)
+  const std::list<std::string> &functions_list)
 {
-  std::istringstream functions_stream(functions_list);
-  std::string single_function;
-  while(std::getline(functions_stream, single_function, ','))
+  for(const auto &function : functions_list)
   {
-    in_function_criteriont matching_criterion(single_function);
+    in_function_criteriont matching_criterion(function);
     reachability_slicert slicer;
     slicer(goto_model.goto_functions, matching_criterion, true);
   }

src/goto-instrument/reachability_slicer.h

@@ -25,7 +25,7 @@ void reachability_slicer(
 
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
-  const std::string &functions_list);
+  const std::list<std::string> &functions_list);
 
 void reachability_slicer(
   goto_modelt &,
@@ -41,12 +41,16 @@ void reachability_slicer(
   "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
 
 #define HELP_REACHABILITY_SLICER                                               \
-  " --fp-reachability-slice <f>  remove instructions that cannot appear on a " \
-  "trace that visits all given functions. The list of functions has to be "    \
-  "given as a comma separated list.\n"                                         \
+  " --fp-reachability-slice f    remove instructions that cannot appear on a " \
+  "trace\n                              that visits all given functions. The " \
+  "list of\n                              functions has to be given as a "     \
+  "comma separated\n                              list f.\n"                   \
   " --reachability-slice         remove instructions that cannot appear on a " \
-  "trace from entry point to a property\n"                                     \
+  "trace\n                              from entry point to a property"        \
+  "\n" // NOLINT(*)
+#define HELP_REACHABILITY_SLICER_FB                                            \
   " --reachability-slice-fb      remove instructions that cannot appear on a " \
-  "trace from entry point through a property\n" // NOLINT(*)
+  "trace\n                              from entry point through a property"   \
+  "\n" // NOLINT(*)
 // clang-format on
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H

src/util/cmdline.cpp

@@ -118,6 +118,23 @@ const std::list<std::string> &cmdlinet::get_values(
     return immutable_empty_list;
 }
 
+std::list<std::string>
+cmdlinet::get_comma_separated_values(const char *option) const
+{
+  std::list<std::string> separated_values;
+  auto i = getoptnr(option);
+  if(i.has_value() && !options[*i].values.empty())
+  {
+    std::istringstream values_stream(options[*i].values.front());
+    std::string single_value;
+    while(std::getline(values_stream, single_value, ','))
+    {
+      separated_values.push_back(single_value);
+    }
+  }
+  return separated_values;
+}
+
 optionalt<std::size_t> cmdlinet::getoptnr(char option) const
 {
   for(std::size_t i=0; i<options.size(); i++)

src/util/cmdline.h

@@ -27,6 +27,8 @@ class cmdlinet
   const std::list<std::string> &get_values(const std::string &option) const;
   const std::list<std::string> &get_values(char option) const;
 
+  std::list<std::string> get_comma_separated_values(const char *option) const;
+
   virtual bool isset(char option) const;
   virtual bool isset(const char *option) const;
   virtual void set(const std::string &option);