44 "at least " +
id2string(entry_point) +
" should be reachable");
61 for(
const auto &i : it->second.body.instructions)
69 goto_functionst::function_mapt::iterator
f_it;
83 std::vector<bool> seen(goto_program.
instructions.size(),
false);
88 std::vector<bool>::iterator
seen_it = seen.begin();
91 if(!*
seen_it && instruction.is_assign())
115 bool changed =
false;
121 it->second.is_static_lifetime && !it->second.is_type &&
122 !it->second.is_macro && it->second.type.id() !=
ID_code &&
126 symbolt &symbol = it.get_writeable_symbol();
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
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.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
void set(const irep_idt &name, const irep_idt &value)
virtual iteratort begin() override
virtual iteratort end() override
exprt value
Initial value of symbol.
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
std::unordered_set< irep_idt > find_symbols_sett
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
void slice_global_inits(goto_modelt &goto_model, message_handlert &message_handler)
Remove initialization of global variables that are not used in any function reachable from the entry ...
Remove initializations of unused global variables.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.