Merge pull request #6720 from tautschnig/bugfixes/reach-def-recursion

Reaching definitions: distinguish recursion from function-without-body

Author: tautschnig

regression/goto-instrument/reaching-definitions/test.desc

@@ -0,0 +1,13 @@
+CORE
+../../cbmc/Recursion6/main.c
+--show-reaching-definitions
+activate-multi-line-match
+recursion::1::some_local\[0:32@\d+\]\n(\s+(__CPROVER|recursion).*\n)*\s*\n\s+//.*\n\s+ASSERT .*recursion::1::some_local = 1
+^EXIT=0$
+^SIGNAL=0$
+--
+^FALSE
+--
+Reaching definitions must not confuse recursion and functions without body, both
+of which yield transform calls where the to and from have the same function
+identifier.

src/analyses/reaching_definitions.cpp

@@ -181,7 +181,8 @@ void rd_range_domaint::transform_function_call(
   reaching_definitions_analysist &rd)
 {
   // only if there is an actual call, i.e., we have a body
-  if(function_from != function_to)
+  const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
+  if(function_to == fn_symbol_expr.get_identifier())
   {
     for(valuest::iterator it=values.begin();
         it!=values.end();
@@ -206,7 +207,6 @@ void rd_range_domaint::transform_function_call(
         ++it;
     }
 
-    const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
     const code_typet &code_type=
       to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);