Go to the documentation of this file.
36 for(
const exprt &argument : arguments)
69 if(!target->is_function_call())
75 if(f.
id() != ID_symbol)
81 goto_functionst::function_mapt::const_iterator f_it =
86 return !f_it->second.body_available();
124 (*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.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
bool empty() const
Is the program empty?
Base class for all expressions.
Remove calls to functions without a body.
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)
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
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.
#define PRECONDITION(CONDITION)
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
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.
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
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.
Goto Programs with Functions.
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.
const source_locationt & source_location() const
instructionst::iterator targett
codet representation of an expression statement.