27 cfg_nodet():node_required(false)
32 #ifdef DEBUG_FULL_SLICERT
33 std::set<unsigned> required_by;
40 typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
41 typedef std::stack<cfgt::entryt> queuet;
43 inline void add_to_queue(
45 const cfgt::entryt &entry,
48 #ifdef DEBUG_FULL_SLICERT
49 cfg[entry].required_by.insert(reason->location_number);
69 for(cfgt::entry_mapt::iterator
74 if(criterion(e_it->first))
78 else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
79 e_it->first->is_throw())
80 jumps.push_back(e_it->second);
81 else if(e_it->first->is_decl())
84 decl_dead[s.get_identifier()].push(e_it->second);
86 else if(e_it->first->is_dead())
89 decl_dead[s.get_identifier()].push(e_it->second);
95 dep_graph(goto_functions, ns);
98 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
104 if(f_it->second.body_available())
109 if(!i_it->is_end_function() &&
110 !
cfg[e].node_required)
112 #ifdef DEBUG_FULL_SLICERT
117 for(std::set<unsigned>::const_iterator
118 req_it=
cfg[e].required_by.begin();
119 req_it!=
cfg[e].required_by.end();
122 if(req_it!=
cfg[e].required_by.begin())
126 i_it->source_location.set_column(c);
127 i_it->source_location.set_comment(c);
142 decl_deadt &decl_dead,
145 std::vector<cfgt::entryt> dep_node_to_cfg;
146 dep_node_to_cfg.reserve(dep_graph.
size());
147 for(
unsigned i=0; i<dep_graph.
size(); ++i)
149 cfgt::entry_mapt::const_iterator entry=
153 dep_node_to_cfg.push_back(entry->second);
157 while(!queue.empty())
159 while(!queue.empty())
166 if(node.node_required)
170 node.node_required=
true;
189 const cfgt::nodet &node,
192 const dep_node_to_cfgt &dep_node_to_cfg)
195 dep_graph[dep_graph[node.PC].get_node_id()];
197 for(dependence_grapht::edgest::const_iterator
198 it=d_node.
in.begin();
201 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
241 typedef std::map<goto_programt::const_targett, unsigned>
243 typedef std::map<irep_idt, goto_program_change_impactt>
293 bool _compact_output):
294 impact_mode(_impact_mode),
295 compact_output(_compact_output),
296 old_goto_functions(model_old.goto_functions),
297 ns_old(model_old.symbol_table),
298 new_goto_functions(model_new.goto_functions),
299 ns_new(model_new.symbol_table),
300 unified_diff(model_old, model_new),
301 old_dep_graph(ns_old),
302 new_dep_graph(ns_new)
322 goto_functionst::function_mapt::const_iterator old_fit=
324 goto_functionst::function_mapt::const_iterator new_fit=
332 old_fit->second.body;
336 new_fit->second.body;
358 for(
const auto &d : diff)
365 old_impact[o_it]|=
SAME;
367 assert(n_it==d.first);
368 new_impact[n_it]|=
SAME;
373 assert(o_it==d.first);
398 assert(n_it==d.first);
418 new_impact[n_it]|=
NEW;
432 for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
433 it != d_node.out.end(); ++it)
459 for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
460 it != d_node.in.end(); ++it)
487 goto_functionst::function_mapt::const_iterator>
490 function_mapt old_funcs, new_funcs;
493 old_funcs.insert(std::make_pair(it->first, it));
495 new_funcs.insert(std::make_pair(it->first, it));
497 function_mapt::const_iterator ito=old_funcs.begin();
498 for(function_mapt::const_iterator itn=new_funcs.begin();
499 itn!=new_funcs.end();
502 while(ito!=old_funcs.end() && ito->first<itn->first)
505 if(ito!=old_funcs.end() && itn->first==ito->first)
513 goto_functions_change_impactt::const_iterator oc_it=
515 for(goto_functions_change_impactt::const_iterator
537 assert(oc_it->first==nc_it->first);
559 goto_functionst::function_mapt::const_iterator f_it=
565 std::cout <<
"/** " <<
function <<
" **/\n";
569 goto_program_change_impactt::const_iterator c_entry=
571 const unsigned mod_flags =
572 c_entry == c_i.end() ? static_cast<unsigned>(
SAME) : c_entry->second;
581 else if(mod_flags&
NEW)
607 goto_functionst::function_mapt::const_iterator o_f_it=
612 goto_functionst::function_mapt::const_iterator f_it=
618 std::cout <<
"/** " <<
function <<
" **/\n";
624 goto_program_change_impactt::const_iterator o_c_entry=
625 o_c_i.find(o_target);
626 const unsigned old_mod_flags = o_c_entry == o_c_i.end()
627 ? static_cast<unsigned>(
SAME)
638 goto_program_change_impactt::const_iterator c_entry=
640 const unsigned mod_flags =
641 c_entry == n_c_i.end() ? static_cast<unsigned>(
SAME) : c_entry->second;
648 if(old_mod_flags==
SAME)
661 else if(mod_flags&
NEW)
667 assert(old_mod_flags==
SAME ||
676 assert(old_mod_flags==
SAME ||
687 o_target!=old_goto_program.instructions.end();
690 goto_program_change_impactt::const_iterator o_c_entry=
691 o_c_i.find(o_target);
692 const unsigned old_mod_flags = o_c_entry == o_c_i.end()
693 ? static_cast<unsigned>(
SAME)
699 if(old_mod_flags==
SAME)
703 else if(old_mod_flags&
NEW)
726 const irep_idt &
file=target->source_location.get_file();
727 const irep_idt &line=target->source_location.get_line();
745 change_impactt c(model_old, model_new, impact_mode, compact_output);