Skip to content

Commit 044f298

Browse files
danpoemartin
authored and
martin
committed
Add control dependencies from function call to function entry point for old dependency graph
1 parent df2638c commit 044f298

File tree

3 files changed

+42
-0
lines changed

3 files changed

+42
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
void func()
2+
{
3+
4+
}
5+
6+
void main(void)
7+
{
8+
func();
9+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--show --dependence-graph
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
Function: main\n.*\n.*\n.*\nControl dependencies: [0-9]+
8+
Function: func\n.*\n.*\n.*\nControl dependencies: [0-9]+
9+
Function: __CPROVER_initialize\n.*\n.*\n.*\nControl dependencies: [0-9]+
10+
--
11+
Function: __CPROVER__start\n.*\n.*\n.*\nControl dependencies: [0-9]+
12+
^warning: ignoring

src/analyses/dependence_graph.cpp

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -203,6 +203,25 @@ void dep_graph_domaint::transform(
203203
dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
204204
assert(dep_graph!=nullptr);
205205

206+
// We do not propagate control dependencies on function calls, i.e., only the
207+
// entry point of a function should have a control dependency on the call
208+
if(!control_deps.empty())
209+
{
210+
const goto_programt::const_targett &dep = *control_deps.begin();
211+
if(dep->is_function_call())
212+
{
213+
INVARIANT(
214+
std::all_of(
215+
std::next(control_deps.begin()),
216+
control_deps.end(),
217+
[](const goto_programt::const_targett &d)
218+
{ return d->is_function_call(); }),
219+
"All entries must be function calls");
220+
221+
control_deps.clear();
222+
}
223+
}
224+
206225
// propagate control dependencies across function calls
207226
if(from->is_function_call())
208227
{
@@ -230,6 +249,8 @@ void dep_graph_domaint::transform(
230249
s->control_dep_candidates, control_dep_candidates);
231250

232251
control_deps.clear();
252+
control_deps.insert(from);
253+
233254
control_dep_candidates.clear();
234255
}
235256
}

0 commit comments

Comments
 (0)