CBMC
goto_inlinet Class Reference

#include <goto_inline_class.h>

+ Collaboration diagram for goto_inlinet:

Classes

class  goto_inline_logt
 

Public Types

typedef goto_functionst::goto_functiont goto_functiont
 
typedef std::pair< goto_programt::targett, bool > callt
 
typedef std::list< calltcall_listt
 
typedef std::map< irep_idt, call_listtinline_mapt
 

Public Member Functions

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

Static Public Member Functions

static void get_call (goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
 

Protected Types

typedef goto_functionst::function_mapt cachet
 
typedef std::unordered_set< irep_idtfinished_sett
 
typedef std::unordered_set< irep_idtrecursion_sett
 
typedef std::unordered_set< irep_idtno_body_sett
 

Protected Member Functions

void goto_inline_nontransitive (const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full)
 
const goto_functiontgoto_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 &parameter_identifiers, const exprt::operandst &arguments, goto_programt &dest)
 
void parameter_destruction (const goto_programt::targett target, const goto_functiont::parameter_identifierst &parameter_identifiers, goto_programt &dest)
 

Protected Attributes

messaget log
 
goto_functionstgoto_functions
 
const namespacetns
 
const bool adjust_function
 
const bool caching
 
goto_inline_logt inline_log
 
cachet cache
 
finished_sett finished_set
 
recursion_sett recursion_set
 
no_body_sett no_body_set
 

Detailed Description

Definition at line 25 of file goto_inline_class.h.

Member Typedef Documentation

◆ cachet

Definition at line 216 of file goto_inline_class.h.

◆ call_listt

typedef std::list<callt> goto_inlinet::call_listt

Definition at line 57 of file goto_inline_class.h.

◆ callt

typedef std::pair<goto_programt::targett, bool> goto_inlinet::callt

Definition at line 54 of file goto_inline_class.h.

◆ finished_sett

typedef std::unordered_set<irep_idt> goto_inlinet::finished_sett
protected

Definition at line 219 of file goto_inline_class.h.

◆ goto_functiont

◆ inline_mapt

Definition at line 60 of file goto_inline_class.h.

◆ no_body_sett

typedef std::unordered_set<irep_idt> goto_inlinet::no_body_sett
protected

Definition at line 225 of file goto_inline_class.h.

◆ recursion_sett

typedef std::unordered_set<irep_idt> goto_inlinet::recursion_sett
protected

Definition at line 222 of file goto_inline_class.h.

Constructor & Destructor Documentation

◆ goto_inlinet()

goto_inlinet::goto_inlinet ( goto_functionst goto_functions,
const namespacet ns,
message_handlert message_handler,
bool  adjust_function,
bool  caching = true 
)
inline

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_functionReplace location in caller location.
caching: cache functions when in transitive mode

Definition at line 35 of file goto_inline_class.h.

Member Function Documentation

◆ check_inline_map() [1/2]

bool goto_inlinet::check_inline_map ( const inline_mapt inline_map) const
protected

Definition at line 675 of file goto_inline_class.cpp.

◆ check_inline_map() [2/2]

bool goto_inlinet::check_inline_map ( const irep_idt  identifier,
const inline_mapt inline_map 
) const
protected

Definition at line 627 of file goto_inline_class.cpp.

◆ clear()

void goto_inlinet::clear ( void  )
inlineprotected

Definition at line 176 of file goto_inline_class.h.

◆ expand_function_call()

void goto_inlinet::expand_function_call ( goto_programt dest,
const inline_mapt inline_map,
const bool  transitive,
const bool  force_full,
goto_programt::targett  target 
)
protected

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

void goto_inlinet::get_call ( goto_programt::const_targett  target,
exprt lhs,
exprt function,
exprt::operandst arguments 
)
static

Definition at line 432 of file goto_inline_class.cpp.

◆ goto_inline() [1/3]

void goto_inlinet::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.

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]

void goto_inlinet::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.

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

void goto_inlinet::goto_inline_nontransitive ( const irep_idt  identifier,
goto_functiont goto_function,
const inline_mapt inline_map,
const bool  force_full 
)
protected

Definition at line 506 of file goto_inline_class.cpp.

◆ goto_inline_transitive()

const goto_inlinet::goto_functiont & goto_inlinet::goto_inline_transitive ( const irep_idt  identifier,
const goto_functiont goto_function,
const bool  force_full 
)
protected

Definition at line 558 of file goto_inline_class.cpp.

◆ insert_function_body()

void goto_inlinet::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 
)
protected

Definition at line 214 of file goto_inline_class.cpp.

◆ is_ignored()

bool goto_inlinet::is_ignored ( const irep_idt  id) const
protected

Definition at line 620 of file goto_inline_class.cpp.

◆ output_cache()

void goto_inlinet::output_cache ( std::ostream &  out) const

Definition at line 727 of file goto_inline_class.cpp.

◆ output_inline_log_json()

jsont goto_inlinet::output_inline_log_json ( )
inline

Definition at line 94 of file goto_inline_class.h.

◆ output_inline_map()

void goto_inlinet::output_inline_map ( std::ostream &  out,
const inline_mapt inline_map 
)

Definition at line 686 of file goto_inline_class.cpp.

◆ parameter_assignments()

void goto_inlinet::parameter_assignments ( const goto_programt::targett  target,
const irep_idt function_name,
const goto_functiont::parameter_identifierst parameter_identifiers,
const exprt::operandst arguments,
goto_programt dest 
)
protected

Definition at line 24 of file goto_inline_class.cpp.

◆ parameter_destruction()

void goto_inlinet::parameter_destruction ( const goto_programt::targett  target,
const goto_functiont::parameter_identifierst parameter_identifiers,
goto_programt dest 
)
protected

Definition at line 125 of file goto_inline_class.cpp.

◆ replace_return()

void goto_inlinet::replace_return ( goto_programt body,
const exprt lhs 
)
protected

Definition at line 151 of file goto_inline_class.cpp.

Member Data Documentation

◆ adjust_function

const bool goto_inlinet::adjust_function
protected

Definition at line 153 of file goto_inline_class.h.

◆ cache

cachet goto_inlinet::cache
protected

Definition at line 217 of file goto_inline_class.h.

◆ caching

const bool goto_inlinet::caching
protected

Definition at line 154 of file goto_inline_class.h.

◆ finished_set

finished_sett goto_inlinet::finished_set
protected

Definition at line 220 of file goto_inline_class.h.

◆ goto_functions

goto_functionst& goto_inlinet::goto_functions
protected

Definition at line 150 of file goto_inline_class.h.

◆ inline_log

goto_inline_logt goto_inlinet::inline_log
protected

Definition at line 156 of file goto_inline_class.h.

◆ log

messaget goto_inlinet::log
protected

Definition at line 149 of file goto_inline_class.h.

◆ no_body_set

no_body_sett goto_inlinet::no_body_set
protected

Definition at line 226 of file goto_inline_class.h.

◆ ns

const namespacet& goto_inlinet::ns
protected

Definition at line 151 of file goto_inline_class.h.

◆ recursion_set

recursion_sett goto_inlinet::recursion_set
protected

Definition at line 223 of file goto_inline_class.h.


The documentation for this class was generated from the following files: