Skip to content

Commit ecc813d

Browse files
committed
Dependence graph: entry points may have additional control dependencies
The first instruction of a function can reasonably have control dependencies other than that of the function call. Pointer18 is such an example, because there is a back edge to the beginning of the main function.
1 parent 7127c4d commit ecc813d

File tree

2 files changed

+15
-17
lines changed

2 files changed

+15
-17
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--unwind 1 --no-unwinding-assertions --pointer-check --full-slice
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

src/analyses/dependence_graph.cpp

Lines changed: 7 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -224,23 +224,13 @@ void dep_graph_domaint::transform(
224224

225225
// We do not propagate control dependencies on function calls, i.e., only the
226226
// entry point of a function should have a control dependency on the call
227-
if(!control_deps.empty())
228-
{
229-
const goto_programt::const_targett &dep = *control_deps.begin();
230-
if(dep->is_function_call())
231-
{
232-
INVARIANT(
233-
std::all_of(
234-
std::next(control_deps.begin()),
235-
control_deps.end(),
236-
[](const goto_programt::const_targett &d) {
237-
return d->is_function_call();
238-
}),
239-
"All entries must be function calls");
240-
241-
control_deps.clear();
242-
}
243-
}
227+
depst filtered_control_deps;
228+
std::copy_if(
229+
control_deps.begin(),
230+
control_deps.end(),
231+
std::inserter(filtered_control_deps, filtered_control_deps.end()),
232+
[](goto_programt::const_targett dep) { return !dep->is_function_call(); });
233+
control_deps = std::move(filtered_control_deps);
244234

245235
// propagate control dependencies across function calls
246236
if(from->is_function_call())

0 commit comments

Comments
 (0)