File tree Expand file tree Collapse file tree 6 files changed +84
-0
lines changed
variable-sensitivity-dependence-graph-01 Expand file tree Collapse file tree 6 files changed +84
-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 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 @@ -448,6 +448,25 @@ void dep_graph_domaint::transform(
448448 dependence_grapht *dep_graph=dynamic_cast <dependence_grapht*>(&ai);
449449 assert (dep_graph!=nullptr );
450450
451+ // We do not propagate control dependencies on function calls, i.e., only the
452+ // entry point of a function should have a control dependency on the call
453+ if (!control_deps.empty ())
454+ {
455+ const goto_programt::const_targett &dep = control_deps.begin ()->first ;
456+ if (dep->is_function_call ())
457+ {
458+ INVARIANT (
459+ std::all_of (
460+ std::next (control_deps.begin ()),
461+ control_deps.end (),
462+ [](const std::pair<const goto_programt::const_targett, tvt> &d)
463+ { return d.first ->is_function_call (); }),
464+ " All entries must be function calls" );
465+
466+ control_deps.clear ();
467+ }
468+ }
469+
451470 // propagate control dependencies across function calls
452471 if (from->is_function_call ())
453472 {
@@ -477,6 +496,8 @@ void dep_graph_domaint::transform(
477496 s->has_changed =true ;
478497
479498 control_deps.clear ();
499+ control_deps.insert (std::make_pair (from, tvt::unknown ()));
500+
480501 control_dep_candidates.clear ();
481502 }
482503 }
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