Skip to content

Commit 512ae33

Browse files
committed
Add control dependencies from function call to function entry point for new dependency graph
1 parent b7a6c80 commit 512ae33

File tree

3 files changed

+42
-0
lines changed

3 files changed

+42
-0
lines changed
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+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--show --dependence-graph-vs
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/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

+21
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,25 @@ void variable_sensitivity_dependence_domaint::transform(
7070
dynamic_cast<variable_sensitivity_dependence_grapht*>(&ai);
7171
assert(dep_graph!=nullptr);
7272

73+
// We do not propagate control dependencies on function calls, i.e., only the
74+
// entry point of a function should have a control dependency on the call
75+
if(!control_deps.empty())
76+
{
77+
const goto_programt::const_targett &dep = control_deps.begin()->first;
78+
if(dep->is_function_call())
79+
{
80+
INVARIANT(
81+
std::all_of(
82+
std::next(control_deps.begin()),
83+
control_deps.end(),
84+
[](const std::pair<const goto_programt::const_targett, tvt> &d)
85+
{ return d.first->is_function_call(); }),
86+
"All entries must be function calls");
87+
88+
control_deps.clear();
89+
}
90+
}
91+
7392
// propagate control dependencies across function calls
7493
if(from->is_function_call())
7594
{
@@ -100,6 +119,8 @@ void variable_sensitivity_dependence_domaint::transform(
100119
s->has_changed=true;
101120

102121
control_deps.clear();
122+
control_deps.insert(std::make_pair(from, tvt::unknown()));
123+
103124
control_dep_candidates.clear();
104125
}
105126
}

0 commit comments

Comments
 (0)