Go to the documentation of this file.
36 for(
const exprt &argument : arguments)
40 t->source_location = target->source_location;
41 t->function = target->function;
53 t->source_location = target->source_location;
54 t->function = target->function;
74 if(!target->is_function_call())
80 if(f.
id() != ID_symbol)
86 goto_functionst::function_mapt::const_iterator f_it =
91 return !f_it->second.body_available();
129 (*this)(f_it->second.body, goto_functions);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
#define PRECONDITION(CONDITION)
bool empty() const
Is the program empty?
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.
function_mapt function_map
Expression to hold a symbol (variable)
targett add_instruction()
Adds an instruction at the end.
typet & type()
Return the type of the expression.
codet representation of a function call statement.
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...
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const source_locationt & source_location() const
const irep_idt & get_identifier() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
std::vector< exprt > operandst
#define Forall_goto_functions(it, functions)
A side_effect_exprt that returns a non-deterministically chosen value.
instructionst instructions
The list of instructions in the goto program.
A collection of goto functions.
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.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
source_locationt & add_source_location()
A codet representing an assignment in the program.
instructionst::iterator targett
codet representation of an expression statement.