|
CBMC
|
#include <util/json.h>
Include dependency graph for goto_inline.h:
This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Functions | |
| void | goto_inline (goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function=false) |
| Inline every function call into the entry_point() function. More... | |
| void | goto_inline (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false) |
| Inline every function call into the entry_point() function. More... | |
| void | goto_partial_inline (goto_modelt &goto_model, message_handlert &message_handler, unsigned smallfunc_limit=0, bool adjust_function=false) |
| Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by instruction count). More... | |
| void | goto_partial_inline (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, unsigned smallfunc_limit=0, bool adjust_function=false) |
| Inline all function calls to functions either marked as "inlined" or smaller than smallfunc_limit (by instruction count). More... | |
| void | goto_function_inline (goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function=false, bool caching=true) |
| Transitively inline all function calls made from a particular function. More... | |
| void | goto_function_inline (goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false, bool caching=true) |
| Transitively inline all function calls made from a particular function. More... | |
| jsont | goto_function_inline_and_log (goto_modelt &, const irep_idt function, message_handlert &message_handler, bool adjust_function=false, bool caching=true) |
Function Inlining This gives a number of different interfaces to the function inlining functionality of goto_inlinet.
Definition in file goto_inline.h.
| void goto_function_inline | ( | goto_functionst & | goto_functions, |
| const irep_idt | function, | ||
| const namespacet & | ns, | ||
| message_handlert & | message_handler, | ||
| bool | adjust_function, | ||
| bool | caching | ||
| ) |
Transitively inline all function calls made from a particular function.
Caller is responsible for calling update(), compute_loop_numbers(), etc.
| goto_functions | The function map to use to find function bodies. |
| function | The function whose calls to inline. |
| ns | Namespace used by goto_inlinet. |
| message_handler | Message handler used by goto_inlinet. |
| adjust_function | Replace location in inlined function with call site. |
| caching | Tell goto_inlinet to cache. |
Definition at line 264 of file goto_inline.cpp.
| void goto_function_inline | ( | goto_modelt & | goto_model, |
| const irep_idt | function, | ||
| message_handlert & | message_handler, | ||
| bool | adjust_function, | ||
| bool | caching | ||
| ) |
Transitively inline all function calls made from a particular function.
Caller is responsible for calling update(), compute_loop_numbers(), etc.
| goto_model | Source of the symbol table and function map to use. |
| function | The function whose calls to inline. |
| message_handler | Message handler used by goto_inlinet. |
| adjust_function | Replace location in inlined function with call site. |
| caching | Tell goto_inlinet to cache. |
Definition at line 239 of file goto_inline.cpp.
| jsont goto_function_inline_and_log | ( | goto_modelt & | , |
| const irep_idt | function, | ||
| message_handlert & | message_handler, | ||
| bool | adjust_function = false, |
||
| bool | caching = true |
||
| ) |
Definition at line 308 of file goto_inline.cpp.
| void goto_inline | ( | goto_functionst & | goto_functions, |
| const namespacet & | ns, | ||
| message_handlert & | message_handler, | ||
| bool | adjust_function | ||
| ) |
Inline every function call into the entry_point() function.
Then delete the bodies of all of the other functions. This is pretty drastic and can result in a very large program. Caller is responsible for calling update(), compute_loop_numbers(), etc.
| goto_functions | The function map to use. |
| ns | : The namespace to use. |
| message_handler | Message handler used by goto_inlinet. |
| adjust_function | Replace location in inlined function with call site. |
Definition at line 47 of file goto_inline.cpp.
| void goto_inline | ( | goto_modelt & | goto_model, |
| message_handlert & | message_handler, | ||
| bool | adjust_function | ||
| ) |
Inline every function call into the entry_point() function.
Then delete the bodies of all of the other functions. This is pretty drastic and can result in a very large program. Caller is responsible for calling update(), compute_loop_numbers(), etc.
| goto_model | Source of the symbol table and function map to use. |
| message_handler | Message handler used by goto_inlinet. |
| adjust_function | Replace location in inlined function with call site. |
Definition at line 26 of file goto_inline.cpp.
| void goto_partial_inline | ( | goto_functionst & | goto_functions, |
| const namespacet & | ns, | ||
| 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 instruction count).
Unlike the goto_inline functions, this doesn't remove function bodies after inlining. Caller is responsible for calling update(), compute_loop_numbers(), etc.
| goto_functions | The function map to use to find functions containing calls and function bodies. |
| ns | Namespace used by goto_inlinet. |
| message_handler | Message handler used by goto_inlinet. |
| smallfunc_limit | The maximum number of instructions in functions to be inlined. |
| adjust_function | Replace location in inlined function with call site. |
Definition at line 149 of file goto_inline.cpp.
| 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 instruction count).
Unlike the goto_inline functions, this doesn't remove function bodies after inlining. Caller is responsible for calling update(), compute_loop_numbers(), etc.
| goto_model | Source of the symbol table and function map to use. |
| message_handler | Message handler used by goto_inlinet. |
| smallfunc_limit | The maximum number of instructions in functions to be inlined. |
| adjust_function | Replace location in inlined function with call site. |
Definition at line 122 of file goto_inline.cpp.