Fix reachability slicer when used with recursive or unreachable functions

Author: tautschnig

regression/cbmc/reachability-slice-interproc2/main.c

@@ -0,0 +1,23 @@
+void b();
+
+void c()
+{
+  __CPROVER_assert(0, "");
+  b();
+}
+
+void b()
+{
+  a();
+  c();
+}
+
+void a()
+{
+  c();
+}
+
+int main()
+{
+  a();
+}

regression/cbmc/reachability-slice-interproc2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--reachability-slice --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+main\(\)
+--
+^warning: ignoring

src/goto-instrument/reachability_slicer.cpp

@@ -74,9 +74,13 @@ void reachability_slicert::fixedpoint_to_assertions(
     const auto caller_is_known = stack.back().caller_is_known;
     stack.pop_back();
 
-    if(node.reaches_assertion)
+    if(
+      node.reaches_assertion.is_true() ||
+      (caller_is_known && node.reaches_assertion.is_unknown()))
+    {
       continue;
-    node.reaches_assertion = true;
+    }
+    node.reaches_assertion = caller_is_known ? tvt::unknown() : tvt(true);
 
     for(const auto &edge : node.in)
     {
@@ -195,7 +199,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions)
       {
         const cfgt::nodet &e=cfg[cfg.entry_map[i_it]];
         if(
-          !e.reaches_assertion && !e.reachable_from_assertion &&
+          e.reaches_assertion.is_false() && !e.reachable_from_assertion &&
           !i_it->is_end_function())
           i_it->make_assumption(false_exprt());
       }

src/goto-instrument/reachability_slicer_class.h

@@ -38,11 +38,12 @@ class reachability_slicert
 protected:
   struct slicer_entryt
   {
-    slicer_entryt() : reaches_assertion(false), reachable_from_assertion(false)
+    slicer_entryt()
+      : reaches_assertion(tvt(false)), reachable_from_assertion(false)
     {
     }
 
-    bool reaches_assertion;
+    tvt reaches_assertion;
     bool reachable_from_assertion;
   };