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 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) |
Protected Types | |
typedef goto_functionst::function_mapt | cachet |
typedef std::unordered_set< irep_idt, irep_id_hash > | finished_sett |
typedef std::unordered_set< irep_idt, irep_id_hash > | recursion_sett |
typedef std::unordered_set< irep_idt, irep_id_hash > | 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, 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_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 207 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 210 of file goto_inline_class.h.
typedef goto_functionst::goto_functiont goto_inlinet::goto_functiont |
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 216 of file goto_inline_class.h.
|
protected |
Definition at line 213 of file goto_inline_class.h.
|
inline |
Definition at line 24 of file goto_inline_class.h.
|
protected |
Definition at line 883 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 837 of file goto_inline_class.cpp.
References goto_functions_templatet< bodyT >::function_map, goto_functions, and is_call().
|
inlineprotected |
Definition at line 157 of file goto_inline_class.h.
References cache, finished_set, no_body_set, and recursion_set.
|
protected |
Definition at line 507 of file goto_inline_class.cpp.
References cache, caching, goto_inlinet::goto_inline_logt::cleanup(), goto_program_templatet< codeT, guardT >::empty(), messaget::eom(), goto_functions_templatet< bodyT >::function_map, get_call(), goto_functions, goto_inline_nontransitive(), goto_inline_transitive(), irept::id(), inline_log, insert_function_body(), insert_function_nobody(), is_call(), is_ignored(), ns, goto_programt::output_instruction(), 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 632 of file goto_inline_class.cpp.
References code_function_callt::arguments(), code_function_callt::function(), get_nil_irep(), is_bp_call(), is_call(), code_function_callt::lhs(), exprt::op0(), exprt::op1(), exprt::operands(), to_code_function_call(), and to_symbol_expr().
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 696 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 677 of file goto_inline_class.cpp.
References check_inline_map(), dstringt::empty(), Forall_goto_functions, goto_functions, and goto_inline().
|
protected |
Definition at line 711 of file goto_inline_class.cpp.
References check_inline_map(), expand_function_call(), finished_set, and recursion_set.
Referenced by expand_function_call(), and goto_inline().
|
protected |
Definition at line 765 of file goto_inline_class.cpp.
References cache, goto_inlinet::goto_inline_logt::copy_from(), messaget::eom(), expand_function_call(), inline_log, goto_program_templatet< codeT, guardT >::instructions, is_call(), messaget::progress(), and recursion_set.
Referenced by expand_function_call().
|
protected |
Definition at line 353 of file goto_inline_class.cpp.
References goto_inlinet::goto_inline_logt::add_segment(), adjust_function, goto_inlinet::goto_inline_logt::copy_from(), goto_program_templatet< codeT, guardT >::copy_from(), goto_program_templatet< codeT, guardT >::destructive_append(), goto_program_templatet< codeT, guardT >::destructive_insert(), goto_program_templatet< codeT, guardT >::empty(), Forall_goto_program_instructions, inline_log, goto_program_templatet< codeT, guardT >::instructions, is_call(), irept::is_not_nil(), code_assignt::lhs(), LOCATION, parameter_assignments(), parameter_destruction(), replace_location(), replace_return(), source_locationt::set_hide(), and to_code_assign().
Referenced by expand_function_call().
|
protected |
Definition at line 454 of file goto_inline_class.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), ASSIGN, goto_program_templatet< codeT, guardT >::destructive_insert(), goto_program_templatet< codeT, guardT >::empty(), messaget::eom(), forall_expr, is_call(), irept::is_not_nil(), LOCATION, no_body_set, messaget::mstreamt::source_location, exprt::type(), and messaget::warning().
Referenced by expand_function_call().
|
static |
Definition at line 666 of file goto_inline_class.cpp.
Referenced by get_call(), and is_call().
|
static |
Definition at line 661 of file goto_inline_class.cpp.
References is_bp_call().
Referenced by check_inline_map(), expand_function_call(), get_call(), goto_function_inline(), goto_function_inline_and_log(), goto_inline(), goto_inline_transitive(), goto_partial_inline(), insert_function_body(), insert_function_nobody(), parameter_assignments(), and parameter_destruction().
|
protected |
Definition at line 826 of file goto_inline_class.cpp.
Referenced by expand_function_call().
void goto_inlinet::output_cache | ( | std::ostream & | out | ) | const |
Definition at line 940 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 894 of file goto_inline_class.cpp.
References check_inline_map(), goto_functions_templatet< bodyT >::function_map, goto_functions, and ns.
|
protected |
Definition at line 30 of file goto_inline_class.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), adjust_function, ASSIGN, base_type_eq(), dstringt::empty(), goto_program_templatet< codeT, guardT >::empty(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), from_type(), code_typet::parametert::get_identifier(), irept::id(), goto_program_templatet< codeT, guardT >::instructions, is_call(), irept::is_nil(), namespacet::lookup(), exprt::make_typecast(), ns, code_typet::parameters(), 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 162 of file goto_inline_class.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), adjust_function, dstringt::empty(), goto_program_templatet< codeT, guardT >::empty(), messaget::eom(), messaget::error(), code_typet::parametert::get_identifier(), is_call(), namespacet::lookup(), ns, code_typet::parameters(), messaget::mstreamt::source_location, and symbolt::symbol_expr().
Referenced by insert_function_body().
|
protected |
Definition at line 206 of file goto_inline_class.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSIGN, exprt::copy_to_operands(), messaget::eom(), messaget::error(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, irept::is_not_nil(), exprt::is_true(), exprt::make_typecast(), exprt::move_to_operands(), exprt::op0(), OTHER, exprt::reserve_operands(), code_assignt::rhs(), messaget::mstreamt::source_location, exprt::type(), and messaget::warning().
Referenced by insert_function_body().
|
protected |
Definition at line 134 of file goto_inline_class.h.
Referenced by insert_function_body(), parameter_assignments(), and parameter_destruction().
|
protected |
Definition at line 208 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 135 of file goto_inline_class.h.
Referenced by expand_function_call().
|
protected |
Definition at line 211 of file goto_inline_class.h.
Referenced by clear(), and goto_inline_nontransitive().
|
protected |
Definition at line 131 of file goto_inline_class.h.
Referenced by check_inline_map(), expand_function_call(), goto_inline(), and output_inline_map().
|
protected |
Definition at line 137 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 217 of file goto_inline_class.h.
Referenced by clear(), and insert_function_nobody().
|
protected |
Definition at line 132 of file goto_inline_class.h.
Referenced by expand_function_call(), output_inline_map(), parameter_assignments(), and parameter_destruction().
|
protected |
Definition at line 214 of file goto_inline_class.h.
Referenced by clear(), expand_function_call(), goto_inline(), goto_inline_nontransitive(), and goto_inline_transitive().