diff --git a/regression/cbmc/Pointer18/full-slice.desc b/regression/cbmc/Pointer18/full-slice.desc new file mode 100644 index 00000000000..37c7526ffee --- /dev/null +++ b/regression/cbmc/Pointer18/full-slice.desc @@ -0,0 +1,8 @@ +CORE +main.c +--unwind 1 --no-unwinding-assertions --pointer-check --full-slice +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index c57bdeb7289..cb2e30eb946 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -224,55 +224,38 @@ void dep_graph_domaint::transform( // We do not propagate control dependencies on function calls, i.e., only the // entry point of a function should have a control dependency on the call - if(!control_deps.empty()) - { - const goto_programt::const_targett &dep = *control_deps.begin(); - if(dep->is_function_call()) - { - INVARIANT( - std::all_of( - std::next(control_deps.begin()), - control_deps.end(), - [](const goto_programt::const_targett &d) { - return d->is_function_call(); - }), - "All entries must be function calls"); - - control_deps.clear(); - } - } + depst filtered_control_deps; + std::copy_if( + control_deps.begin(), + control_deps.end(), + std::inserter(filtered_control_deps, filtered_control_deps.end()), + [](goto_programt::const_targett dep) { return !dep->is_function_call(); }); + control_deps = std::move(filtered_control_deps); // propagate control dependencies across function calls - if(from->is_function_call()) + if(from->is_function_call() && function_from != function_to) { - if(function_from == function_to) - { - control_dependencies(function_from, from, to, *dep_graph); - } - else - { - // edge to function entry point - const goto_programt::const_targett next = std::next(from); + // edge to function entry point + const goto_programt::const_targett next = std::next(from); - dep_graph_domaint *s= - dynamic_cast(&(dep_graph->get_state(next))); - assert(s!=nullptr); + dep_graph_domaint *s = + dynamic_cast(&(dep_graph->get_state(next))); + CHECK_RETURN(s != nullptr); - if(s->is_bottom()) - { - s->has_values = tvt::unknown(); - s->has_changed = true; - } + if(s->is_bottom()) + { + s->has_values = tvt::unknown(); + s->has_changed = true; + } - s->has_changed |= util_inplace_set_union(s->control_deps, control_deps); - s->has_changed |= util_inplace_set_union( - s->control_dep_candidates, control_dep_candidates); + s->has_changed |= util_inplace_set_union(s->control_deps, control_deps); + s->has_changed |= + util_inplace_set_union(s->control_dep_candidates, control_dep_candidates); - control_deps.clear(); - control_deps.insert(from); + control_deps.clear(); + control_deps.insert(from); - control_dep_candidates.clear(); - } + control_dep_candidates.clear(); } else control_dependencies(function_from, from, to, *dep_graph);