cprover
|
#include <goto_program2code.h>
Classes | |
struct | caset |
Public Member Functions | |
goto_program2codet (const irep_idt &identifier, const goto_programt &_goto_program, symbol_tablet &_symbol_table, code_blockt &_dest, id_listt &_local_static, id_listt &_type_names, const id_sett &_typedef_names, std::set< std::string > &_system_headers) | |
void | operator() () |
Protected Attributes | |
const irep_idt & | func_name |
const goto_programt & | goto_program |
symbol_tablet & | symbol_table |
const namespacet | ns |
code_blockt & | toplevel_block |
id_listt & | local_static |
id_listt & | type_names |
const id_sett & | typedef_names |
std::set< std::string > & | system_headers |
std::unordered_set< exprt, irep_hash > | va_list_expr |
natural_loopst | loops |
loopt | loop_map |
id_sett | labels_in_use |
dead_mapt | dead_map |
loop_last_stackt | loop_last_stack |
id_sett | local_static_set |
id_sett | type_names_set |
id_sett | const_removed |
Private Types | |
typedef std::list< irep_idt > | id_listt |
typedef std::unordered_set< irep_idt, irep_id_hash > | id_sett |
typedef std::map< goto_programt::const_targett, goto_programt::const_targett > | loopt |
typedef std::unordered_map< irep_idt, unsigned, irep_id_hash > | dead_mapt |
typedef std::list< std::pair< goto_programt::const_targett, bool > > | loop_last_stackt |
typedef std::list< caset > | cases_listt |
Definition at line 20 of file goto_program2code.h.
|
private |
Definition at line 46 of file goto_program2code.h.
|
private |
Definition at line 26 of file goto_program2code.h.
|
private |
Definition at line 22 of file goto_program2code.h.
|
private |
Definition at line 23 of file goto_program2code.h.
|
private |
Definition at line 28 of file goto_program2code.h.
|
private |
Definition at line 25 of file goto_program2code.h.
|
inline |
Definition at line 49 of file goto_program2code.h.
References local_static, type_names, and type_names_set.
|
protected |
Definition at line 1433 of file goto_program2code.cpp.
References struct_union_typet::components(), dstringt::empty(), namespace_baset::follow(), source_locationt::get_function(), symbol_typet::get_identifier(), tag_typet::get_identifier(), irept::id(), symbolt::location, namespacet::lookup(), ns, typet::subtype(), to_c_enum_tag_type(), to_struct_union_type(), to_symbol_type(), type_names, and type_names_set.
Referenced by cleanup_code(), and cleanup_expr().
|
protected |
Definition at line 95 of file goto_program2code.cpp.
References dead_map, forall_goto_program_instructions, code_deadt::get_identifier(), goto_program, and to_code_dead().
Referenced by operator()().
|
protected |
Definition at line 59 of file goto_program2code.cpp.
References goto_program, natural_loops_templatet< P, T >::loop_map, loop_map, and loops.
Referenced by operator()().
Definition at line 1488 of file goto_program2code.cpp.
References add_local_types(), code_function_callt::arguments(), side_effect_expr_function_callt::arguments(), code_dowhilet::body(), cleanup_code_block(), cleanup_code_ifthenelse(), cleanup_expr(), cleanup_function_call(), code_labelt::code(), code_dowhilet::cond(), dstringt::empty(), Forall_expr, Forall_operands, code_function_callt::function(), side_effect_expr_function_callt::function(), irept::get(), code_labelt::get_label(), codet::get_statement(), exprt::has_operands(), irept::id(), exprt::is_false(), irept::is_not_nil(), labels_in_use, code_function_callt::lhs(), exprt::op0(), exprt::op1(), exprt::operands(), irept::remove(), codet::set_statement(), irept::swap(), to_array_type(), to_code(), to_code_dowhile(), to_code_function_call(), to_code_label(), to_side_effect_expr(), to_side_effect_expr_function_call(), to_typecast_expr(), exprt::type(), typedef_names, and va_list_expr.
Referenced by cleanup_code_ifthenelse(), and operator()().
Definition at line 1610 of file goto_program2code.cpp.
References dstringt::empty(), forall_operands, codet::get_statement(), exprt::op0(), exprt::operands(), size_type(), irept::swap(), and to_code().
Referenced by cleanup_code().
|
protected |
Definition at line 1734 of file goto_program2code.cpp.
References cleanup_code(), cleanup_expr(), code_ifthenelset::cond(), code_ifthenelset::else_case(), codet::get_statement(), has_labels(), exprt::is_false(), irept::is_nil(), irept::is_not_nil(), exprt::is_true(), irept::make_nil(), move_label_ifthenelse(), exprt::move_to_operands(), ns, simplify(), simplify_expr(), irept::swap(), code_ifthenelset::then_case(), to_code(), and to_code_ifthenelse().
Referenced by cleanup_code().
|
protected |
Definition at line 1830 of file goto_program2code.cpp.
References add_local_types(), exprt::add_source_location(), configt::ansi_c, symbolt::base_name, config, dstringt::empty(), irept::find(), namespace_baset::follow(), Forall_operands, from_integer(), side_effect_expr_function_callt::function(), irept::get(), irept::get_bool(), source_locationt::get_function(), symbol_exprt::get_identifier(), side_effect_exprt::get_statement(), has_prefix(), irept::id(), id2string(), configt::ansi_ct::int_width, exprt::is_constant(), symbolt::is_extern, ieee_floatt::is_infinity(), ieee_floatt::is_NaN(), irept::is_not_nil(), symbolt::is_static_lifetime, exprt::is_true(), local_static, local_static_set, symbolt::location, namespacet::lookup(), exprt::make_typecast(), symbol_tablet::move(), symbolt::name, ns, unary_exprt::op(), typecast_exprt::op(), code_typet::parameters(), irept::remove(), code_typet::return_type(), simplify(), exprt::source_location(), irept::swap(), symbol_table, symbol_tablet::symbols, system_headers, to_code_type(), to_constant_expr(), to_side_effect_expr(), to_symbol_expr(), to_typecast_expr(), to_union_expr(), symbolt::type, exprt::type(), type_eq(), typedef_names, and symbolt::value.
Referenced by cleanup_code(), and cleanup_code_ifthenelse().
|
protected |
Definition at line 1580 of file goto_program2code.cpp.
References namespace_baset::follow(), Forall_expr, symbol_exprt::get_identifier(), namespacet::lookup(), ns, code_typet::parameters(), to_code_type(), to_symbol_expr(), and symbolt::type.
Referenced by cleanup_code().
|
protected |
Definition at line 302 of file goto_program2code.cpp.
References convert_assign_rec(), convert_assign_varargs(), code_assignt::lhs(), to_code_assign(), and va_list_expr.
Referenced by convert_instruction().
|
protected |
Definition at line 410 of file goto_program2code.cpp.
References exprt::copy_to_operands(), namespace_baset::follow(), forall_operands, from_integer(), irept::id(), index_type(), code_assignt::lhs(), ns, code_assignt::rhs(), typet::subtype(), to_array_type(), and exprt::type().
Referenced by convert_assign().
|
protected |
Definition at line 317 of file goto_program2code.cpp.
References side_effect_expr_function_callt::arguments(), side_effect_expr_function_callt::function(), side_effect_exprt::get_statement(), constant_exprt::get_value(), goto_program, irept::id(), goto_program_templatet< codeT, guardT >::instructions, code_assignt::lhs(), code_function_callt::lhs(), irept::make_nil(), exprt::move_to_operands(), pointer_type(), r, code_assignt::rhs(), skip_typecast(), to_address_of_expr(), to_code_assign(), to_constant_expr(), to_dereference_expr(), and to_side_effect_expr().
Referenced by convert_assign().
|
protected |
Definition at line 1423 of file goto_program2code.cpp.
Referenced by convert_instruction().
|
protected |
Definition at line 463 of file goto_program2code.cpp.
References code_function_callt::arguments(), side_effect_expr_function_callt::arguments(), convert_labels(), exprt::copy_to_operands(), dead_map, code_function_callt::function(), side_effect_expr_function_callt::function(), symbol_exprt::get_identifier(), goto_program, goto_program_templatet< codeT, guardT >::instructions, code_assignt::lhs(), code_function_callt::lhs(), exprt::move_to_operands(), remove_const(), code_assignt::rhs(), code_declt::symbol(), to_code_assign(), to_code_decl(), to_code_function_call(), to_symbol_expr(), toplevel_block, exprt::type(), and va_list_expr.
Referenced by convert_instruction().
|
protected |
Definition at line 525 of file goto_program2code.cpp.
References code_dowhilet::cond(), convert_instruction(), convert_labels(), loop_last_stack, exprt::move_to_operands(), ns, and simplify().
Referenced by convert_instruction().
|
protected |
Definition at line 550 of file goto_program2code.cpp.
References convert_goto_break_continue(), convert_goto_goto(), convert_goto_switch(), convert_goto_while(), goto_program, goto_program_templatet< codeT, guardT >::instructions, loop_last_stack, and loop_map.
Referenced by convert_instruction().
|
protected |
Definition at line 1148 of file goto_program2code.cpp.
References code_ifthenelset::cond(), convert_goto_goto(), exprt::copy_to_operands(), natural_loops_templatet< P, T >::get_dominator_info(), goto_program, goto_program_templatet< codeT, guardT >::instructions, exprt::is_true(), loop_last_stack, loops, exprt::move_to_operands(), ns, simplify(), irept::swap(), and code_ifthenelset::then_case().
Referenced by convert_goto(), and convert_goto_if().
|
protected |
Definition at line 1237 of file goto_program2code.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, code_ifthenelset::cond(), cfg_baset< T, P, I >::entry_map, natural_loops_templatet< P, T >::get_dominator_info(), has_prefix(), id2string(), labels_in_use, loops, exprt::move_to_operands(), ns, simplify(), irept::swap(), and code_ifthenelset::then_case().
Referenced by convert_goto(), convert_goto_break_continue(), convert_goto_if(), convert_goto_switch(), and convert_goto_while().
|
protected |
Definition at line 1072 of file goto_program2code.cpp.
References code_ifthenelset::cond(), convert_goto_break_continue(), convert_goto_goto(), convert_instruction(), convert_labels(), exprt::copy_to_operands(), code_ifthenelset::else_case(), goto_program, goto_program_templatet< codeT, guardT >::instructions, loop_last_stack, exprt::move_to_operands(), ns, simplify(), code_ifthenelset::then_case(), and to_code().
Referenced by convert_goto_switch().
|
protected |
Definition at line 893 of file goto_program2code.cpp.
References code_switcht::body(), code_switch_caset::case_op(), cfg_dominators_templatet< P, T, post_dom >::cfg, code_switch_caset::code(), convert_goto_goto(), convert_goto_if(), convert_instruction(), convert_labels(), grapht< N >::empty(), cfg_baset< T, P, I >::entry_map, get_cases(), natural_loops_templatet< P, T >::get_dominator_info(), goto_program, irept::id(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, exprt::is_constant(), binary_relation_exprt::lhs(), loop_last_stack, loops, exprt::move_to_operands(), exprt::op0(), exprt::operands(), remove_default(), set_block_end_points(), code_switch_caset::set_default(), skip_typecast(), irept::swap(), to_code(), to_code_switch_case(), to_equal_expr(), toplevel_block, and code_switcht::value().
Referenced by convert_goto(), and convert_goto_while().
|
protected |
Definition at line 573 of file goto_program2code.cpp.
References code_whilet::body(), code_dowhilet::body(), code_fort::body(), code_ifthenelset::cond(), code_whilet::cond(), code_dowhilet::cond(), code_fort::cond(), convert_goto_goto(), convert_goto_switch(), convert_instruction(), convert_labels(), codet::get_statement(), goto_program, exprt::has_operands(), irept::id(), code_fort::init(), goto_program_templatet< codeT, guardT >::instructions, exprt::is_true(), code_fort::iter(), loop_last_stack, irept::make_nil(), exprt::move_to_operands(), ns, exprt::operands(), simplify(), irept::swap(), code_ifthenelset::then_case(), to_code(), and to_code_ifthenelse().
Referenced by convert_goto().
|
protected |
Definition at line 156 of file goto_program2code.cpp.
References ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, CATCH, convert_assign(), convert_catch(), convert_decl(), convert_do_while(), convert_goto(), convert_labels(), convert_return(), convert_start_thread(), convert_throw(), exprt::copy_to_operands(), DEAD, DECL, END_FUNCTION, END_THREAD, code_function_callt::function(), FUNCTION_CALL, GOTO, goto_program, goto_program_templatet< codeT, guardT >::instructions, LOCATION, loop_map, exprt::move_to_operands(), NO_INSTRUCTION_TYPE, exprt::operands(), OTHER, RETURN, code_typet::return_type(), SKIP, START_THREAD, system_headers, and THROW.
Referenced by convert_do_while(), convert_goto_if(), convert_goto_switch(), convert_goto_while(), convert_start_thread(), and operator()().
|
protected |
Definition at line 260 of file goto_program2code.cpp.
References exprt::add_source_location(), code_labelt::code(), exprt::copy_to_operands(), has_prefix(), id2string(), labels_in_use, exprt::move_to_operands(), exprt::operands(), to_code(), and to_code_label().
Referenced by convert_decl(), convert_do_while(), convert_goto_if(), convert_goto_switch(), convert_goto_while(), and convert_instruction().
|
protected |
Definition at line 433 of file goto_program2code.cpp.
References exprt::copy_to_operands(), goto_program, code_returnt::has_return_value(), irept::id(), goto_program_templatet< codeT, guardT >::instructions, code_returnt::return_value(), to_code_return(), and to_side_effect_expr().
Referenced by convert_instruction().
|
protected |
Definition at line 1296 of file goto_program2code.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), code_labelt::code(), convert_instruction(), code_function_callt::function(), codet::get_statement(), goto_program, has_prefix(), id2string(), goto_program_templatet< codeT, guardT >::instructions, labels_in_use, code_function_callt::lhs(), exprt::move_to_operands(), pointer_type(), irept::swap(), system_headers, to_code(), and to_code_function_call().
Referenced by convert_instruction().
|
protected |
Definition at line 1414 of file goto_program2code.cpp.
Referenced by convert_instruction().
|
protected |
Definition at line 672 of file goto_program2code.cpp.
References goto_program, goto_program_templatet< codeT, guardT >::instructions, binary_relation_exprt::lhs(), binary_relation_exprt::rhs(), skip_typecast(), and to_equal_expr().
Referenced by convert_goto_switch().
void goto_program2codet::operator() | ( | void | ) |
Definition at line 32 of file goto_program2code.cpp.
References build_dead_map(), build_loop_map(), cleanup_code(), convert_instruction(), forall_goto_program_instructions, goto_program, goto_program_templatet< codeT, guardT >::instructions, labels_in_use, exprt::reserve_operands(), scan_for_varargs(), and toplevel_block.
|
protected |
Definition at line 1663 of file goto_program2code.cpp.
References struct_union_typet::components(), const_removed, irept::get_bool(), symbol_typet::get_identifier(), irept::id(), irept::remove(), typet::subtype(), symbol_table, symbol_tablet::symbols, to_struct_union_type(), and to_symbol_type().
Referenced by convert_decl().
|
protected |
Definition at line 831 of file goto_program2code.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, cfg_baset< T, P, I >::entry_map, goto_program, and goto_program_templatet< codeT, guardT >::instructions.
Referenced by convert_goto_switch().
|
protected |
Definition at line 106 of file goto_program2code.cpp.
References forall_goto_program_instructions, func_name, irept::get(), side_effect_exprt::get_statement(), goto_program, irept::id(), code_assignt::lhs(), namespacet::lookup(), ns, typecast_exprt::op(), r, code_assignt::rhs(), symbol_table, symbol_tablet::symbols, system_headers, to_code_assign(), to_code_type(), to_side_effect_expr(), to_typecast_expr(), exprt::type(), and va_list_expr.
Referenced by operator()().
|
protected |
Definition at line 774 of file goto_program2code.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, END_FUNCTION, cfg_baset< T, P, I >::entry_map, goto_program, and goto_program_templatet< codeT, guardT >::instructions.
Referenced by convert_goto_switch().
|
protected |
Definition at line 98 of file goto_program2code.h.
Referenced by remove_const().
|
protected |
Definition at line 94 of file goto_program2code.h.
Referenced by build_dead_map(), and convert_decl().
|
protected |
Definition at line 80 of file goto_program2code.h.
Referenced by scan_for_varargs().
|
protected |
Definition at line 81 of file goto_program2code.h.
Referenced by build_dead_map(), build_loop_map(), convert_assign_varargs(), convert_decl(), convert_goto(), convert_goto_break_continue(), convert_goto_if(), convert_goto_switch(), convert_goto_while(), convert_instruction(), convert_return(), convert_start_thread(), get_cases(), operator()(), remove_default(), scan_for_varargs(), and set_block_end_points().
|
protected |
Definition at line 93 of file goto_program2code.h.
Referenced by cleanup_code(), convert_goto_goto(), convert_labels(), convert_start_thread(), and operator()().
|
protected |
Definition at line 85 of file goto_program2code.h.
Referenced by cleanup_expr(), and goto_program2codet().
|
protected |
Definition at line 96 of file goto_program2code.h.
Referenced by cleanup_expr().
|
protected |
Definition at line 95 of file goto_program2code.h.
Referenced by convert_do_while(), convert_goto(), convert_goto_break_continue(), convert_goto_if(), convert_goto_switch(), and convert_goto_while().
|
protected |
Definition at line 92 of file goto_program2code.h.
Referenced by build_loop_map(), convert_goto(), and convert_instruction().
|
protected |
Definition at line 91 of file goto_program2code.h.
Referenced by build_loop_map(), convert_goto_break_continue(), convert_goto_goto(), and convert_goto_switch().
|
protected |
Definition at line 83 of file goto_program2code.h.
Referenced by add_local_types(), cleanup_code_ifthenelse(), cleanup_expr(), cleanup_function_call(), convert_assign_rec(), convert_do_while(), convert_goto_break_continue(), convert_goto_goto(), convert_goto_if(), convert_goto_while(), and scan_for_varargs().
|
protected |
Definition at line 82 of file goto_program2code.h.
Referenced by cleanup_expr(), remove_const(), and scan_for_varargs().
|
protected |
Definition at line 88 of file goto_program2code.h.
Referenced by cleanup_expr(), convert_instruction(), convert_start_thread(), and scan_for_varargs().
|
protected |
Definition at line 84 of file goto_program2code.h.
Referenced by convert_decl(), convert_goto_switch(), and operator()().
|
protected |
Definition at line 86 of file goto_program2code.h.
Referenced by add_local_types(), and goto_program2codet().
|
protected |
Definition at line 97 of file goto_program2code.h.
Referenced by add_local_types(), and goto_program2codet().
|
protected |
Definition at line 87 of file goto_program2code.h.
Referenced by cleanup_code(), and cleanup_expr().
Definition at line 89 of file goto_program2code.h.
Referenced by cleanup_code(), convert_assign(), convert_decl(), and scan_for_varargs().