slicer: add function path to goto-instrument

This commit adds the command line argument handling for the
function path slicer.

To keep all possible exeuction traces that hit both function a and b, an
example invocation could look as follows:

goto-instrument --fp-reachability-slice a:b input output

Note, any trace that touches only a, but not b, will not be kept in the
program.

Author: nmanthey

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1430,6 +1430,15 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       reachability_slicer(goto_model);
   }
 
+  if(cmdline.isset("fp-reachability-slice"))
+  {
+    do_indirect_call_and_rtti_removal();
+
+    status() << "Performing a function pointer reachability slice" << eom;
+    function_path_reachability_slicer(
+      goto_model, cmdline.get_values("fp-reachability-slice"));
+  }
+
   // full slice?
   if(cmdline.isset("full-slice"))
   {
@@ -1610,6 +1619,9 @@ 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 colon separated list.\n"
     " --reachability-slice         slice away instructions that can't reach assertions\n" // NOLINT(*)
     " --full-slice                 slice away instructions that don't affect assertions\n" // NOLINT(*)
     " --property id                slice with respect to specific property only\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -71,6 +71,7 @@ Author: Daniel Kroening, [email protected]
   "(show-struct-alignment)(interval-analysis)(show-intervals)" \
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(reachability-slice)(slice-global-inits)" \
+  "(fp-reachability-slice):" \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \