cprover
|
#include <goto_inline_class.h>
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< callt > | call_listt |
typedef std::map< irep_idt, call_listt > | inline_mapt |
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 () |
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_idt > | finished_sett |
typedef std::unordered_set< irep_idt > | recursion_sett |
typedef std::unordered_set< irep_idt > | no_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_functiont & | goto_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 ¶meter_identifiers, const exprt::operandst &arguments, goto_programt &dest) |
void | parameter_destruction (const goto_programt::targett target, const goto_functiont::parameter_identifierst ¶meter_identifiers, goto_programt &dest) |
Protected Attributes | |
messaget | log |
goto_functionst & | goto_functions |
const namespacet & | ns |
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 |
Definition at line 20 of file goto_inline_class.h.
|
protected |
Definition at line 192 of file goto_inline_class.h.
typedef std::list<callt> goto_inlinet::call_listt |
Definition at line 45 of file goto_inline_class.h.
typedef std::pair<goto_programt::targett, bool> goto_inlinet::callt |
Definition at line 42 of file goto_inline_class.h.
|
protected |
Definition at line 195 of file goto_inline_class.h.
Definition at line 37 of file goto_inline_class.h.
typedef std::map<irep_idt, call_listt> goto_inlinet::inline_mapt |
Definition at line 48 of file goto_inline_class.h.
|
protected |
Definition at line 201 of file goto_inline_class.h.
|
protected |
Definition at line 198 of file goto_inline_class.h.
|
inline |
Definition at line 23 of file goto_inline_class.h.
|
protected |
Definition at line 658 of file goto_inline_class.cpp.
|
protected |
Definition at line 610 of file goto_inline_class.cpp.
|
inlineprotected |
Definition at line 152 of file goto_inline_class.h.
|
protected |
Definition at line 310 of file goto_inline_class.cpp.
|
static |
Definition at line 440 of file goto_inline_class.cpp.
void goto_inlinet::goto_inline | ( | const inline_mapt & | inline_map, |
const bool | force_full = false |
||
) |
Definition at line 455 of file goto_inline_class.cpp.
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 474 of file goto_inline_class.cpp.
|
protected |
Definition at line 489 of file goto_inline_class.cpp.
|
protected |
Definition at line 541 of file goto_inline_class.cpp.
|
protected |
Definition at line 223 of file goto_inline_class.cpp.
|
protected |
Definition at line 603 of file goto_inline_class.cpp.
void goto_inlinet::output_cache | ( | std::ostream & | out | ) | const |
Definition at line 712 of file goto_inline_class.cpp.
|
inline |
Definition at line 72 of file goto_inline_class.h.
void goto_inlinet::output_inline_map | ( | std::ostream & | out, |
const inline_mapt & | inline_map | ||
) |
Definition at line 669 of file goto_inline_class.cpp.
|
protected |
Definition at line 30 of file goto_inline_class.cpp.
|
protected |
Definition at line 131 of file goto_inline_class.cpp.
|
protected |
Definition at line 157 of file goto_inline_class.cpp.
|
protected |
Definition at line 129 of file goto_inline_class.h.
|
protected |
Definition at line 193 of file goto_inline_class.h.
|
protected |
Definition at line 130 of file goto_inline_class.h.
|
protected |
Definition at line 196 of file goto_inline_class.h.
|
protected |
Definition at line 126 of file goto_inline_class.h.
|
protected |
Definition at line 132 of file goto_inline_class.h.
|
protected |
Definition at line 125 of file goto_inline_class.h.
|
protected |
Definition at line 202 of file goto_inline_class.h.
|
protected |
Definition at line 127 of file goto_inline_class.h.
|
protected |
Definition at line 199 of file goto_inline_class.h.