File tree 3 files changed +42
-0
lines changed
regression/goto-analyzer/dependence-graph13
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 @@ -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
}
You can’t perform that action at this time.
0 commit comments