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;
68 const codet &code = i_it->code;
70 const exprt &expr = i_it->guard;
77 goto_functionst::function_mapt::iterator f_it;
93 symbols.find(
id)==symbols.end())
const std::string & id2string(const irep_idt &d)
Remove initializations of unused global variables.
const irep_idt & get_identifier() const
Goto Programs with Functions.
function_mapt function_map
const code_assignt & to_code_assign(const codet &code)
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms...
#define INITIALIZE_FUNCTION
API to expression classes.
void slice_global_inits(goto_modelt &goto_model)
bool has_prefix(const std::string &s, const std::string &prefix)
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A generic container class for the GOTO intermediate representation of one function.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
Data structure for representing an arbitrary statement in a program.
std::unordered_set< irep_idt > find_symbols_sett
#define forall_goto_program_instructions(it, program)
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
A codet representing an assignment in the program.