38 for(
const exprt &argument : arguments)
70 if(!target->is_function_call())
73 const exprt &f = target->call_function();
75 if(f.
id() != ID_symbol)
81 goto_functionst::function_mapt::const_iterator f_it =
86 return !f_it->second.body_available();
110 log.status() <<
"Removing call to "
114 goto_program, it, it->call_lhs(), it->call_arguments());
134 (*this)(gf_entry.second.body, goto_functions, message_handler);
A goto_instruction_codet representing an assignment in the program.
codet representation of an expression statement.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
const source_locationt & source_location() const
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
instructionst::iterator targett
instructionst::const_iterator const_targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
static instructiont make_location(const source_locationt &l)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
bool empty() const
Is the program empty?
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
void remove_call_no_body(goto_programt &dest, goto_programt::targett target, const exprt &lhs, const exprt::operandst &arguments)
Remove a single call.
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.
void operator()(goto_programt &goto_program, const goto_functionst &goto_functions, message_handlert &)
Remove calls to functions without a body and replace them with evaluations of the arguments of the ca...
A side_effect_exprt that returns a non-deterministically chosen value.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const source_locationt & source_location() const
Goto Programs with Functions.
Remove calls to functions without a body.
#define PRECONDITION(CONDITION)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.