#include <goto_inline_class.h>
|
| goto_inlinet (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true) |
| Sets up the class with the program to operate on. More...
|
|
void | goto_inline (const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false) |
| Inline all of the chosen calls in a given function. More...
|
|
void | goto_inline (const goto_inlinet::call_listt &call_list, goto_programt &goto_program, const bool force_full=false) |
| Inline specified calls in a given program. More...
|
|
void | goto_inline (const inline_mapt &inline_map, const bool force_full=false) |
| Inline all of the given call locations. More...
|
|
void | output_inline_map (std::ostream &out, const inline_mapt &inline_map) |
|
void | output_cache (std::ostream &out) const |
|
jsont | output_inline_log_json () |
|
|
void | goto_inline_nontransitive (const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full) |
|
const goto_functiont & | goto_inline_transitive (const irep_idt identifier, const goto_functiont &goto_function, const bool force_full) |
|
bool | check_inline_map (const inline_mapt &inline_map) const |
|
bool | check_inline_map (const irep_idt identifier, const inline_mapt &inline_map) const |
|
bool | is_ignored (const irep_idt id) const |
|
void | clear () |
|
void | expand_function_call (goto_programt &dest, const inline_mapt &inline_map, const bool transitive, const bool force_full, goto_programt::targett target) |
| Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive. More...
|
|
void | insert_function_body (const goto_functiont &f, goto_programt &dest, goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments) |
|
void | replace_return (goto_programt &body, const exprt &lhs) |
|
void | parameter_assignments (const goto_programt::targett target, const irep_idt &function_name, const goto_functiont::parameter_identifierst ¶meter_identifiers, const exprt::operandst &arguments, goto_programt &dest) |
|
void | parameter_destruction (const goto_programt::targett target, const goto_functiont::parameter_identifierst ¶meter_identifiers, goto_programt &dest) |
|
Definition at line 25 of file goto_inline_class.h.
◆ cachet
◆ call_listt
◆ callt
◆ finished_sett
◆ goto_functiont
◆ inline_mapt
◆ no_body_sett
◆ recursion_sett
◆ goto_inlinet()
Sets up the class with the program to operate on.
- Parameters
-
goto_functions | : The map of functions to work on |
ns | : The corresponding namespace |
message_handler | : Used to log what is being inlined |
adjust_function | Replace location in caller location. |
caching | : cache functions when in transitive mode |
Definition at line 35 of file goto_inline_class.h.
◆ check_inline_map() [1/2]
bool goto_inlinet::check_inline_map |
( |
const inline_mapt & |
inline_map | ) |
const |
|
protected |
◆ check_inline_map() [2/2]
bool goto_inlinet::check_inline_map |
( |
const irep_idt |
identifier, |
|
|
const inline_mapt & |
inline_map |
|
) |
| const |
|
protected |
◆ clear()
void goto_inlinet::clear |
( |
void |
| ) |
|
|
inlineprotected |
◆ expand_function_call()
Inlines a single function call Calls out to goto_inline_transitive or goto_inline_nontransitive.
Definition at line 302 of file goto_inline_class.cpp.
◆ get_call()
◆ goto_inline() [1/3]
Inline specified calls in a given program.
- Parameters
-
call_list | : calls to inline in the goto_program . |
goto_program | : goto program to inline calls_list in. |
force_full | : true to break recursion with a SKIP, false means detecting recursion is an error. |
Definition at line 491 of file goto_inline_class.cpp.
◆ goto_inline() [2/3]
void goto_inlinet::goto_inline |
( |
const inline_mapt & |
inline_map, |
|
|
const bool |
force_full = false |
|
) |
| |
Inline all of the given call locations.
This is the highest-level interface and calls the other goto_inline
- Parameters
-
inline_map | : which call locations to inline. |
force_full | : true to break recursion with a SKIP, false means detecting recursion is an error. |
Definition at line 450 of file goto_inline_class.cpp.
◆ goto_inline() [3/3]
Inline all of the chosen calls in a given function.
This is main entry point for the functionality
- Parameters
-
identifier | : the name of the caller function. |
goto_function | : the caller function itself. |
inline_map | : which call locations to inline. |
force_full | : true to break recursion with a SKIP, false means detecting recursion is an error. |
Definition at line 476 of file goto_inline_class.cpp.
◆ goto_inline_nontransitive()
◆ goto_inline_transitive()
◆ insert_function_body()
◆ is_ignored()
bool goto_inlinet::is_ignored |
( |
const irep_idt |
id | ) |
const |
|
protected |
◆ output_cache()
void goto_inlinet::output_cache |
( |
std::ostream & |
out | ) |
const |
◆ output_inline_log_json()
jsont goto_inlinet::output_inline_log_json |
( |
| ) |
|
|
inline |
◆ output_inline_map()
void goto_inlinet::output_inline_map |
( |
std::ostream & |
out, |
|
|
const inline_mapt & |
inline_map |
|
) |
| |
◆ parameter_assignments()
◆ parameter_destruction()
◆ replace_return()
◆ adjust_function
const bool goto_inlinet::adjust_function |
|
protected |
◆ cache
◆ caching
const bool goto_inlinet::caching |
|
protected |
◆ finished_set
◆ goto_functions
◆ inline_log
◆ log
◆ no_body_set
◆ ns
◆ recursion_set
The documentation for this class was generated from the following files: