diff --git a/regression/goto-instrument/reaching-definitions/test.desc b/regression/goto-instrument/reaching-definitions/test.desc new file mode 100644 index 00000000000..7c499b184ec --- /dev/null +++ b/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. diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index a8634a5e9bd..d7ffa9bc26a 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/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);