cprover
goto_inlinet Class Reference

#include <goto_inline_class.h>

+ Inheritance diagram for goto_inlinet:
+ 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 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 message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. 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 commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 

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

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
 

Additional Inherited Members

- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 

Detailed Description

Definition at line 20 of file goto_inline_class.h.

Member Typedef Documentation

◆ cachet

Definition at line 191 of file goto_inline_class.h.

◆ call_listt

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

Definition at line 45 of file goto_inline_class.h.

◆ callt

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

Definition at line 42 of file goto_inline_class.h.

◆ finished_sett

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

Definition at line 194 of file goto_inline_class.h.

◆ goto_functiont

◆ inline_mapt

Definition at line 48 of file goto_inline_class.h.

◆ no_body_sett

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

Definition at line 200 of file goto_inline_class.h.

◆ recursion_sett

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

Definition at line 197 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 23 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 665 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 617 of file goto_inline_class.cpp.

◆ clear()

void goto_inlinet::clear ( void  )
inlineprotected

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

Definition at line 321 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 447 of file goto_inline_class.cpp.

◆ goto_inline() [1/2]

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

Definition at line 462 of file goto_inline_class.cpp.

◆ goto_inline() [2/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 481 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 496 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 548 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 234 of file goto_inline_class.cpp.

◆ is_ignored()

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

Definition at line 610 of file goto_inline_class.cpp.

◆ output_cache()

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

Definition at line 719 of file goto_inline_class.cpp.

◆ output_inline_log_json()

jsont goto_inlinet::output_inline_log_json ( )
inline

Definition at line 72 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 676 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 30 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 131 of file goto_inline_class.cpp.

◆ replace_return()

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

Definition at line 157 of file goto_inline_class.cpp.

Member Data Documentation

◆ adjust_function

const bool goto_inlinet::adjust_function
protected

Definition at line 128 of file goto_inline_class.h.

◆ cache

cachet goto_inlinet::cache
protected

Definition at line 192 of file goto_inline_class.h.

◆ caching

const bool goto_inlinet::caching
protected

Definition at line 129 of file goto_inline_class.h.

◆ finished_set

finished_sett goto_inlinet::finished_set
protected

Definition at line 195 of file goto_inline_class.h.

◆ goto_functions

goto_functionst& goto_inlinet::goto_functions
protected

Definition at line 125 of file goto_inline_class.h.

◆ inline_log

goto_inline_logt goto_inlinet::inline_log
protected

Definition at line 131 of file goto_inline_class.h.

◆ no_body_set

no_body_sett goto_inlinet::no_body_set
protected

Definition at line 201 of file goto_inline_class.h.

◆ ns

const namespacet& goto_inlinet::ns
protected

Definition at line 126 of file goto_inline_class.h.

◆ recursion_set

recursion_sett goto_inlinet::recursion_set
protected

Definition at line 198 of file goto_inline_class.h.


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