52 goto_functionst::function_mapt::iterator it=
61 "body of entry point function must be available");
81 if(!i_it->is_function_call())
112 unsigned smallfunc_limit,
113 bool adjust_function)
137 unsigned smallfunc_limit,
138 bool adjust_function)
168 if(!i_it->is_function_call())
176 if(function_expr.
id()!=ID_symbol)
183 goto_functionst::function_mapt::const_iterator f_it=
222 bool adjust_function,
247 bool adjust_function,
257 goto_functionst::function_mapt::iterator f_it=
265 if(!goto_function.body_available())
277 if(!i_it->is_function_call())
283 goto_inline.goto_inline(
function, goto_function, inline_map,
true);
290 bool adjust_function,
302 goto_functionst::function_mapt::iterator f_it=
310 if(!goto_function.body_available())
323 if(!i_it->is_function_call())
329 goto_inline.goto_inline(
function, goto_function, inline_map,
true);
std::pair< goto_programt::targett, bool > callt
std::list< callt > call_listt
void compute_loop_numbers()
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.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
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 clear()
Clear the goto program.
const irep_idt & id() const
std::map< irep_idt, call_listt > inline_mapt
instructionst instructions
The list of instructions in the goto program.
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
#define PRECONDITION(CONDITION)
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::vector< exprt > operandst
A goto function, consisting of function type (see type), function body (see body),...
A generic container class for the GOTO intermediate representation of one function.
bool body_available() const
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
Base class for all expressions.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
goto_functionst goto_functions
GOTO functions.