cprover
goto_inlinet Class Reference

#include <goto_inline_class.h>

Inheritance diagram for goto_inlinet:
[legend]
Collaboration diagram for goto_inlinet:
[legend]

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 Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 

Public Member Functions

 goto_inlinet (goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, bool adjust_function, bool caching=true)
 
void goto_inline (const irep_idt identifier, goto_functiont &goto_function, const inline_mapt &inline_map, const bool force_full=false)
 
void goto_inline (const inline_mapt &inline_map, const bool force_full=false)
 
void output_inline_map (std::ostream &out, const inline_mapt &inline_map)
 
void output_cache (std::ostream &out) const
 
jsont output_inline_log_json ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level)
 
mstreamterror ()
 
mstreamtwarning ()
 
mstreamtresult ()
 
mstreamtstatus ()
 
mstreamtstatistics ()
 
mstreamtprogress ()
 
mstreamtdebug ()
 

Static Public Member Functions

static bool is_bp_call (goto_programt::const_targett target)
 
static bool is_call (goto_programt::const_targett target)
 
static void get_call (goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments, exprt &constrain)
 
- Static Public Member Functions inherited from messaget
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

Protected Types

typedef goto_functionst::function_mapt cachet
 
typedef std::unordered_set< irep_idt, irep_id_hashfinished_sett
 
typedef std::unordered_set< irep_idt, irep_id_hashrecursion_sett
 
typedef std::unordered_set< irep_idt, irep_id_hashno_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)
 
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, const exprt &constrain)
 
void insert_function_nobody (goto_programt &dest, const exprt &lhs, goto_programt::targett target, const symbol_exprt &function, const exprt::operandst &arguments)
 
void replace_return (goto_programt &body, const exprt &lhs, const exprt &constrain)
 
void parameter_assignments (const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest)
 
void parameter_destruction (const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest)
 

Protected Attributes

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
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Definition at line 21 of file goto_inline_class.h.

Member Typedef Documentation

◆ cachet

Definition at line 207 of file goto_inline_class.h.

◆ call_listt

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

Definition at line 46 of file goto_inline_class.h.

◆ callt

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

Definition at line 43 of file goto_inline_class.h.

◆ finished_sett

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

Definition at line 210 of file goto_inline_class.h.

◆ goto_functiont

typedef goto_functionst::goto_functiont goto_inlinet::goto_functiont

Definition at line 38 of file goto_inline_class.h.

◆ inline_mapt

Definition at line 49 of file goto_inline_class.h.

◆ no_body_sett

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

Definition at line 216 of file goto_inline_class.h.

◆ recursion_sett

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

Definition at line 213 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

Definition at line 24 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

◆ 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

Definition at line 157 of file goto_inline_class.h.

References cache, finished_set, no_body_set, and recursion_set.

◆ expand_function_call()

◆ get_call()

◆ goto_inline() [1/2]

void goto_inlinet::goto_inline ( const irep_idt  identifier,
goto_functiont goto_function,
const inline_mapt inline_map,
const bool  force_full = false 
)

Definition at line 696 of file goto_inline_class.cpp.

References goto_inline_nontransitive(), and recursion_set.

Referenced by goto_inline().

◆ goto_inline() [2/2]

void goto_inlinet::goto_inline ( const inline_mapt inline_map,
const bool  force_full = false 
)

◆ 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

◆ 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

◆ insert_function_body()

◆ insert_function_nobody()

◆ is_bp_call()

bool goto_inlinet::is_bp_call ( goto_programt::const_targett  target)
static

Definition at line 666 of file goto_inline_class.cpp.

Referenced by get_call(), and is_call().

◆ is_call()

◆ is_ignored()

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

Definition at line 826 of file goto_inline_class.cpp.

Referenced by expand_function_call().

◆ output_cache()

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

Definition at line 940 of file goto_inline_class.cpp.

References cache.

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

Member Data Documentation

◆ adjust_function

const bool goto_inlinet::adjust_function
protected

◆ cache

cachet goto_inlinet::cache
protected

◆ caching

const bool goto_inlinet::caching
protected

Definition at line 135 of file goto_inline_class.h.

Referenced by expand_function_call().

◆ finished_set

finished_sett goto_inlinet::finished_set
protected

Definition at line 211 of file goto_inline_class.h.

Referenced by clear(), and goto_inline_nontransitive().

◆ goto_functions

goto_functionst& goto_inlinet::goto_functions
protected

◆ inline_log

goto_inline_logt goto_inlinet::inline_log
protected

◆ no_body_set

no_body_sett goto_inlinet::no_body_set
protected

Definition at line 217 of file goto_inline_class.h.

Referenced by clear(), and insert_function_nobody().

◆ ns

const namespacet& goto_inlinet::ns
protected

◆ recursion_set

recursion_sett goto_inlinet::recursion_set
protected

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