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 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_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 21 of file goto_inline_class.h.
|
protected |
Definition at line 193 of file goto_inline_class.h.
typedef std::list<callt> goto_inlinet::call_listt |
Definition at line 46 of file goto_inline_class.h.
typedef std::pair<goto_programt::targett, bool> goto_inlinet::callt |
Definition at line 43 of file goto_inline_class.h.
|
protected |
Definition at line 196 of file goto_inline_class.h.
Definition at line 38 of file goto_inline_class.h.
typedef std::map<irep_idt, call_listt> goto_inlinet::inline_mapt |
Definition at line 49 of file goto_inline_class.h.
|
protected |
Definition at line 202 of file goto_inline_class.h.
|
protected |
Definition at line 199 of file goto_inline_class.h.
|
inline |
Definition at line 24 of file goto_inline_class.h.
|
protected |
Definition at line 728 of file goto_inline_class.cpp.
References forall_goto_functions, and goto_functions.
Referenced by goto_inline(), goto_inline_nontransitive(), and output_inline_map().
|
protected |
Definition at line 684 of file goto_inline_class.cpp.
References goto_functionst::function_map, goto_functions, and PRECONDITION.
|
inlineprotected |
Definition at line 152 of file goto_inline_class.h.
References cache, finished_set, no_body_set, and recursion_set.
|
protected |
Definition at line 381 of file goto_inline_class.cpp.
References goto_functiont::body, goto_functiont::body_available(), cache, caching, goto_inlinet::goto_inline_logt::cleanup(), goto_programt::empty(), messaget::eom(), goto_functionst::function_map, get_call(), goto_functions, goto_inline_nontransitive(), goto_inline_transitive(), irept::id(), inline_log, insert_function_body(), goto_programt::instructions, is_ignored(), no_body_set, ns, goto_programt::output_instruction(), PRECONDITION, messaget::progress(), recursion_set, messaget::mstreamt::source_location, to_symbol_expr(), and messaget::warning().
Referenced by goto_inline_nontransitive(), and goto_inline_transitive().
|
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().
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().
void goto_inlinet::goto_inline | ( | const inline_mapt & | inline_map, |
const bool | force_full = false |
||
) |
Definition at line 524 of file goto_inline_class.cpp.
References check_inline_map(), DATA_INVARIANT, dstringt::empty(), Forall_goto_functions, goto_functions, goto_inline(), and PRECONDITION.
|
protected |
Definition at line 558 of file goto_inline_class.cpp.
References goto_functiont::body, goto_functiont::body_available(), check_inline_map(), expand_function_call(), finished_set, goto_program, PRECONDITION, and recursion_set.
Referenced by expand_function_call(), and goto_inline().
|
protected |
Definition at line 610 of file goto_inline_class.cpp.
References goto_functiont::body, goto_functiont::body_available(), cache, goto_functiont::copy_from(), goto_inlinet::goto_inline_logt::copy_from(), DATA_INVARIANT, goto_programt::empty(), messaget::eom(), expand_function_call(), Forall_goto_program_instructions, goto_program, inline_log, goto_programt::instructions, INVARIANT, PRECONDITION, messaget::progress(), and recursion_set.
Referenced by expand_function_call().
|
protected |
Definition at line 277 of file goto_inline_class.cpp.
References goto_inlinet::goto_inline_logt::add_segment(), adjust_function, goto_functiont::body, goto_functiont::body_available(), goto_inlinet::goto_inline_logt::copy_from(), goto_programt::copy_from(), DATA_INVARIANT, goto_programt::destructive_append(), goto_programt::destructive_insert(), goto_programt::empty(), Forall_goto_program_instructions, inline_log, goto_programt::instructions, goto_programt::instructiont::is_end_function(), goto_functiont::is_hidden(), irept::is_not_nil(), code_assignt::lhs(), LOCATION, parameter_assignments(), parameter_destruction(), PRECONDITION, replace_location(), replace_return(), source_locationt::set_hide(), to_code_assign(), goto_functiont::type, and goto_programt::instructiont::type.
Referenced by expand_function_call().
|
protected |
Definition at line 673 of file goto_inline_class.cpp.
Referenced by expand_function_call().
void goto_inlinet::output_cache | ( | std::ostream & | out | ) | const |
Definition at line 782 of file goto_inline_class.cpp.
References cache.
|
inline |
Definition at line 73 of file goto_inline_class.h.
References cache, goto_inlinet::goto_inline_logt::cleanup(), inline_log, and goto_inlinet::goto_inline_logt::output_inline_log_json().
void goto_inlinet::output_inline_map | ( | std::ostream & | out, |
const inline_mapt & | inline_map | ||
) |
Definition at line 739 of file goto_inline_class.cpp.
References goto_functiont::body, goto_functiont::body_available(), check_inline_map(), goto_functionst::function_map, goto_functions, goto_program, ns, goto_programt::output_instruction(), and PRECONDITION.
|
protected |
Definition at line 33 of file goto_inline_class.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), adjust_function, ASSIGN, base_type_eq(), dstringt::empty(), goto_programt::empty(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), from_type(), irept::id(), goto_programt::instructions, irept::is_nil(), namespacet::lookup(), exprt::make_typecast(), ns, code_typet::parameters(), PRECONDITION, irept::pretty(), messaget::mstreamt::source_location, typet::subtype(), symbolt::symbol_expr(), exprt::type(), and messaget::warning().
Referenced by insert_function_body().
|
protected |
Definition at line 160 of file goto_inline_class.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), adjust_function, dstringt::empty(), goto_programt::empty(), messaget::eom(), messaget::error(), namespacet::lookup(), ns, code_typet::parameters(), PRECONDITION, messaget::mstreamt::source_location, and symbolt::symbol_expr().
Referenced by insert_function_body().
|
protected |
Definition at line 199 of file goto_inline_class.cpp.
References ASSIGN, messaget::eom(), goto_programt::instructions, irept::is_not_nil(), exprt::make_typecast(), exprt::op0(), OTHER, code_assignt::rhs(), messaget::mstreamt::source_location, exprt::type(), and messaget::warning().
Referenced by insert_function_body().
|
protected |
Definition at line 129 of file goto_inline_class.h.
Referenced by insert_function_body(), parameter_assignments(), and parameter_destruction().
|
protected |
Definition at line 194 of file goto_inline_class.h.
Referenced by clear(), expand_function_call(), goto_inline_transitive(), output_cache(), and output_inline_log_json().
|
protected |
Definition at line 130 of file goto_inline_class.h.
Referenced by expand_function_call().
|
protected |
Definition at line 197 of file goto_inline_class.h.
Referenced by clear(), and goto_inline_nontransitive().
|
protected |
Definition at line 126 of file goto_inline_class.h.
Referenced by check_inline_map(), expand_function_call(), goto_inline(), and output_inline_map().
|
protected |
Definition at line 132 of file goto_inline_class.h.
Referenced by expand_function_call(), goto_inline_transitive(), insert_function_body(), and output_inline_log_json().
|
protected |
Definition at line 203 of file goto_inline_class.h.
Referenced by clear(), and expand_function_call().
|
protected |
Definition at line 127 of file goto_inline_class.h.
Referenced by expand_function_call(), output_inline_map(), parameter_assignments(), and parameter_destruction().
|
protected |
Definition at line 200 of file goto_inline_class.h.
Referenced by clear(), expand_function_call(), goto_inline(), goto_inline_nontransitive(), and goto_inline_transitive().