Skip to content

Commit 70779ad

Browse files
committed
Reaching definitions: distinguish recursion from function-without-body
Comparing function names addressed the problem of comparing iterators over distinct objects (b2fba97), but resulted in possible confusion of recursion vs calling a function that doesn't have a body.
1 parent 7127c4d commit 70779ad

File tree

2 files changed

+15
-2
lines changed

2 files changed

+15
-2
lines changed
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
../../cbmc/Recursion6/main.c
3+
--show-reaching-definitions
4+
activate-multi-line-match
5+
recursion::1::some_local\[0:32@\d+\]\n(\s+(__CPROVER|recursion).*\n)*\s*\n\s+//.*\n\s+ASSERT .*recursion::1::some_local = 1
6+
^EXIT=0$
7+
^SIGNAL=0$
8+
--
9+
^FALSE
10+
--
11+
Reaching definitions must not confuse recursion and functions without body, both
12+
of which yield transform calls where the to and from have the same function
13+
identifier.

src/analyses/reaching_definitions.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,8 @@ void rd_range_domaint::transform_function_call(
181181
reaching_definitions_analysist &rd)
182182
{
183183
// only if there is an actual call, i.e., we have a body
184-
if(function_from != function_to)
184+
const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
185+
if(function_to == fn_symbol_expr.get_identifier())
185186
{
186187
for(valuest::iterator it=values.begin();
187188
it!=values.end();
@@ -206,7 +207,6 @@ void rd_range_domaint::transform_function_call(
206207
++it;
207208
}
208209

209-
const symbol_exprt &fn_symbol_expr = to_symbol_expr(from->call_function());
210210
const code_typet &code_type=
211211
to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type);
212212

0 commit comments

Comments
 (0)