Go to the documentation of this file.
46 !directed_graph.empty(),
47 "at least " +
id2string(entry_point) +
" should be reachable");
53 for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
55 const irep_idt &
id = directed_graph[node_idx].function;
64 for(
const auto &i : it->second.body.instructions)
66 i.apply([&symbols_to_keep](
const exprt &expr) {
72 goto_functionst::function_mapt::iterator f_it;
81 bool fixed_point_reached =
false;
86 std::vector<bool> seen(goto_program.
instructions.size(),
false);
87 while(!fixed_point_reached)
89 fixed_point_reached =
true;
91 std::vector<bool>::iterator seen_it = seen.begin();
94 if(!*seen_it && i_it->is_assign())
103 symbols_to_keep.find(
id) != symbols_to_keep.end())
105 fixed_point_reached =
false;
120 if(i_it->is_assign())
128 symbols_to_keep.find(
id) == symbols_to_keep.end())
130 i_it->turn_into_skip();
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Base class for all expressions.
function_mapt function_map
Expression to hold a symbol (variable)
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
const std::string & id2string(const irep_idt &d)
const irep_idt & get_identifier() const
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void slice_global_inits(goto_modelt &goto_model)
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
goto_functionst goto_functions
GOTO functions.
std::unordered_set< irep_idt > find_symbols_sett
Goto Programs with Functions.
A generic container class for the GOTO intermediate representation of one function.
bool has_prefix(const std::string &s, const std::string &prefix)
Remove initializations of unused global variables.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A codet representing an assignment in the program.
API to expression classes.
#define forall_goto_program_instructions(it, program)