File tree Expand file tree Collapse file tree 3 files changed +42
-0
lines changed
regression/goto-analyzer/dependence-graph13 Expand file tree Collapse file tree 3 files changed +42
-0
lines changed Original file line number Diff line number Diff line change 1+ void func ()
2+ {
3+
4+ }
5+
6+ void main (void )
7+ {
8+ func ();
9+ }
Original file line number Diff line number Diff line change 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
Original file line number Diff line number Diff 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 }
You can’t perform that action at this time.
0 commit comments