Merge pull request #5391 from martin-cs/VSD/dependency-graph

Add control dependencies on function call

Author: martin-cs

regression/goto-analyzer/dependence-graph13/main.c

@@ -0,0 +1,8 @@
+void func()
+{
+}
+
+void main(void)
+{
+  func();
+}

regression/goto-analyzer/dependence-graph13/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+--show --dependence-graph
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+Function: main\n.*\n.*\n.*\nControl dependencies: [0-9]+
+Function: func\n.*\n.*\n.*\nControl dependencies: [0-9]+
+Function: __CPROVER_initialize\n.*\n.*\n.*\nControl dependencies: [0-9]+
+--
+Function: __CPROVER__start\n.*\n.*\n.*\nControl dependencies: [0-9]+
+^warning: ignoring

src/analyses/dependence_graph.cpp

@@ -203,6 +203,26 @@ void dep_graph_domaint::transform(
   dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
   assert(dep_graph!=nullptr);
 
+  // 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();
+    }
+  }
+
   // propagate control dependencies across function calls
   if(from->is_function_call())
   {
@@ -230,6 +250,8 @@ void dep_graph_domaint::transform(
         s->control_dep_candidates, control_dep_candidates);
 
       control_deps.clear();
+      control_deps.insert(from);
+
       control_dep_candidates.clear();
     }
   }