53 goto_functionst::function_mapt::iterator it=
59 goto_functiont &goto_function=it->second;
60 assert(goto_function.body_available());
69 goto_functiont &goto_function=f_it->second;
71 if(!goto_function.body_available())
95 goto_functiont &goto_function=f_it->second;
96 goto_function.body.clear();
111 unsigned smallfunc_limit,
112 bool adjust_function)
136 unsigned smallfunc_limit,
137 bool adjust_function)
152 goto_functiont &goto_function=f_it->second;
154 if(!goto_function.body_available())
176 if(function_expr.
id()!=ID_symbol)
183 goto_functionst::function_mapt::const_iterator f_it=
191 const goto_functiont &goto_function=f_it->second;
193 if(!goto_function.body_available())
199 if(goto_function.is_inlined() ||
221 bool adjust_function,
246 bool adjust_function,
256 goto_functionst::function_mapt::iterator f_it=
264 if(!goto_function.body_available())
282 goto_inline.goto_inline(
function, goto_function, inline_map,
true);
290 bool adjust_function,
300 goto_functionst::function_mapt::iterator f_it=
308 if(!goto_function.body_available())
327 goto_inline.goto_inline(
function, goto_function, inline_map,
true);
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
void goto_function_inline(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
Inline all function calls made from a particular function.
symbol_tablet symbol_table
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
void goto_partial_inline(goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit, bool adjust_function)
Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by...
void compute_loop_numbers()
const irep_idt & id() const
std::map< irep_idt, call_listt > inline_mapt
static irep_idt entry_point()
API to expression classes.
goto_function_templatet< goto_programt > goto_functiont
function_mapt function_map
jsont goto_function_inline_and_log(goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching)
std::vector< exprt > operandst
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
static bool is_call(goto_programt::const_targett target)
goto_functionst goto_functions