49 goto_functionst::function_mapt::iterator it=
58 "body of entry point function must be available");
78 if(!i_it->is_function_call())
109 unsigned smallfunc_limit,
110 bool adjust_function)
134 unsigned smallfunc_limit,
135 bool adjust_function)
167 if(!i_it->is_function_call())
175 if(function_expr.
id()!=ID_symbol)
182 goto_functionst::function_mapt::const_iterator called_it =
220 bool adjust_function,
245 bool adjust_function,
255 goto_functionst::function_mapt::iterator f_it=
263 if(!goto_function.body_available())
275 if(!i_it->is_function_call())
281 goto_inline.goto_inline(
function, goto_function, inline_map,
true);
288 bool adjust_function,
300 goto_functionst::function_mapt::iterator f_it=
308 if(!goto_function.body_available())
321 if(!i_it->is_function_call())
327 goto_inline.goto_inline(
function, goto_function, inline_map,
true);
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
A collection of goto functions.
void compute_loop_numbers()
function_mapt function_map
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
bool body_available() const
std::list< callt > call_listt
static void get_call(goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
std::pair< goto_programt::targett, bool > callt
std::map< irep_idt, call_listt > inline_mapt
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void clear()
Clear the goto program.
const irep_idt & id() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
void goto_inline(goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function)
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.
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...
jsont goto_function_inline_and_log(goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching)
#define Forall_goto_program_instructions(it, program)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.