30 for(dependence_grapht::edgest::const_iterator
42 goto_functionst::function_mapt::const_iterator
f_it =
46 assert(!
f_it->second.body.instructions.empty());
48 f_it->second.body.instructions.begin();
51 for(
const auto &
in_edge : entry.in)
67 for(find_symbols_sett::const_iterator
72 decl_deadt::iterator entry=
decl_dead.find(*it);
76 while(!entry->second.empty())
116 jumpst::iterator next=it;
159 for(cfg_dominatorst::target_sett::const_iterator d_it =
165 if(node.node_required)
169 "goto/jump expected to be within a single function");
205 while(!queue.empty())
207 while(!queue.empty())
214 if(node.node_required)
218 node.node_required=
true;
239 const irep_idt &statement = target->get_code().get_statement();
243 if(!target->is_assign())
284 (instruction->is_goto() && instruction->get_condition().is_true()) ||
285 instruction->is_throw())
287 else if(instruction->is_decl())
289 const auto &s = instruction->decl_symbol();
292 else if(instruction->is_dead())
294 const auto &s = instruction->dead_symbol();
311 if(
gf_entry.second.body_available())
317 !
i_it->is_end_function() &&
320 i_it->turn_into_skip();
322#ifdef DEBUG_FULL_SLICERT
325 std::string
c=
"ins:"+std::to_string(
i_it->location_number);
327 for(std::set<unsigned>::const_iterator
req_it =
336 i_it->source_location.set_column(
c);
337 i_it->source_location.set_comment(
c);
374 const std::list<std::string> &properties)
382 const std::list<std::string> &properties)
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
base_grapht::node_indext entryt
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
std::list< cfgt::entryt > jumpst
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::unordered_map< irep_idt, queuet > decl_deadt
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
std::stack< cfgt::entryt > queuet
std::vector< cfgt::entryt > dep_node_to_cfgt
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
instructionst::const_iterator const_targett
nodet::node_indext node_indext
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual ~slicing_criteriont()
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
std::unordered_set< irep_idt > find_symbols_sett
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
static bool implicit(goto_programt::const_targett target)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.