Reachability slice requires function bodies

Reachability slicing relies on the CFG. The CFG, however, will not
contain edges from a function call to the next instruction when no body
is available for the function call. Therefore, reachability slicing
requires two steps:

- The model library needs to be applied. CBMC already did so,
goto-instrument now does with this commit.
- Remaining function calls without body need to be replaced by
nondet-return-value assignments.

Fixes: #6394

Author: tautschnig

regression/goto-instrument/reachability-slice/main.c

@@ -0,0 +1,21 @@
+#include <stdlib.h>
+
+void undefined_function();
+
+void a()
+{
+  undefined_function();
+}
+
+void b()
+{
+  int should_be_sliced_away;
+}
+
+int main()
+{
+  int *p = malloc(sizeof(int));
+  a();
+  __CPROVER_assert(0, "reach me");
+  b();
+}

regression/goto-instrument/reachability-slice/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--reachability-slice
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+should_be_sliced_away

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1066,8 +1066,11 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // we add the library in some cases, as some analyses benefit
 
-  if(cmdline.isset("add-library") ||
-     cmdline.isset("mm"))
+  if(
+    cmdline.isset("add-library") || cmdline.isset("mm") ||
+    cmdline.isset("reachability-slice") ||
+    cmdline.isset("reachability-slice-fb") ||
+    cmdline.isset("fp-reachability-slice"))
   {
     if(cmdline.isset("show-custom-bitvector-analysis") ||
        cmdline.isset("custom-bitvector-analysis"))

src/goto-instrument/reachability_slicer.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 /// from the criterion).
 
 #include "full_slicer_class.h"
-#include "reachability_slicer.h"
 #include "reachability_slicer_class.h"
 
 #include <util/exception_utils.h>
@@ -26,11 +25,20 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/is_threaded.h>
 
+#include "reachability_slicer.h"
+
 void reachability_slicert::operator()(
   goto_functionst &goto_functions,
   const slicing_criteriont &criterion,
   bool include_forward_reachability)
 {
+  // Replace function calls without body by non-deterministic return values to
+  // ensure the CFG does not consider instructions after such a call to be
+  // unreachable.
+  remove_calls_no_bodyt remove_calls_no_body;
+  remove_calls_no_body(goto_functions);
+  goto_functions.update();
+
   cfg(goto_functions);
   for(const auto &gf_entry : goto_functions.function_map)
   {