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)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to mstream using output_generator if the configured verbosity is at least as high as that of mstream. More...
 

Static Public Member Functions

static void get_call (goto_programt::const_targett target, exprt &lhs, exprt &function, exprt::operandst &arguments)
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static mstreamteom (mstreamt &m)
 
static mstreamtendl (mstreamt &m)
 

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

Definition at line 196 of file goto_inline_class.h.

◆ goto_functiont

◆ inline_mapt

Definition at line 49 of file goto_inline_class.h.

◆ no_body_sett

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

Definition at line 202 of file goto_inline_class.h.

◆ recursion_sett

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

Definition at line 199 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 152 of file goto_inline_class.h.

References cache, finished_set, no_body_set, and recursion_set.

◆ expand_function_call()

◆ get_call()

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

Definition at line 509 of file goto_inline_class.cpp.

References PRECONDITION, and to_code_function_call().

Referenced by expand_function_call(), and goto_partial_inline().

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

◆ insert_function_body()

◆ is_ignored()

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

Definition at line 673 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 786 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 130 of file goto_inline_class.h.

Referenced by expand_function_call().

◆ finished_set

finished_sett goto_inlinet::finished_set
protected

Definition at line 197 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 203 of file goto_inline_class.h.

Referenced by clear(), and expand_function_call().

◆ 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: