Fix based on comments

Author: Petr Bauch

regression/goto-instrument/fp-reachability-slice1/test.desc

@@ -3,6 +3,9 @@ main.c
 --fp-reachability-slice c
 ^EXIT=0$
 ^SIGNAL=0$
+1: ASSUME FALSE
+dead e;
+dead d;
 --
 ^warning: ignoring
 dead f;

regression/goto-instrument/fp-reachability-slice3/test.desc

@@ -3,7 +3,9 @@ main.c
 --fp-reachability-slice b,c
 ^EXIT=0$
 ^SIGNAL=0$
+1 file main.c line 34
 --
 ^warning: ignoring
 dead d;
+dead e;
 dead f;

src/goto-instrument/reachability_slicer.cpp

@@ -89,12 +89,12 @@ void reachability_slicert::fixedpoint_to_assertions(
       {
         // This is an end-of-function -> successor-of-callsite edge.
         // Queue both the caller and the end of the callee.
-        if(std::prev(node.PC)->is_function_call())
-        {
-          stack.emplace_back(edge.first, true);
-          stack.emplace_back(
-            cfg.entry_map[std::prev(node.PC)], caller_is_known);
-        }
+        INVARIANT(
+          std::prev(node.PC)->is_function_call(),
+          "all function return edges should point to the successor of a "
+          "FUNCTION_CALL instruction");
+        stack.emplace_back(edge.first, true);
+        stack.emplace_back(cfg.entry_map[std::prev(node.PC)], caller_is_known);
       }
       else if(pred_node.PC->is_function_call())
       {
@@ -200,7 +200,6 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
           !e.reaches_assertion && !e.reachable_from_assertion &&
           !i_it->is_end_function())
           i_it->make_assumption(false_exprt());
-        e.reaches_assertion = e.reachable_from_assertion = false;
       }
 
       // replace unreachable code by skip
@@ -245,21 +244,20 @@ void reachability_slicer(
 
 /// Perform reachability slicing on goto_model for selected functions.
 /// \param goto_model Goto program to slice
-/// \param functions The functions relevant for the slicing (i.e. starting
+/// \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
 /// starting from these functions will be kept.
 void function_path_reachability_slicer(
   goto_modelt &goto_model,
   const std::string &functions_list)
 {
-  reachability_slicert s;
-
-  std::istringstream multiple_functions(functions_list);
+  std::istringstream functions_stream(functions_list);
   std::string single_function;
-  while(std::getline(multiple_functions, single_function, ','))
+  while(std::getline(functions_stream, single_function, ','))
   {
-    in_function_criteriont p(single_function);
-    s(goto_model.goto_functions, p, true);
+    in_function_criteriont matching_criterion(single_function);
+    reachability_slicert slicer;
+    slicer(goto_model.goto_functions, matching_criterion, true);
   }
 
   remove_calls_no_bodyt remove_calls_no_body;