cprover
|
#include <goto_convert_class.h>
Classes | |
struct | break_continue_targetst |
struct | break_switch_targetst |
struct | guarded_gotot |
struct | leave_targett |
struct | targetst |
struct | throw_targett |
Public Member Functions | |
void | goto_convert (const codet &code, goto_programt &dest) |
goto_convertt (symbol_tablet &_symbol_table, message_handlert &_message_handler) | |
virtual | ~goto_convertt () |
Protected Types | |
typedef std::vector< codet > | destructor_stackt |
typedef std::map< irep_idt, std::pair< goto_programt::targett, destructor_stackt > > | labelst |
typedef std::list< std::pair< goto_programt::targett, destructor_stackt > > | gotost |
typedef std::list< goto_programt::targett > | computed_gotost |
typedef exprt::operandst | caset |
typedef std::list< std::pair< goto_programt::targett, caset > > | casest |
typedef std::map< goto_programt::targett, casest::iterator > | cases_mapt |
typedef std::list< guarded_gotot > | guarded_gotost |
Static Protected Member Functions | |
static bool | needs_cleaning (const exprt &expr) |
static bool | has_sideeffect (const exprt &expr) |
static bool | has_function_call (const exprt &expr) |
static void | replace_new_object (const exprt &object, exprt &dest) |
static void | collect_operands (const exprt &expr, const irep_idt &id, std::list< exprt > &dest) |
Protected Attributes | |
symbol_tablet & | symbol_table |
namespacet | ns |
unsigned | temporary_counter |
std::string | tmp_symbol_prefix |
struct goto_convertt::targetst | targets |
guarded_gotost | guarded_gotos |
Additional Inherited Members |
Definition at line 26 of file goto_convert_class.h.
|
protected |
Definition at line 292 of file goto_convert_class.h.
|
protected |
Definition at line 291 of file goto_convert_class.h.
|
protected |
Definition at line 290 of file goto_convert_class.h.
|
protected |
Definition at line 289 of file goto_convert_class.h.
|
protected |
Definition at line 263 of file goto_convert_class.h.
|
protected |
Definition at line 288 of file goto_convert_class.h.
|
protected |
Definition at line 474 of file goto_convert_class.h.
|
protected |
Definition at line 286 of file goto_convert_class.h.
|
inline |
Definition at line 31 of file goto_convert_class.h.
|
inlinevirtual |
Definition at line 42 of file goto_convert_class.h.
Definition at line 1190 of file goto_convert.cpp.
References forall_expr, binary_relation_exprt::lhs(), exprt::move_to_operands(), exprt::op0(), exprt::operands(), exprt::reserve_operands(), binary_relation_exprt::rhs(), and irept::swap().
Referenced by convert_switch().
|
protected |
Definition at line 163 of file goto_clean_expr.cpp.
References exprt::add_source_location(), side_effect_expr_function_callt::arguments(), clean_expr_address_of(), if_exprt::cond(), convert(), convert_assign(), messaget::eom(), messaget::error(), if_exprt::false_case(), exprt::find_source_location(), Forall_operands, generate_ifthenelse(), side_effect_exprt::get_statement(), irept::id(), exprt::is_boolean(), exprt::is_false(), irept::is_nil(), irept::is_not_nil(), exprt::is_true(), code_assignt::lhs(), irept::make_nil(), needs_cleaning(), new_tmp_symbol(), ns, exprt::op0(), exprt::op1(), exprt::operands(), irept::pretty(), remove_gcc_conditional_expression(), remove_side_effect(), remove_statement_expression(), messaget::result(), rewrite_boolean(), code_assignt::rhs(), simplify(), exprt::source_location(), messaget::mstreamt::source_location, irept::swap(), symbolt::symbol_expr(), to_if_expr(), to_side_effect_expr(), to_side_effect_expr_function_call(), to_symbol_expr(), if_exprt::true_case(), and exprt::type().
Referenced by clean_expr_address_of(), convert_assert(), convert_assign(), convert_assume(), convert_bp_abortif(), convert_bp_enforce(), convert_cpp_delete(), convert_dowhile(), convert_expression(), convert_for(), convert_ifthenelse(), convert_loop_invariant(), convert_return(), convert_switch(), do_cpp_new(), do_function_call(), generate_conditional_branch(), and remove_gcc_conditional_expression().
|
protected |
Definition at line 440 of file goto_clean_expr.cpp.
References clean_expr(), convert(), Forall_operands, irept::id(), make_compound_literal(), exprt::op0(), exprt::op1(), exprt::operands(), messaget::result(), and irept::swap().
Referenced by clean_expr().
|
staticprotected |
Definition at line 1737 of file goto_convert.cpp.
References forall_operands, and irept::id().
Referenced by generate_conditional_branch().
|
protected |
converts 'code' and appends the result to 'dest'
Definition at line 448 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), convert_asm(), convert_assert(), convert_assign(), convert_assume(), convert_atomic_begin(), convert_atomic_end(), convert_block(), convert_bp_abortif(), convert_bp_enforce(), convert_break(), convert_continue(), convert_cpp_delete(), convert_CPROVER_throw(), convert_CPROVER_try_catch(), convert_CPROVER_try_finally(), convert_decl(), convert_decl_type(), convert_dowhile(), convert_end_thread(), convert_expression(), convert_for(), convert_function_call(), convert_gcc_computed_goto(), convert_gcc_local_label(), convert_gcc_switch_case_range(), convert_goto(), convert_ifthenelse(), convert_init(), convert_label(), convert_msc_leave(), convert_msc_try_except(), convert_msc_try_finally(), convert_non_deterministic_goto(), convert_return(), convert_skip(), convert_specc_notify(), convert_specc_par(), convert_specc_wait(), convert_start_thread(), convert_switch(), convert_switch_case(), convert_try_catch(), convert_while(), copy(), DEAD, messaget::eom(), messaget::error(), exprt::find_source_location(), forall_operands, codet::get_statement(), get_string_constant(), goto_program_templatet< codeT, guardT >::instructions, exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::operands(), OTHER, simplify(), SKIP, exprt::source_location(), messaget::mstreamt::source_location, to_code(), to_code_asm(), to_code_assert(), to_code_assign(), to_code_assume(), to_code_block(), to_code_break(), to_code_continue(), to_code_decl(), to_code_expression(), to_code_for(), to_code_function_call(), to_code_ifthenelse(), to_code_label(), to_code_return(), to_code_switch(), to_code_switch_case(), and to_code_while().
Referenced by clean_expr(), clean_expr_address_of(), convert_block(), convert_bp_enforce(), convert_cpp_delete(), convert_CPROVER_try_catch(), convert_CPROVER_try_finally(), convert_dowhile(), convert_for(), convert_gcc_switch_case_range(), convert_ifthenelse(), convert_init(), convert_label(), convert_msc_leave(), convert_msc_try_except(), convert_msc_try_finally(), convert_start_thread(), convert_switch(), convert_switch_case(), convert_try_catch(), convert_while(), cpp_new_initializer(), do_array_equal(), do_cpp_new(), do_java_new_array(), goto_convert_rec(), make_compound_literal(), make_temp_symbol(), remove_assignment(), remove_cpp_new(), remove_malloc(), remove_post(), remove_pre(), remove_statement_expression(), remove_temporary_object(), and unwind_destructor_stack().
|
protected |
|
protected |
Definition at line 899 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSERT, code_assertt::assertion(), clean_expr(), irept::set(), and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 729 of file goto_convert.cpp.
References ASSIGN, clean_expr(), copy(), do_cpp_new(), do_function_call(), do_java_new(), do_java_new_array(), messaget::eom(), messaget::error(), Forall_operands, irept::id(), code_assignt::lhs(), exprt::make_typecast(), exprt::op0(), exprt::op1(), exprt::operands(), code_assignt::rhs(), messaget::mstreamt::source_location, irept::swap(), to_side_effect_expr(), and exprt::type().
Referenced by clean_expr(), convert(), convert_decl(), and remove_assignment().
|
protected |
Definition at line 923 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSUME, code_assumet::assumption(), clean_expr(), and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 1576 of file goto_convert.cpp.
References ATOMIC_BEGIN, copy(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::operands(), and messaget::mstreamt::source_location.
Referenced by convert().
|
protected |
Definition at line 1590 of file goto_convert.cpp.
References ATOMIC_END, copy(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::operands(), and messaget::mstreamt::source_location.
Referenced by convert().
|
protected |
Definition at line 581 of file goto_convert.cpp.
References convert(), goto_convertt::targetst::destructor_stack, goto_program_templatet< codeT, guardT >::empty(), code_blockt::end_location(), forall_operands, goto_program_templatet< codeT, guardT >::instructions, targets, to_code(), and unwind_destructor_stack().
Referenced by convert().
|
protected |
Definition at line 1663 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSERT, clean_expr(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::make_not(), exprt::op0(), exprt::operands(), exprt::source_location(), and messaget::mstreamt::source_location.
Referenced by convert().
|
protected |
Definition at line 1604 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSUME, clean_expr(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), Forall_goto_program_instructions, exprt::is_true(), make_next_state(), exprt::op0(), exprt::op1(), exprt::operands(), OTHER, exprt::source_location(), messaget::mstreamt::source_location, and to_code().
Referenced by convert().
|
protected |
Definition at line 1300 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_convertt::targetst::break_set, goto_convertt::targetst::break_stack_size, goto_convertt::targetst::break_target, messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::source_location(), messaget::mstreamt::source_location, targets, and unwind_destructor_stack().
Referenced by convert().
|
protected |
Definition at line 1391 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_convertt::targetst::continue_set, goto_convertt::targetst::continue_stack_size, goto_convertt::targetst::continue_target, messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::source_location(), messaget::mstreamt::source_location, targets, and unwind_destructor_stack().
Referenced by convert().
|
protected |
Definition at line 834 of file goto_convert.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), clean_expr(), convert(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), code_function_callt::function(), codet::get_statement(), irept::is_not_nil(), code_function_callt::lhs(), namespacet::lookup(), irept::make_nil(), ns, exprt::op0(), exprt::operands(), replace_new_object(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), to_code(), to_code_type(), and exprt::type().
Referenced by convert(), and remove_cpp_delete().
|
protected |
Definition at line 241 of file goto_convert_exceptions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSIGN, exception_flag(), goto_convertt::targetst::return_target, exprt::source_location(), targets, goto_convertt::targetst::throw_set, goto_convertt::targetst::throw_stack_size, goto_convertt::targetst::throw_target, and unwind_destructor_stack().
Referenced by convert().
|
protected |
Definition at line 204 of file goto_convert_exceptions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), code_ifthenelset::cond(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exception_flag(), exprt::find_source_location(), goto_program_templatet< codeT, guardT >::instructions, exprt::op0(), exprt::op1(), exprt::operands(), goto_convertt::targetst::set_throw(), SKIP, exprt::source_location(), messaget::mstreamt::source_location, targets, code_ifthenelset::then_case(), and to_code().
Referenced by convert().
|
protected |
Definition at line 278 of file goto_convert_exceptions.cpp.
References convert(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::op0(), exprt::op1(), exprt::operands(), messaget::mstreamt::source_location, targets, and to_code().
Referenced by convert().
|
protected |
Definition at line 655 of file goto_convert.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), convert_assign(), copy(), DECL, goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), irept::get(), get_destructor(), irept::id(), irept::is_not_nil(), symbolt::is_static_lifetime, lookup(), symbolt::name, ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_type(), exprt::source_location(), messaget::mstreamt::source_location, targets, and symbolt::type.
Referenced by convert(), new_tmp_symbol(), remove_cpp_new(), remove_function_call(), and remove_malloc().
|
protected |
Definition at line 722 of file goto_convert.cpp.
Referenced by convert().
|
protected |
Definition at line 1118 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), clean_expr(), convert(), convert_loop_invariant(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), goto_program_templatet< codeT, guardT >::instructions, exprt::op0(), exprt::op1(), exprt::operands(), goto_convertt::break_continue_targetst::restore(), goto_convertt::targetst::set_break(), goto_convertt::targetst::set_continue(), exprt::source_location(), messaget::mstreamt::source_location, targets, and to_code().
Referenced by convert().
|
protected |
Definition at line 1562 of file goto_convert.cpp.
References copy(), END_THREAD, messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::operands(), and messaget::mstreamt::source_location.
Referenced by convert().
|
protected |
Definition at line 612 of file goto_convert.cpp.
References exprt::add_source_location(), clean_expr(), code_ifthenelset::cond(), if_exprt::cond(), convert_ifthenelse(), copy(), code_ifthenelset::else_case(), messaget::eom(), messaget::error(), if_exprt::false_case(), exprt::find_source_location(), irept::id(), irept::is_not_nil(), exprt::op0(), exprt::operands(), OTHER, exprt::source_location(), messaget::mstreamt::source_location, code_ifthenelset::then_case(), to_if_expr(), and if_exprt::true_case().
Referenced by convert().
|
protected |
Definition at line 959 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), code_fort::body(), clean_expr(), code_fort::cond(), convert(), convert_loop_invariant(), goto_program_templatet< codeT, guardT >::destructive_append(), code_fort::init(), goto_program_templatet< codeT, guardT >::instructions, irept::is_nil(), irept::is_not_nil(), code_fort::iter(), exprt::make_not(), exprt::op2(), goto_convertt::break_continue_targetst::restore(), goto_convertt::targetst::set_break(), goto_convertt::targetst::set_continue(), SKIP, exprt::source_location(), targets, and to_code().
Referenced by convert().
|
protected |
Definition at line 24 of file goto_convert_function_call.cpp.
References code_function_callt::arguments(), do_function_call(), code_function_callt::function(), and code_function_callt::lhs().
Referenced by convert(), and remove_function_call().
|
protected |
Definition at line 1425 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_convertt::targetst::computed_gotos, exprt::source_location(), and targets.
Referenced by convert().
|
protected |
Definition at line 368 of file goto_convert.cpp.
Referenced by convert().
|
protected |
Definition at line 414 of file goto_convert.cpp.
References goto_convertt::targetst::cases, goto_convertt::targetst::cases_map, convert(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::op2(), exprt::operands(), messaget::mstreamt::source_location, targets, and to_code().
Referenced by convert().
|
protected |
Definition at line 1412 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_convertt::targetst::destructor_stack, goto_convertt::targetst::gotos, exprt::source_location(), and targets.
Referenced by convert(), and convert_non_deterministic_goto().
|
protected |
Definition at line 1686 of file goto_convert.cpp.
References exprt::add_source_location(), clean_expr(), code_ifthenelset::cond(), convert(), code_ifthenelset::else_case(), messaget::eom(), messaget::error(), exprt::find_source_location(), generate_ifthenelse(), irept::id(), irept::is_nil(), irept::is_not_nil(), needs_cleaning(), exprt::op0(), exprt::op1(), exprt::operands(), exprt::source_location(), messaget::mstreamt::source_location, code_ifthenelset::then_case(), and to_code().
Referenced by convert(), and convert_expression().
|
protected |
Definition at line 816 of file goto_convert.cpp.
References convert(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::operands(), codet::set_statement(), messaget::mstreamt::source_location, and to_code_assign().
Referenced by convert().
|
protected |
Definition at line 96 of file goto_convert_exceptions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_program_templatet< codeT, guardT >::destructive_append(), irept::find(), source_locationt::get_function(), irept::get_sub(), exprt::has_operands(), irept::is_not_nil(), exprt::op0(), exprt::operands(), and exprt::source_location().
Referenced by remove_push_catch().
|
protected |
Definition at line 333 of file goto_convert.cpp.
References exprt::add_source_location(), convert(), exprt::copy_to_operands(), goto_program_templatet< codeT, guardT >::destructive_append(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), code_labelt::get_label(), has_prefix(), id2string(), goto_program_templatet< codeT, guardT >::instructions, goto_convertt::targetst::labels, exprt::op0(), exprt::operands(), exprt::source_location(), messaget::mstreamt::source_location, targets, and to_code().
Referenced by convert().
|
protected |
Definition at line 936 of file goto_convert.cpp.
References clean_expr(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), goto_program_templatet< codeT, guardT >::instructions, irept::is_nil(), and messaget::mstreamt::source_location.
Referenced by convert_dowhile(), convert_for(), and convert_while().
|
protected |
Definition at line 70 of file goto_convert_exceptions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), convert(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), goto_convertt::targetst::leave_set, goto_convertt::targetst::leave_stack_size, goto_convertt::targetst::leave_target, exprt::source_location(), messaget::mstreamt::source_location, and targets.
Referenced by convert().
|
protected |
Definition at line 54 of file goto_convert_exceptions.cpp.
References convert(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::op0(), exprt::operands(), messaget::mstreamt::source_location, and to_code().
Referenced by convert().
|
protected |
Definition at line 16 of file goto_convert_exceptions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), goto_program_templatet< codeT, guardT >::instructions, exprt::op0(), exprt::op1(), exprt::operands(), goto_convertt::targetst::set_leave(), SKIP, exprt::source_location(), messaget::mstreamt::source_location, targets, and to_code().
Referenced by convert().
|
protected |
Definition at line 1438 of file goto_convert.cpp.
References convert_goto().
Referenced by convert().
|
protected |
Definition at line 1321 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), clean_expr(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), goto_convertt::targetst::has_return_value, code_returnt::has_return_value(), irept::id(), irept::make_nil(), exprt::operands(), goto_convertt::targetst::return_set, goto_convertt::targetst::return_target, code_returnt::return_value(), exprt::source_location(), messaget::mstreamt::source_location, targets, exprt::type(), and unwind_destructor_stack().
Referenced by convert().
|
protected |
Definition at line 914 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), SKIP, and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 1462 of file goto_convert.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), forall_operands, irept::get(), has_prefix(), irept::id(), id2string(), and messaget::mstreamt::source_location.
Referenced by convert_specc_notify(), and convert_specc_wait().
|
protected |
Definition at line 1445 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), convert_specc_event(), copy(), forall_operands, OTHER, and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 1516 of file goto_convert.cpp.
Referenced by convert().
|
protected |
Definition at line 1488 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), convert_specc_event(), copy(), messaget::eom(), messaget::error(), exprt::find_source_location(), irept::id(), exprt::op0(), exprt::operands(), OTHER, exprt::source_location(), and messaget::mstreamt::source_location.
Referenced by convert().
|
protected |
Definition at line 1523 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), END_THREAD, messaget::eom(), messaget::error(), exprt::find_source_location(), GOTO, goto_program_templatet< codeT, guardT >::instructions, exprt::op0(), exprt::operands(), SKIP, exprt::source_location(), messaget::mstreamt::source_location, START_THREAD, and to_code().
Referenced by convert().
|
protected |
Definition at line 1217 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), case_guard(), goto_convertt::targetst::cases, goto_convertt::targetst::cases_map, clean_expr(), convert(), goto_convertt::targetst::default_target, goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), forall_operands, exprt::operands(), goto_convertt::break_switch_targetst::restore(), goto_convertt::targetst::set_break(), goto_convertt::targetst::set_default(), exprt::source_location(), messaget::mstreamt::source_location, targets, to_code(), and code_switcht::value().
Referenced by convert().
|
protected |
Definition at line 375 of file goto_convert.cpp.
References code_switch_caset::case_op(), goto_convertt::targetst::cases, goto_convertt::targetst::cases_map, code_switch_caset::code(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), goto_program_templatet< codeT, guardT >::instructions, code_switch_caset::is_default(), exprt::operands(), goto_convertt::targetst::set_default(), messaget::mstreamt::source_location, and targets.
Referenced by convert().
|
protected |
Definition at line 151 of file goto_convert_exceptions.cpp.
References irept::add(), goto_program_templatet< codeT, guardT >::add_instruction(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), irept::get(), irept::get_sub(), goto_program_templatet< codeT, guardT >::instructions, exprt::op0(), exprt::operands(), exprt::source_location(), and to_code().
Referenced by convert().
|
protected |
Definition at line 1058 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), code_whilet::body(), boolean_negate(), code_whilet::cond(), convert(), convert_loop_invariant(), goto_program_templatet< codeT, guardT >::destructive_append(), generate_conditional_branch(), goto_program_templatet< codeT, guardT >::instructions, goto_convertt::break_continue_targetst::restore(), goto_convertt::targetst::set_break(), goto_convertt::targetst::set_continue(), exprt::source_location(), and targets.
Referenced by convert().
|
protected |
Definition at line 323 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), and exprt::source_location().
Referenced by convert(), convert_asm(), convert_assign(), convert_atomic_begin(), convert_atomic_end(), convert_decl(), convert_end_thread(), convert_expression(), convert_specc_notify(), convert_specc_par(), convert_specc_wait(), do_array_op(), do_function_call_symbol(), do_input(), do_output(), do_printf(), do_prob_coin(), do_prob_uniform(), do_scanf(), and make_compound_literal().
|
protected |
builds a goto program for object initialization after new
Definition at line 769 of file builtin_functions.cpp.
References convert(), exprt::copy_to_operands(), irept::find(), side_effect_exprt::get_statement(), irept::is_not_nil(), replace_new_object(), typet::subtype(), to_code(), and exprt::type().
Referenced by do_cpp_new().
|
protected |
Definition at line 855 of file builtin_functions.cpp.
References exprt::add_source_location(), convert(), messaget::eom(), messaget::error(), namespace_baset::follow(), irept::id(), irept::is_not_nil(), code_assignt::lhs(), ns, exprt::op0(), code_assignt::rhs(), messaget::mstreamt::source_location, typet::subtype(), and exprt::type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 833 of file builtin_functions.cpp.
References exprt::add_source_location(), copy(), messaget::eom(), messaget::error(), exprt::operands(), OTHER, codet::set_statement(), and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
|
protected |
Definition at line 374 of file builtin_functions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ATOMIC_BEGIN, messaget::eom(), messaget::error(), exprt::find_source_location(), irept::is_not_nil(), and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 398 of file builtin_functions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ATOMIC_END, messaget::eom(), messaget::error(), exprt::find_source_location(), irept::is_not_nil(), and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protectedvirtual |
Definition at line 422 of file builtin_functions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), ASSIGN, clean_expr(), convert(), cpp_new_initializer(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), code_function_callt::function(), irept::get(), irept::is_nil(), code_function_callt::lhs(), namespacet::lookup(), exprt::make_typecast(), new_tmp_symbol(), ns, object_size(), exprt::op0(), exprt::operands(), code_typet::parameters(), code_typet::return_type(), irept::set(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), to_code_type(), and exprt::type().
Referenced by convert_assign().
|
protected |
|
protectedvirtual |
Definition at line 35 of file goto_convert_function_call.cpp.
References clean_expr(), do_function_call_if(), do_function_call_other(), do_function_call_symbol(), messaget::eom(), messaget::error(), Forall_expr, symbol_exprt::get_identifier(), irept::is_nil(), messaget::mstreamt::source_location, to_if_expr(), and to_symbol_expr().
Referenced by convert_assign(), convert_function_call(), and do_function_call_if().
|
protectedvirtual |
Definition at line 91 of file goto_convert_function_call.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), goto_program_templatet< codeT, guardT >::destructive_append(), do_function_call(), goto_program_templatet< codeT, guardT >::instructions, and SKIP.
Referenced by do_function_call().
|
protectedvirtual |
Definition at line 155 of file goto_convert_function_call.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), code_function_callt::function(), FUNCTION_CALL, and code_function_callt::lhs().
Referenced by do_function_call().
|
protectedvirtual |
add function calls to function queue for later processing
Definition at line 929 of file builtin_functions.cpp.
References symbol_tablet::add(), goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), function_application_exprt::arguments(), as_string(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, symbolt::base_name, copy(), exprt::copy_to_operands(), CPROVER_PREFIX, do_array_equal(), do_array_op(), do_atomic_begin(), do_atomic_end(), do_input(), do_output(), do_printf(), do_prob_coin(), do_prob_uniform(), do_scanf(), double_type(), messaget::eom(), messaget::error(), exprt::find_source_location(), float_type(), namespace_baset::follow(), forall_expr, from_expr(), code_function_callt::function(), function_application_exprt::function(), FUNCTION_CALL, messaget::get_message_handler(), get_string_constant(), has_prefix(), symbol_tablet::has_symbol(), irept::id(), id2string(), is_lvalue(), irept::is_nil(), irept::is_not_nil(), code_function_callt::lhs(), symbolt::location, namespacet::lookup(), exprt::make_typecast(), make_va_list(), symbolt::name, ns, exprt::op0(), exprt::op1(), OTHER, code_typet::parameters(), pointer_type(), code_typet::remove_ellipsis(), irept::set(), symbol_exprt::set_identifier(), typet::source_location(), messaget::mstreamt::source_location, symbol_table, to_code_type(), symbolt::type, exprt::type(), and zero_initializer().
Referenced by do_function_call().
|
inlineprotectedvirtual |
Definition at line 189 of file goto_convert_class.h.
|
protected |
Definition at line 332 of file builtin_functions.cpp.
References exprt::add_source_location(), copy(), messaget::eom(), messaget::error(), exprt::operands(), OTHER, codet::set_statement(), and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 567 of file builtin_functions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSIGN, exprt::copy_to_operands(), messaget::eom(), messaget::error(), exprt::find_source_location(), messaget::get_message_handler(), irept::id(), irept::is_nil(), ns, object_size(), exprt::operands(), set_class_identifier(), size_of_expr(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), to_struct_expr(), to_symbol_type(), exprt::type(), and zero_initializer().
Referenced by convert_assign().
|
protected |
Definition at line 622 of file builtin_functions.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), ASSIGN, code_fort::body(), code_fort::cond(), convert(), exprt::copy_to_operands(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), namespace_baset::follow(), from_integer(), messaget::get_message_handler(), irept::id(), code_fort::init(), irept::is_nil(), code_fort::iter(), new_tmp_symbol(), ns, object_size(), exprt::op0(), exprt::op1(), exprt::operands(), OTHER, irept::set(), size_of_expr(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), symbolt::symbol_expr(), to_struct_type(), exprt::type(), and zero_initializer().
Referenced by convert_assign().
|
protected |
Definition at line 353 of file builtin_functions.cpp.
References exprt::add_source_location(), copy(), messaget::eom(), messaget::error(), exprt::operands(), OTHER, codet::set_statement(), and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 192 of file builtin_functions.cpp.
References exprt::add_source_location(), ASSIGN, copy(), CPROVER_PREFIX, irept::id(), irept::is_not_nil(), exprt::operands(), OTHER, to_code(), and exprt::type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 115 of file builtin_functions.cpp.
References exprt::add_source_location(), ASSIGN, copy(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), from_rational(), irept::is_nil(), messaget::mstreamt::source_location, to_integer(), and exprt::type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 37 of file builtin_functions.cpp.
References exprt::add_source_location(), ASSIGN, copy(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), irept::id(), irept::is_nil(), messaget::mstreamt::source_location, to_integer(), and exprt::type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 227 of file builtin_functions.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), ASSIGN, copy(), CPROVER_PREFIX, messaget::eom(), messaget::error(), from_integer(), code_function_callt::function(), FUNCTION_CALL, get_string_constant(), get_type(), irept::id(), id2string(), index_type(), irept::is_not_nil(), code_function_callt::lhs(), new_tmp_symbol(), exprt::op0(), exprt::op1(), exprt::operands(), OTHER, parse_format_string(), pointer_type(), codet::set_statement(), array_typet::size(), size_type(), messaget::mstreamt::source_location, typet::subtype(), symbolt::symbol_expr(), and to_array_type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 302 of file goto_convert_exceptions.cpp.
References symbolt::base_name, symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_thread_local, symbol_tablet::move(), symbolt::name, symbol_table, symbol_tablet::symbols, and symbolt::type.
Referenced by convert_CPROVER_throw(), and convert_CPROVER_try_catch().
|
protected |
Definition at line 235 of file goto_convert.cpp.
References goto_convertt::targetst::computed_gotos, irept::id(), goto_program_templatet< codeT, guardT >::insert_after(), goto_convertt::targetst::labels, binary_relation_exprt::lhs(), exprt::op0(), exprt::operands(), OTHER, binary_relation_exprt::rhs(), irept::set(), targets, and exprt::type().
Referenced by goto_convert_rec().
|
protected |
Definition at line 121 of file goto_convert.cpp.
References messaget::debug(), goto_program_templatet< codeT, guardT >::destructive_insert(), messaget::eom(), messaget::error(), irept::find(), forall_irep, irept::get_sub(), goto_convertt::targetst::gotos, goto_convertt::targetst::labels, messaget::mstreamt::source_location, targets, and unwind_destructor_stack().
Referenced by goto_convert_rec().
|
protected |
For each if(x) goto z; goto y; z: emitted, see if any destructor statements were inserted between goto z and z, and if not, simplify into if(!x) goto y;.
Definition at line 277 of file goto_convert.cpp.
References guarded_gotos.
Referenced by goto_convert_rec().
|
protected |
if(guard) goto target_true; else goto target_false;
Definition at line 1956 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), boolean_negate(), clean_expr(), collect_operands(), forall_expr_list, irept::id(), exprt::op0(), exprt::operands(), and exprt::source_location().
Referenced by convert_while(), generate_conditional_branch(), and generate_ifthenelse().
|
protected |
Definition at line 1917 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), clean_expr(), goto_program_templatet< codeT, guardT >::destructive_append(), generate_conditional_branch(), has_and_or(), needs_cleaning(), and exprt::source_location().
|
protected |
if(guard) true_case; else false_case;
Definition at line 1764 of file goto_convert.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), boolean_negate(), goto_program_templatet< codeT, guardT >::destructive_append(), generate_conditional_branch(), guarded_gotos, goto_program_templatet< codeT, guardT >::instructions, is_empty(), is_size_one(), and goto_program_templatet< codeT, guardT >::swap().
Referenced by clean_expr(), and convert_ifthenelse().
Definition at line 797 of file builtin_functions.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), irept::id(), ns, exprt::op0(), exprt::operands(), messaget::mstreamt::source_location, and exprt::type().
Definition at line 2090 of file goto_convert.cpp.
References irept::id(), namespacet::lookup(), ns, exprt::op0(), exprt::op1(), to_symbol_expr(), and symbolt::value.
Referenced by get_string_constant().
Definition at line 2074 of file goto_convert.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), irept::pretty(), messaget::result(), and messaget::mstreamt::source_location.
Referenced by convert(), do_function_call_symbol(), do_scanf(), and get_string_constant().
Definition at line 2033 of file goto_convert.cpp.
References binary2integer(), forall_operands, irept::get(), get_constant(), get_string_constant(), constant_exprt::get_value(), irept::id(), id2string(), integer2ulong(), ns, exprt::op0(), exprt::operands(), messaget::result(), simplify(), and to_constant_expr().
void goto_convertt::goto_convert | ( | const codet & | code, |
goto_programt & | dest | ||
) |
Definition at line 306 of file goto_convert.cpp.
References goto_convert_rec().
|
protected |
Definition at line 311 of file goto_convert.cpp.
References convert(), finish_catch_push_targets(), finish_computed_gotos(), finish_gotos(), and finish_guarded_gotos().
Referenced by goto_convert_functionst::convert_function(), and goto_convert().
|
staticprotected |
Definition at line 23 of file goto_convert_side_effect.cpp.
References forall_operands, irept::get(), and irept::id().
|
staticprotected |
Definition at line 2168 of file goto_convert.cpp.
References messaget::eom(), messaget::error(), namespacet::lookup(), and ns.
Referenced by convert_decl(), and remove_function_call().
|
protected |
Definition at line 22 of file goto_clean_expr.cpp.
References exprt::add_source_location(), convert(), copy(), DECL, goto_convertt::targetst::destructor_stack, exprt::find_source_location(), get_fresh_aux_symbol(), symbolt::is_static_lifetime, messaget::result(), symbolt::symbol_expr(), symbol_table, targets, tmp_symbol_prefix, exprt::type(), and symbolt::value.
Referenced by clean_expr_address_of().
|
protected |
Definition at line 2139 of file goto_convert.cpp.
References exprt::add_source_location(), convert(), exprt::find_source_location(), code_assignt::lhs(), new_tmp_symbol(), symbolt::symbol_expr(), and exprt::type().
Referenced by remove_post().
|
staticprotected |
Definition at line 63 of file goto_clean_expr.cpp.
References index_exprt::array(), forall_operands, irept::id(), index_exprt::index(), exprt::is_zero(), and to_index_expr().
Referenced by clean_expr(), convert_ifthenelse(), and generate_conditional_branch().
|
protected |
Definition at line 2159 of file goto_convert.cpp.
References symbol_tablet::add(), get_new_name(), ns, and symbol_table.
Referenced by remove_cpp_new(), remove_function_call(), and remove_malloc().
|
protected |
Definition at line 2116 of file goto_convert.cpp.
References exprt::add_source_location(), convert_decl(), get_fresh_aux_symbol(), code_declt::symbol(), symbolt::symbol_expr(), symbol_table, and tmp_symbol_prefix.
Referenced by clean_expr(), do_cpp_new(), do_java_new_array(), do_scanf(), make_temp_symbol(), remove_statement_expression(), and remove_temporary_object().
|
protected |
Definition at line 36 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), convert_assign(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), side_effect_exprt::get_statement(), irept::id(), is_not_zero(), irept::make_nil(), exprt::make_typecast(), ns, exprt::op0(), exprt::op1(), exprt::operands(), exprt::source_location(), messaget::mstreamt::source_location, irept::swap(), to_code(), to_code_assign(), and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 453 of file goto_convert_side_effect.cpp.
References convert_cpp_delete(), irept::find(), side_effect_exprt::get_statement(), irept::make_nil(), exprt::op0(), exprt::operands(), irept::set(), codet::set_statement(), and exprt::source_location().
Referenced by remove_side_effect().
|
protected |
Definition at line 423 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), symbolt::base_name, convert(), convert_decl(), id2string(), symbolt::location, irept::make_nil(), symbolt::name, new_name(), code_declt::symbol(), symbolt::symbol_expr(), temporary_counter, tmp_symbol_prefix, symbolt::type, and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 332 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), symbolt::base_name, convert_decl(), convert_function_call(), messaget::eom(), messaget::error(), exprt::find_source_location(), code_function_callt::function(), irept::get(), irept::id(), id2string(), code_function_callt::lhs(), symbolt::location, lookup(), irept::make_nil(), symbolt::mode, symbolt::name, new_name(), exprt::op0(), exprt::op1(), exprt::operands(), exprt::source_location(), messaget::mstreamt::source_location, code_declt::symbol(), symbolt::symbol_expr(), temporary_counter, tmp_symbol_prefix, symbolt::type, and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 503 of file goto_clean_expr.cpp.
References typet::add_source_location(), clean_expr(), if_exprt::cond(), messaget::eom(), messaget::error(), exprt::find_source_location(), exprt::op0(), exprt::op1(), exprt::operands(), exprt::source_location(), messaget::mstreamt::source_location, irept::swap(), and exprt::type().
Referenced by clean_expr().
|
protected |
Definition at line 472 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), symbolt::base_name, convert(), convert_decl(), id2string(), symbolt::location, exprt::move_to_operands(), symbolt::name, new_name(), exprt::source_location(), code_declt::symbol(), symbolt::symbol_expr(), temporary_counter, tmp_symbol_prefix, symbolt::type, and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 226 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), exprt::copy_to_operands(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), from_integer(), side_effect_exprt::get_statement(), irept::id(), index_type(), is_not_zero(), is_number(), irept::make_nil(), make_temp_symbol(), exprt::make_typecast(), exprt::move_to_operands(), ns, exprt::op0(), exprt::operands(), irept::pretty(), signed_int_type(), exprt::source_location(), messaget::mstreamt::source_location, typet::subtype(), irept::swap(), to_complex_type(), and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 139 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), exprt::find_source_location(), namespace_baset::follow(), from_integer(), side_effect_exprt::get_statement(), irept::id(), index_type(), is_not_zero(), is_number(), irept::make_nil(), exprt::make_typecast(), exprt::move_to_operands(), ns, exprt::op0(), exprt::operands(), irept::pretty(), signed_int_type(), exprt::source_location(), messaget::mstreamt::source_location, irept::swap(), and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 639 of file goto_convert_side_effect.cpp.
References convert_java_try_catch(), and irept::make_nil().
Referenced by remove_side_effect().
|
protected |
Definition at line 650 of file goto_convert_side_effect.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), side_effect_exprt::get_statement(), irept::make_nil(), exprt::operands(), remove_assignment(), remove_cpp_delete(), remove_cpp_new(), remove_function_call(), remove_malloc(), remove_post(), remove_pre(), remove_push_catch(), remove_statement_expression(), remove_temporary_object(), exprt::source_location(), messaget::mstreamt::source_location, and THROW.
Referenced by clean_expr().
|
protected |
Definition at line 549 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), goto_program_templatet< codeT, guardT >::destructive_append(), messaget::eom(), messaget::error(), code_expressiont::expression(), code_blockt::find_last_statement(), exprt::find_source_location(), irept::get(), codet::get_statement(), irept::id(), code_assignt::lhs(), irept::make_nil(), symbolt::name, new_tmp_symbol(), exprt::op0(), exprt::operands(), messaget::mstreamt::source_location, to_code(), to_code_assign(), to_code_block(), to_code_expression(), symbolt::type, and exprt::type().
Referenced by clean_expr(), and remove_side_effect().
|
protected |
Definition at line 509 of file goto_convert_side_effect.cpp.
References convert(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), irept::get(), irept::is_not_nil(), symbolt::mode, exprt::move_to_operands(), new_tmp_symbol(), exprt::op0(), exprt::operands(), replace_new_object(), exprt::reserve_operands(), messaget::mstreamt::source_location, symbolt::symbol_expr(), to_code(), and exprt::type().
Referenced by remove_side_effect().
Definition at line 412 of file goto_convert_side_effect.cpp.
References Forall_operands, and irept::id().
Referenced by convert_cpp_delete(), cpp_new_initializer(), and remove_temporary_object().
|
protected |
re-write boolean operators into ?:
Definition at line 108 of file goto_clean_expr.cpp.
References messaget::eom(), messaget::error(), exprt::find_source_location(), irept::id(), exprt::is_boolean(), exprt::operands(), irept::pretty(), messaget::mstreamt::source_location, and irept::swap().
Referenced by clean_expr().
|
protected |
Definition at line 324 of file goto_convert_exceptions.cpp.
References goto_convertt::targetst::destructor_stack, and targets.
Referenced by convert_block(), convert_break(), convert_continue(), convert_CPROVER_throw(), convert_return(), and finish_gotos().
|
protected |
Definition at line 336 of file goto_convert_exceptions.cpp.
References exprt::add_source_location(), and convert().
|
protected |
Definition at line 475 of file goto_convert_class.h.
Referenced by finish_guarded_gotos(), and generate_ifthenelse().
|
protected |
Definition at line 48 of file goto_convert_class.h.
Referenced by clean_expr(), convert(), convert_cpp_delete(), convert_decl(), goto_convert_functionst::convert_function(), do_array_equal(), do_cpp_new(), do_function_call_symbol(), do_java_new(), do_java_new_array(), get_array_argument(), get_constant(), get_string_constant(), lookup(), new_name(), remove_assignment(), remove_post(), and remove_pre().
|
protected |
Definition at line 47 of file goto_convert_class.h.
Referenced by do_function_call_symbol(), exception_flag(), goto_convert_functionst::goto_convert(), make_compound_literal(), new_name(), and new_tmp_symbol().
|
protected |
Referenced by goto_convertt::break_continue_targetst::break_continue_targetst(), goto_convertt::break_switch_targetst::break_switch_targetst(), convert_block(), convert_break(), convert_continue(), convert_CPROVER_throw(), convert_CPROVER_try_catch(), convert_CPROVER_try_finally(), convert_decl(), convert_dowhile(), convert_for(), goto_convert_functionst::convert_function(), convert_gcc_computed_goto(), convert_gcc_switch_case_range(), convert_goto(), convert_label(), convert_msc_leave(), convert_msc_try_finally(), convert_return(), convert_switch(), convert_switch_case(), convert_while(), finish_computed_gotos(), finish_gotos(), goto_convertt::leave_targett::leave_targett(), make_compound_literal(), goto_convertt::break_continue_targetst::restore(), goto_convertt::break_switch_targetst::restore(), goto_convertt::throw_targett::restore(), goto_convertt::leave_targett::restore(), goto_convertt::throw_targett::throw_targett(), and unwind_destructor_stack().
|
protected |
Definition at line 49 of file goto_convert_class.h.
Referenced by goto_convert_functionst::convert_function(), remove_cpp_new(), remove_function_call(), and remove_malloc().
|
protected |
Definition at line 50 of file goto_convert_class.h.
Referenced by goto_convert_functionst::convert_function(), make_compound_literal(), new_tmp_symbol(), remove_cpp_new(), remove_function_call(), and remove_malloc().