File tree 6 files changed +84
-0
lines changed
variable-sensitivity-dependence-graph-01
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(
448
448
dependence_grapht *dep_graph=dynamic_cast <dependence_grapht*>(&ai);
449
449
assert (dep_graph!=nullptr );
450
450
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
+
451
470
// propagate control dependencies across function calls
452
471
if (from->is_function_call ())
453
472
{
@@ -477,6 +496,8 @@ void dep_graph_domaint::transform(
477
496
s->has_changed =true ;
478
497
479
498
control_deps.clear ();
499
+ control_deps.insert (std::make_pair (from, tvt::unknown ()));
500
+
480
501
control_dep_candidates.clear ();
481
502
}
482
503
}
Original file line number Diff line number Diff line change @@ -70,6 +70,25 @@ void variable_sensitivity_dependence_domaint::transform(
70
70
dynamic_cast <variable_sensitivity_dependence_grapht*>(&ai);
71
71
assert (dep_graph!=nullptr );
72
72
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
+
73
92
// propagate control dependencies across function calls
74
93
if (from->is_function_call ())
75
94
{
@@ -100,6 +119,8 @@ void variable_sensitivity_dependence_domaint::transform(
100
119
s->has_changed =true ;
101
120
102
121
control_deps.clear ();
122
+ control_deps.insert (std::make_pair (from, tvt::unknown ()));
123
+
103
124
control_dep_candidates.clear ();
104
125
}
105
126
}
You can’t perform that action at this time.
0 commit comments