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 std::unordered_set< irep_idt > &_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 std::unordered_set< irep_idt > & | typedef_names |
std::set< std::string > & | system_headers |
std::unordered_set< exprt, irep_hash > | va_list_expr |
natural_loopst | loops |
loopt | loop_map |
std::unordered_set< irep_idt > | labels_in_use |
dead_mapt | dead_map |
loop_last_stackt | loop_last_stack |
std::unordered_set< irep_idt > | local_static_set |
std::unordered_set< irep_idt > | type_names_set |
std::unordered_set< irep_idt > | const_removed |
Private Types | |
typedef std::list< irep_idt > | id_listt |
typedef std::map< goto_programt::const_targett, goto_programt::const_targett > | loopt |
typedef std::unordered_map< irep_idt, unsigned > | 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 45 of file goto_program2code.h.
|
private |
Definition at line 25 of file goto_program2code.h.
|
private |
Definition at line 22 of file goto_program2code.h.
|
private |
Definition at line 27 of file goto_program2code.h.
|
private |
Definition at line 24 of file goto_program2code.h.
|
inline |
Definition at line 48 of file goto_program2code.h.
References local_static, type_names, and type_names_set.
|
protected |
Definition at line 1432 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, loops, and UNREACHABLE.
Referenced by operator()().
Definition at line 1487 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 1609 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 1733 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 1829 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(), symbol_tablet::insert(), 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(), symbolt::name, ns, unary_exprt::op(), code_typet::parameters(), irept::remove(), code_typet::return_type(), simplify(), exprt::source_location(), irept::swap(), symbol_table, symbol_table_baset::symbols, system_headers, to_code_type(), to_constant_expr(), to_side_effect_expr(), to_string(), 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 1579 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 299 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 408 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 314 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_programt::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 1422 of file goto_program2code.cpp.
References UNREACHABLE.
Referenced by convert_instruction().
|
protected |
Definition at line 461 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_programt::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 523 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 548 of file goto_program2code.cpp.
References convert_goto_break_continue(), convert_goto_goto(), convert_goto_switch(), convert_goto_while(), goto_program, goto_programt::instructions, loop_last_stack, and loop_map.
Referenced by convert_instruction().
|
protected |
Definition at line 1146 of file goto_program2code.cpp.
References cfg_dominators_templatet< P, T, post_dom >::cfg, code_ifthenelset::cond(), convert_goto_goto(), exprt::copy_to_operands(), cfg_baset< T, P, I >::entry_map, natural_loops_templatet< P, T >::get_dominator_info(), goto_program, goto_programt::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 1235 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 1070 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_programt::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 891 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, goto_programt::instructiont::guard, irept::id(), goto_programt::insert_before(), goto_programt::insert_before_swap(), goto_programt::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, UNREACHABLE, and code_switcht::value().
Referenced by convert_goto(), and convert_goto_while().
|
protected |
Definition at line 571 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_programt::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 153 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, INCOMPLETE_GOTO, goto_programt::instructions, LOCATION, loop_map, exprt::move_to_operands(), NO_INSTRUCTION_TYPE, exprt::operands(), OTHER, RETURN, SKIP, START_THREAD, system_headers, THROW, and UNREACHABLE.
Referenced by convert_do_while(), convert_goto_if(), convert_goto_switch(), convert_goto_while(), convert_start_thread(), and operator()().
|
protected |
Definition at line 257 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 431 of file goto_program2code.cpp.
References exprt::copy_to_operands(), goto_program, code_returnt::has_return_value(), irept::id(), goto_programt::instructions, code_returnt::return_value(), to_code_return(), and to_side_effect_expr().
Referenced by convert_instruction().
|
protected |
Definition at line 1294 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_programt::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 1413 of file goto_program2code.cpp.
References UNREACHABLE.
Referenced by convert_instruction().
|
protected |
Definition at line 670 of file goto_program2code.cpp.
References goto_program, goto_programt::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_programt::instructions, labels_in_use, exprt::reserve_operands(), scan_for_varargs(), and toplevel_block.
|
protected |
Definition at line 1662 of file goto_program2code.cpp.
References struct_union_typet::components(), const_removed, irept::get_bool(), symbol_typet::get_identifier(), symbol_tablet::get_writeable(), irept::id(), id2string(), INVARIANT, symbolt::is_type, irept::remove(), typet::subtype(), symbol_table, to_struct_union_type(), to_symbol_type(), and symbolt::type.
Referenced by convert_decl().
|
protected |
Definition at line 829 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_programt::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(), symbol_table_baset::get_writeable_ref(), goto_program, irept::id(), code_assignt::lhs(), namespacet::lookup(), ns, unary_exprt::op(), code_typet::parameters(), r, code_assignt::rhs(), symbol_table, system_headers, to_code_assign(), to_code_type(), to_side_effect_expr(), to_typecast_expr(), symbolt::type, exprt::type(), and va_list_expr.
Referenced by operator()().
|
protected |
Definition at line 772 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, goto_programt::instructions, and UNREACHABLE.
Referenced by convert_goto_switch().
|
protected |
Definition at line 97 of file goto_program2code.h.
Referenced by remove_const().
|
protected |
Definition at line 93 of file goto_program2code.h.
Referenced by build_dead_map(), and convert_decl().
|
protected |
Definition at line 79 of file goto_program2code.h.
Referenced by scan_for_varargs().
|
protected |
Definition at line 80 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 92 of file goto_program2code.h.
Referenced by cleanup_code(), convert_goto_goto(), convert_labels(), convert_start_thread(), and operator()().
|
protected |
Definition at line 84 of file goto_program2code.h.
Referenced by cleanup_expr(), and goto_program2codet().
|
protected |
Definition at line 95 of file goto_program2code.h.
Referenced by cleanup_expr().
|
protected |
Definition at line 94 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 91 of file goto_program2code.h.
Referenced by build_loop_map(), convert_goto(), and convert_instruction().
|
protected |
Definition at line 90 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 82 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 81 of file goto_program2code.h.
Referenced by cleanup_expr(), remove_const(), and scan_for_varargs().
|
protected |
Definition at line 87 of file goto_program2code.h.
Referenced by cleanup_expr(), convert_instruction(), convert_start_thread(), and scan_for_varargs().
|
protected |
Definition at line 83 of file goto_program2code.h.
Referenced by convert_decl(), convert_goto_switch(), and operator()().
|
protected |
Definition at line 85 of file goto_program2code.h.
Referenced by add_local_types(), and goto_program2codet().
|
protected |
Definition at line 96 of file goto_program2code.h.
Referenced by add_local_types(), and goto_program2codet().
|
protected |
Definition at line 86 of file goto_program2code.h.
Referenced by cleanup_code(), and cleanup_expr().
Definition at line 88 of file goto_program2code.h.
Referenced by cleanup_code(), convert_assign(), convert_decl(), and scan_for_varargs().