Merge pull request #6721 from tautschnig/bugfixes/control-deps

Dependence graph: entry points may have additional control dependencies

Author: tautschnig

regression/cbmc/Pointer18/full-slice.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 1 --no-unwinding-assertions --pointer-check --full-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/analyses/dependence_graph.cpp

@@ -224,55 +224,38 @@ void dep_graph_domaint::transform(
 
   // We do not propagate control dependencies on function calls, i.e., only the
   // entry point of a function should have a control dependency on the call
-  if(!control_deps.empty())
-  {
-    const goto_programt::const_targett &dep = *control_deps.begin();
-    if(dep->is_function_call())
-    {
-      INVARIANT(
-        std::all_of(
-          std::next(control_deps.begin()),
-          control_deps.end(),
-          [](const goto_programt::const_targett &d) {
-            return d->is_function_call();
-          }),
-        "All entries must be function calls");
-
-      control_deps.clear();
-    }
-  }
+  depst filtered_control_deps;
+  std::copy_if(
+    control_deps.begin(),
+    control_deps.end(),
+    std::inserter(filtered_control_deps, filtered_control_deps.end()),
+    [](goto_programt::const_targett dep) { return !dep->is_function_call(); });
+  control_deps = std::move(filtered_control_deps);
 
   // propagate control dependencies across function calls
-  if(from->is_function_call())
+  if(from->is_function_call() && function_from != function_to)
   {
-    if(function_from == function_to)
-    {
-      control_dependencies(function_from, from, to, *dep_graph);
-    }
-    else
-    {
-      // edge to function entry point
-      const goto_programt::const_targett next = std::next(from);
+    // edge to function entry point
+    const goto_programt::const_targett next = std::next(from);
 
-      dep_graph_domaint *s=
-        dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
-      assert(s!=nullptr);
+    dep_graph_domaint *s =
+      dynamic_cast<dep_graph_domaint *>(&(dep_graph->get_state(next)));
+    CHECK_RETURN(s != nullptr);
 
-      if(s->is_bottom())
-      {
-        s->has_values = tvt::unknown();
-        s->has_changed = true;
-      }
+    if(s->is_bottom())
+    {
+      s->has_values = tvt::unknown();
+      s->has_changed = true;
+    }
 
-      s->has_changed |= util_inplace_set_union(s->control_deps, control_deps);
-      s->has_changed |= util_inplace_set_union(
-        s->control_dep_candidates, control_dep_candidates);
+    s->has_changed |= util_inplace_set_union(s->control_deps, control_deps);
+    s->has_changed |=
+      util_inplace_set_union(s->control_dep_candidates, control_dep_candidates);
 
-      control_deps.clear();
-      control_deps.insert(from);
+    control_deps.clear();
+    control_deps.insert(from);
 
-      control_dep_candidates.clear();
-    }
+    control_dep_candidates.clear();
   }
   else
     control_dependencies(function_from, from, to, *dep_graph);