36 for(
const exprt &argument : arguments)
40 t->source_location = target->source_location;
41 t->function = target->function;
54 t->source_location = target->source_location;
55 t->function = target->function;
75 if(!target->is_function_call())
81 if(f.
id() != ID_symbol)
87 goto_functionst::function_mapt::const_iterator f_it =
92 return !f_it->second.body_available();
130 (*this)(f_it->second.body, goto_functions);
const irep_idt & get_identifier() const
Goto Programs with Functions.
Remove calls to functions without a body.
function_mapt function_map
void operator()(goto_programt &goto_program, const goto_functionst &goto_functions)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
bool is_opaque_function_call(const goto_programt::const_targett target, const goto_functionst &goto_functions)
Check if instruction is a call to an opaque function through an ordinary (non-function pointer) call...
const irep_idt & id() const
instructionst::iterator targett
instructionst instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
#define PRECONDITION(CONDITION)
A side effect that returns a non-deterministically chosen value.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program at the given location.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
std::vector< exprt > operandst
A generic container class for the GOTO intermediate representation of one function.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single call.
#define Forall_goto_functions(it, functions)
bool empty() const
Is the program empty?
goto_programt & goto_program
source_locationt & add_source_location()
Expression to hold a symbol (variable)
const code_function_callt & to_code_function_call(const codet &code)