17 #ifdef DEBUG_FULL_SLICERT 23 const cfgt::nodet &node,
29 dep_graph[dep_graph[node.PC].get_node_id()];
31 for(dependence_grapht::edgest::const_iterator
35 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
39 const cfgt::nodet &node,
43 goto_functionst::function_mapt::const_iterator f_it=
47 assert(!f_it->second.body.instructions.empty());
49 f_it->second.body.instructions.begin();
51 cfgt::entry_mapt::const_iterator entry=
55 for(cfgt::edgest::const_iterator
56 it=
cfg[entry->second].
in.begin();
57 it!=
cfg[entry->second].
in.end();
63 const cfgt::nodet &node,
74 for(find_symbols_sett::const_iterator
79 decl_deadt::iterator entry=decl_dead.find(*it);
80 if(entry==decl_dead.end())
83 while(!entry->second.empty())
89 decl_dead.erase(entry);
123 jumpst::iterator next=it;
138 for( ; !lex_succ->is_end_function(); ++lex_succ)
140 cfgt::entry_mapt::const_iterator entry=
144 if(
cfg[entry->second].node_required)
147 if(lex_succ->is_end_function())
156 cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
165 if(n.dominators.find(lex_succ)==n.dominators.end())
175 std::size_t post_dom_size=0;
176 for(cfg_dominatorst::target_sett::const_iterator
177 d_it=n.dominators.begin();
178 d_it!=n.dominators.end();
181 cfgt::entry_mapt::const_iterator entry=
185 if(
cfg[entry->second].node_required)
187 const irep_idt id2=(*d_it)->function;
189 "goto/jump expected to be within a single function");
191 cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2=
199 if(n2.dominators.size()>post_dom_size)
202 post_dom_size=n2.dominators.
size();
206 if(nearest!=lex_succ)
224 std::vector<cfgt::entryt> dep_node_to_cfg;
225 dep_node_to_cfg.reserve(dep_graph.
size());
228 cfgt::entry_mapt::const_iterator entry=
232 dep_node_to_cfg.push_back(entry->second);
236 while(!queue.empty())
238 while(!queue.empty())
245 if(node.node_required)
249 node.node_required=
true;
270 const irep_idt &statement=target->code.get_statement();
271 if(statement==ID_array_copy)
274 if(!target->is_assign())
278 if(a.
lhs().
id()!=ID_symbol)
301 for(cfgt::entry_mapt::iterator
310 else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
311 e_it->first->is_throw())
312 jumps.push_back(e_it->second);
313 else if(e_it->first->is_decl())
318 else if(e_it->first->is_dead())
327 dep_graph(goto_functions, ns);
330 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
336 if(f_it->second.body_available())
341 if(!i_it->is_end_function() &&
342 !
cfg[e].node_required)
344 #ifdef DEBUG_FULL_SLICERT 349 for(std::set<unsigned>::const_iterator
350 req_it=
cfg[e].required_by.begin();
351 req_it!=
cfg[e].required_by.end();
354 if(req_it!=
cfg[e].required_by.begin())
358 i_it->source_location.set_column(c);
359 i_it->source_location.set_comment(c);
395 const std::list<std::string> &properties)
403 const std::list<std::string> &properties)
const code_declt & to_code_decl(const codet &code)
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
const code_deadt & to_code_dead(const codet &code)
virtual ~slicing_criteriont()
const irep_idt & get_identifier() const
std::unordered_map< irep_idt, queuet > decl_deadt
static bool implicit(goto_programt::const_targett target)
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
#define INVARIANT(CONDITION, REASON)
const code_assignt & to_code_assign(const codet &code)
const irep_idt & id() const
std::stack< cfgt::entryt > queuet
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
instructionst::const_iterator const_targett
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
std::list< cfgt::entryt > jumpst
const post_dominators_mapt & cfg_post_dominators() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
nodet::node_indext node_indext
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
goto_programt coverage_criteriont criterion
const edgest & in(node_indext n) const
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
std::unordered_set< irep_idt > find_symbols_sett
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
std::vector< cfgt::entryt > dep_node_to_cfgt
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.