File tree Expand file tree Collapse file tree 3 files changed +42
-0
lines changed
regression/goto-analyzer/variable-sensitivity-dependence-graph-01
src/analyses/variable-sensitivity 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-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
Original file line number Diff line number Diff 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 }
You can’t perform that action at this time.
0 commit comments