36 throw "entry point not found";
44 !directed_graph.empty(),
"At least __CPROVER_start should be reachable");
50 for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
52 const irep_idt &
id = directed_graph[node_idx].function;
65 const codet &code = i_it->code;
67 const exprt &expr = i_it->guard;
74 goto_functionst::function_mapt::iterator f_it;
89 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
#define INVARIANT(CONDITION, REASON)
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)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic 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()
Base class for all expressions.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
goto_programt & goto_program
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
A statement in a programming language.
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.