cprover
|
Function Inlining. More...
#include "goto_inline.h"
#include <cassert>
#include <util/prefix.h>
#include <util/cprover_prefix.h>
#include <util/std_code.h>
#include <util/std_expr.h>
#include "goto_inline_class.h"
Go to the source code of this file.
Functions | |
void | goto_inline (goto_modelt &goto_model, message_handlert &message_handler, bool adjust_function) |
void | goto_inline (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_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 instruction count). More... | |
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). More... | |
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. More... | |
void | goto_function_inline (goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching) |
Inline all function calls made from a particular function. More... | |
jsont | goto_function_inline_and_log (goto_modelt &goto_model, const irep_idt function, message_handlert &message_handler, bool adjust_function, bool caching) |
Function Inlining.
Definition in file goto_inline.cpp.
void goto_function_inline | ( | goto_functionst & | goto_functions, |
const irep_idt | function, | ||
const namespacet & | ns, | ||
message_handlert & | message_handler, | ||
bool | adjust_function, | ||
bool | caching | ||
) |
Inline all function calls made from a particular function.
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 | Tell goto_inlinet to adjust function. |
caching | Tell goto_inlinet to cache. |
Definition at line 240 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 | ||
) |
Inline all function calls made from a particular function.
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 | Tell goto_inlinet to adjust function. |
caching | Tell goto_inlinet to cache. |
Definition at line 216 of file goto_inline.cpp.
jsont goto_function_inline_and_log | ( | goto_modelt & | goto_model, |
const irep_idt | function, | ||
message_handlert & | message_handler, | ||
bool | adjust_function, | ||
bool | caching | ||
) |
Definition at line 284 of file goto_inline.cpp.
void goto_inline | ( | goto_functionst & | goto_functions, |
const namespacet & | ns, | ||
message_handlert & | message_handler, | ||
bool | adjust_function | ||
) |
Definition at line 36 of file goto_inline.cpp.
void goto_inline | ( | goto_modelt & | goto_model, |
message_handlert & | message_handler, | ||
bool | adjust_function | ||
) |
Definition at line 23 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).
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 | Tell goto_inlinet to adjust function. |
Definition at line 132 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).
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 | Tell goto_inlinet to adjust function. |
Definition at line 108 of file goto_inline.cpp.