cprover
goto_inline.h File Reference

Function Inlining. More...

#include <util/json.h>
#include "goto_model.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)
 
void goto_inline (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false)
 
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)
 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)
 Inline all function calls made from a particular function. More...
 
jsont goto_function_inline_and_log (goto_functionst &goto_functions, const irep_idt function, const namespacet &ns, message_handlert &message_handler, bool adjust_function=false, bool caching=true)
 

Detailed Description

Function Inlining.

Definition in file goto_inline.h.

Function Documentation

◆ goto_function_inline() [1/2]

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.

Parameters
goto_modelSource of the symbol table and function map to use.
functionThe function whose calls to inline.
message_handlerMessage handler used by goto_inlinet.
adjust_functionTell goto_inlinet to adjust function.
cachingTell goto_inlinet to cache.

Definition at line 217 of file goto_inline.cpp.

References goto_function_inline(), goto_modelt::goto_functions, and goto_modelt::symbol_table.

Referenced by goto_function_inline(), and goto_instrument_parse_optionst::instrument_goto_program().

◆ goto_function_inline() [2/2]

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.

Parameters
goto_functionsThe function map to use to find function bodies.
functionThe function whose calls to inline.
nsNamespace used by goto_inlinet.
message_handlerMessage handler used by goto_inlinet.
adjust_functionTell goto_inlinet to adjust function.
cachingTell goto_inlinet to cache.

Definition at line 241 of file goto_inline.cpp.

References Forall_goto_program_instructions, goto_functions_templatet< bodyT >::function_map, goto_inline(), and goto_inlinet::is_call().

◆ goto_function_inline_and_log()

jsont goto_function_inline_and_log ( goto_functionst goto_functions,
const irep_idt  function,
const namespacet ns,
message_handlert message_handler,
bool  adjust_function = false,
bool  caching = true 
)

◆ goto_inline() [1/2]

◆ goto_inline() [2/2]

void goto_inline ( goto_functionst goto_functions,
const namespacet ns,
message_handlert message_handler,
bool  adjust_function = false 
)

◆ goto_partial_inline() [1/2]

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).

Parameters
goto_modelSource of the symbol table and function map to use.
message_handlerMessage handler used by goto_inlinet.
smallfunc_limitThe maximum number of instructions in functions to be inlined.
adjust_functionTell goto_inlinet to adjust function.

Definition at line 108 of file goto_inline.cpp.

References goto_modelt::goto_functions, goto_partial_inline(), and goto_modelt::symbol_table.

Referenced by goto_instrument_parse_optionst::do_partial_inlining(), goto_partial_inline(), goto_fence_inserter_parse_optionst::instrument_goto_program(), goto_instrument_parse_optionst::instrument_goto_program(), clobber_parse_optionst::process_goto_program(), goto_diff_parse_optionst::process_goto_program(), goto_analyzer_parse_optionst::process_goto_program(), symex_parse_optionst::process_goto_program(), and cbmc_parse_optionst::process_goto_program().

◆ goto_partial_inline() [2/2]

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).

Parameters
goto_functionsThe function map to use to find functions containing calls and function bodies.
nsNamespace used by goto_inlinet.
message_handlerMessage handler used by goto_inlinet.
smallfunc_limitThe maximum number of instructions in functions to be inlined.
adjust_functionTell goto_inlinet to adjust function.

Definition at line 132 of file goto_inline.cpp.

References goto_functions_templatet< bodyT >::entry_point(), Forall_goto_functions, Forall_goto_program_instructions, goto_functions_templatet< bodyT >::function_map, goto_inlinet::get_call(), symbol_exprt::get_identifier(), goto_inline(), irept::id(), goto_program_templatet< codeT, guardT >::instructions, goto_inlinet::is_call(), and to_symbol_expr().