cprover
|
#include <goto_convert_class.h>
Classes | |
struct | break_continue_targetst |
struct | break_switch_targetst |
struct | leave_targett |
struct | targetst |
struct | throw_targett |
Public Member Functions | |
void | goto_convert (const codet &code, goto_programt &dest, const irep_idt &mode) |
goto_convertt (symbol_table_baset &_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 |
Protected Member Functions | |
void | goto_convert_rec (const codet &code, goto_programt &dest, const irep_idt &mode) |
symbolt & | new_tmp_symbol (const typet &type, const std::string &suffix, goto_programt &dest, const source_locationt &, const irep_idt &mode) |
symbol_exprt | make_compound_literal (const exprt &expr, goto_programt &dest, const irep_idt &mode) |
void | clean_expr (exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used=true) |
void | clean_expr_address_of (exprt &expr, goto_programt &dest, const irep_idt &mode) |
void | make_temp_symbol (exprt &expr, const std::string &suffix, goto_programt &, const irep_idt &mode) |
void | rewrite_boolean (exprt &dest) |
re-write boolean operators into ?: More... | |
void | remove_side_effect (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_assignment (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode) |
void | remove_pre (side_effect_exprt &expr, goto_programt &dest, bool result_is_used, const irep_idt &mode) |
void | remove_post (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_function_call (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_cpp_new (side_effect_exprt &expr, goto_programt &dest, bool result_is_used) |
void | remove_cpp_delete (side_effect_exprt &expr, goto_programt &dest) |
void | remove_malloc (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_temporary_object (side_effect_exprt &expr, goto_programt &dest) |
void | remove_statement_expression (side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, bool result_is_used) |
void | remove_gcc_conditional_expression (exprt &expr, goto_programt &dest, const irep_idt &mode) |
virtual void | do_cpp_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
void | do_java_new (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
void | do_java_new_array (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
void | cpp_new_initializer (const exprt &lhs, const side_effect_exprt &rhs, goto_programt &dest) |
builds a goto program for object initialization after new More... | |
virtual void | do_function_call (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode) |
virtual void | do_function_call_if (const exprt &lhs, const if_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode) |
virtual void | do_function_call_symbol (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
add function calls to function queue for later processing More... | |
virtual void | do_function_call_symbol (const symbolt &) |
virtual void | do_function_call_other (const exprt &lhs, const exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | convert_block (const code_blockt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_decl (const code_declt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_decl_type (const codet &code, goto_programt &dest) |
void | convert_expression (const code_expressiont &code, goto_programt &dest, const irep_idt &mode) |
void | convert_assign (const code_assignt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_cpp_delete (const codet &code, goto_programt &dest) |
void | convert_loop_invariant (const codet &code, goto_programt::targett loop, const irep_idt &mode) |
void | convert_for (const code_fort &code, goto_programt &dest, const irep_idt &mode) |
void | convert_while (const code_whilet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_dowhile (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_assume (const code_assumet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_assert (const code_assertt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_switch (const code_switcht &code, goto_programt &dest, const irep_idt &mode) |
void | convert_break (const code_breakt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_return (const code_returnt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_continue (const code_continuet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_ifthenelse (const code_ifthenelset &code, goto_programt &dest, const irep_idt &mode) |
void | convert_init (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_goto (const code_gotot &code, goto_programt &dest) |
void | convert_gcc_computed_goto (const codet &code, goto_programt &dest) |
void | convert_skip (const codet &code, goto_programt &dest) |
void | convert_label (const code_labelt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_gcc_local_label (const codet &code, goto_programt &dest) |
void | convert_switch_case (const code_switch_caset &code, goto_programt &dest, const irep_idt &mode) |
void | convert_gcc_switch_case_range (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_function_call (const code_function_callt &code, goto_programt &dest, const irep_idt &mode) |
void | convert_start_thread (const codet &code, goto_programt &dest) |
void | convert_end_thread (const codet &code, goto_programt &dest) |
void | convert_atomic_begin (const codet &code, goto_programt &dest) |
void | convert_atomic_end (const codet &code, goto_programt &dest) |
void | convert_msc_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_msc_try_except (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_msc_leave (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_CPROVER_try_catch (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_CPROVER_try_finally (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_CPROVER_throw (const codet &code, goto_programt &dest, const irep_idt &mode) |
void | convert_asm (const code_asmt &code, goto_programt &dest) |
void | convert (const codet &code, goto_programt &dest, const irep_idt &mode) |
converts 'code' and appends the result to 'dest' More... | |
void | copy (const codet &code, goto_program_instruction_typet type, goto_programt &dest) |
symbol_exprt | exception_flag () |
void | unwind_destructor_stack (const source_locationt &, std::size_t stack_size, goto_programt &dest, const irep_idt &mode) |
void | unwind_destructor_stack (const source_locationt &, std::size_t stack_size, goto_programt &dest, destructor_stackt &stack, const irep_idt &mode) |
void | finish_gotos (goto_programt &dest, const irep_idt &mode) |
void | finish_computed_gotos (goto_programt &dest) |
void | optimize_guarded_gotos (goto_programt &dest) |
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target. More... | |
exprt | case_guard (const exprt &value, const caset &case_op) |
void | generate_ifthenelse (const exprt &cond, goto_programt &true_case, goto_programt &false_case, const source_locationt &, goto_programt &dest, const irep_idt &mode) |
if(guard) true_case; else false_case; More... | |
void | generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, goto_programt::targett target_false, const source_locationt &, goto_programt &dest, const irep_idt &mode) |
if(guard) goto target_true; else goto target_false; More... | |
void | generate_conditional_branch (const exprt &guard, goto_programt::targett target_true, const source_locationt &, goto_programt &dest, const irep_idt &mode) |
void | generate_thread_block (const code_blockt &thread_body, goto_programt &dest, const irep_idt &mode) |
Generates the necessary goto-instructions to represent a thread-block. More... | |
irep_idt | get_string_constant (const exprt &expr) |
bool | get_string_constant (const exprt &expr, irep_idt &) |
exprt | get_constant (const exprt &expr) |
void | do_atomic_begin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_atomic_end (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_create_thread (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_array_equal (const exprt &lhs, const symbol_exprt &rhs, const exprt::operandst &arguments, goto_programt &dest) |
void | do_array_op (const irep_idt &id, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_printf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_scanf (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_input (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest) |
void | do_output (const exprt &rhs, const exprt::operandst &arguments, goto_programt &dest) |
void | do_prob_coin (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
void | do_prob_uniform (const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest) |
exprt | get_array_argument (const exprt &src) |
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_table_baset & | symbol_table |
namespacet | ns |
std::string | tmp_symbol_prefix |
struct goto_convertt::targetst | targets |
Additional Inherited Members |
Definition at line 26 of file goto_convert_class.h.
|
protected |
Definition at line 365 of file goto_convert_class.h.
|
protected |
Definition at line 364 of file goto_convert_class.h.
|
protected |
Definition at line 363 of file goto_convert_class.h.
|
protected |
Definition at line 362 of file goto_convert_class.h.
|
protected |
Definition at line 334 of file goto_convert_class.h.
|
protected |
Definition at line 361 of file goto_convert_class.h.
|
protected |
Definition at line 359 of file goto_convert_class.h.
|
inline |
Definition at line 32 of file goto_convert_class.h.
|
inlinevirtual |
Definition at line 42 of file goto_convert_class.h.
Definition at line 1206 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 162 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_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 445 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 1587 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 444 of file goto_convert.cpp.
References goto_programt::add_instruction(), CATCH, convert_asm(), convert_assert(), convert_assign(), convert_assume(), convert_atomic_begin(), convert_atomic_end(), convert_block(), 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_return(), convert_skip(), 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_programt::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_goto(), 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_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_switch(), convert_switch_case(), convert_try_catch(), convert_while(), cpp_new_initializer(), do_cpp_new(), generate_thread_block(), 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 909 of file goto_convert.cpp.
References goto_programt::add_instruction(), ASSERT, code_assertt::assertion(), clean_expr(), irept::set(), and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 721 of file goto_convert.cpp.
References ASSIGN, clean_expr(), copy(), DATA_INVARIANT, do_cpp_new(), do_function_call(), 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 934 of file goto_convert.cpp.
References goto_programt::add_instruction(), ASSUME, code_assumet::assumption(), clean_expr(), and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 1506 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 1520 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 570 of file goto_convert.cpp.
References convert(), goto_convertt::targetst::destructor_stack, goto_programt::empty(), code_blockt::end_location(), forall_operands, goto_programt::instructions, targets, to_code(), and unwind_destructor_stack().
Referenced by convert().
|
protected |
Definition at line 1339 of file goto_convert.cpp.
References goto_programt::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 1432 of file goto_convert.cpp.
References goto_programt::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 845 of file goto_convert.cpp.
References exprt::add_source_location(), code_function_callt::arguments(), clean_expr(), convert(), 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, to_code(), to_code_type(), exprt::type(), and UNREACHABLE.
Referenced by convert(), and remove_cpp_delete().
|
protected |
Definition at line 195 of file goto_convert_exceptions.cpp.
References goto_programt::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 157 of file goto_convert_exceptions.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), code_ifthenelset::cond(), convert(), goto_programt::destructive_append(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exception_flag(), exprt::find_source_location(), goto_programt::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 233 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 646 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(), get_destructor(), symbol_exprt::get_identifier(), irept::id(), irept::is_not_nil(), symbolt::is_static_lifetime, namespacet::lookup(), symbolt::name, ns, exprt::op0(), exprt::op1(), exprt::operands(), pointer_type(), exprt::source_location(), messaget::mstreamt::source_location, code_declt::symbol(), targets, to_symbol_expr(), and symbolt::type.
Referenced by convert(), new_tmp_symbol(), remove_cpp_new(), remove_function_call(), and remove_malloc().
|
protected |
Definition at line 714 of file goto_convert.cpp.
Referenced by convert().
|
protected |
Definition at line 1133 of file goto_convert.cpp.
References goto_programt::add_instruction(), clean_expr(), convert(), convert_loop_invariant(), goto_programt::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), goto_programt::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 1492 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 602 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 972 of file goto_convert.cpp.
References goto_programt::add_instruction(), code_fort::body(), clean_expr(), code_fort::cond(), convert(), convert_loop_invariant(), goto_programt::destructive_append(), code_fort::init(), goto_programt::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 1465 of file goto_convert.cpp.
References goto_programt::add_instruction(), goto_convertt::targetst::computed_gotos, NO_INSTRUCTION_TYPE, exprt::source_location(), and targets.
Referenced by convert().
|
protected |
Definition at line 354 of file goto_convert.cpp.
Referenced by convert().
|
protected |
Definition at line 393 of file goto_convert.cpp.
References goto_convertt::targetst::cases, goto_convertt::targetst::cases_map, convert(), goto_programt::destructive_append(), messaget::eom(), messaget::error(), exprt::find_source_location(), from_integer(), goto_programt::instructions, numeric_cast(), exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), messaget::mstreamt::source_location, targets, to_code(), exprt::type(), and messaget::warning().
Referenced by convert().
|
protected |
Definition at line 1454 of file goto_convert.cpp.
References goto_programt::add_instruction(), goto_convertt::targetst::destructor_stack, goto_convertt::targetst::gotos, exprt::source_location(), and targets.
Referenced by convert().
|
protected |
Definition at line 1534 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, and code_ifthenelset::then_case().
Referenced by convert(), and convert_expression().
|
protected |
Definition at line 826 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 308 of file goto_convert.cpp.
References code_blockt::add(), convert(), goto_programt::destructive_append(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), generate_thread_block(), code_labelt::get_label(), has_prefix(), id2string(), goto_programt::instructions, INVARIANT, irept::is_not_nil(), 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 948 of file goto_convert.cpp.
References clean_expr(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), goto_programt::instructions, irept::is_nil(), and messaget::mstreamt::source_location.
Referenced by convert_dowhile(), convert_for(), and convert_while().
|
protected |
Definition at line 72 of file goto_convert_exceptions.cpp.
References goto_programt::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 55 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_programt::add_instruction(), convert(), goto_programt::destructive_append(), goto_convertt::targetst::destructor_stack, messaget::eom(), messaget::error(), exprt::find_source_location(), goto_programt::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 1361 of file goto_convert.cpp.
References goto_programt::add_instruction(), clean_expr(), goto_programt::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 925 of file goto_convert.cpp.
References goto_programt::add_instruction(), SKIP, and exprt::source_location().
Referenced by convert().
|
protected |
Definition at line 1478 of file goto_convert.cpp.
References goto_programt::add_instruction(), goto_convertt::targetst::destructor_stack, goto_convertt::targetst::gotos, exprt::source_location(), START_THREAD, and targets.
Referenced by convert().
|
protected |
Definition at line 1233 of file goto_convert.cpp.
References goto_programt::add_instruction(), code_switcht::body(), case_guard(), goto_convertt::targetst::cases, goto_convertt::targetst::cases_map, clean_expr(), convert(), goto_convertt::targetst::default_target, goto_programt::destructive_append(), codet::get_statement(), goto_convertt::break_switch_targetst::restore(), goto_convertt::targetst::set_break(), source_locationt::set_case_number(), goto_convertt::targetst::set_default(), exprt::source_location(), irept::swap(), targets, to_code_block(), to_string(), and code_switcht::value().
Referenced by convert().
|
protected |
Definition at line 361 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_programt::destructive_append(), goto_programt::instructions, code_switch_caset::is_default(), goto_convertt::targetst::set_default(), and targets.
Referenced by convert().
|
protected |
Definition at line 99 of file goto_convert_exceptions.cpp.
References goto_programt::add_instruction(), convert(), goto_programt::destructive_append(), code_push_catcht::exception_list(), irept::get(), goto_programt::instructions, exprt::op0(), exprt::operands(), exprt::source_location(), and to_code().
Referenced by convert().
|
protected |
Definition at line 1072 of file goto_convert.cpp.
References goto_programt::add_instruction(), code_whilet::body(), boolean_negate(), code_whilet::cond(), convert(), convert_loop_invariant(), goto_programt::destructive_append(), generate_conditional_branch(), goto_programt::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 298 of file goto_convert.cpp.
References goto_programt::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(), 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 532 of file builtin_functions.cpp.
References convert(), irept::find(), side_effect_exprt::get_statement(), irept::is_not_nil(), replace_new_object(), typet::subtype(), to_code(), exprt::type(), and UNREACHABLE.
Referenced by do_cpp_new().
|
protected |
|
protected |
Definition at line 595 of file builtin_functions.cpp.
References exprt::add_source_location(), copy(), exprt::copy_to_operands(), messaget::eom(), messaget::error(), exprt::operands(), OTHER, and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 363 of file builtin_functions.cpp.
References goto_programt::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 387 of file builtin_functions.cpp.
References goto_programt::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 411 of file builtin_functions.cpp.
References goto_programt::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), ASSIGN, clean_expr(), convert(), cpp_new_initializer(), goto_programt::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 37 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 95 of file goto_convert_function_call.cpp.
References goto_programt::add_instruction(), goto_programt::destructive_append(), do_function_call(), goto_programt::instructions, and SKIP.
Referenced by do_function_call().
|
protectedvirtual |
Definition at line 160 of file goto_convert_function_call.cpp.
References goto_programt::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 637 of file builtin_functions.cpp.
References symbol_table_baset::add(), goto_programt::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), function_application_exprt::arguments(), ASSERT, ASSIGN, ASSUME, ATOMIC_BEGIN, ATOMIC_END, symbolt::base_name, copy(), exprt::copy_to_operands(), CPROVER_PREFIX, 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_table_baset::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 196 of file goto_convert_class.h.
|
protected |
Definition at line 325 of file builtin_functions.cpp.
References exprt::add_source_location(), copy(), messaget::eom(), messaget::error(), exprt::operands(), OTHER, and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
|
protected |
|
protected |
Definition at line 344 of file builtin_functions.cpp.
References exprt::add_source_location(), copy(), messaget::eom(), messaget::error(), exprt::operands(), OTHER, and messaget::mstreamt::source_location.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 184 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(), exprt::type(), and UNREACHABLE.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 108 of file builtin_functions.cpp.
References exprt::add_source_location(), ASSIGN, copy(), messaget::eom(), messaget::error(), from_rational(), irept::is_nil(), typet::source_location(), messaget::mstreamt::source_location, to_integer(), and exprt::type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 30 of file builtin_functions.cpp.
References exprt::add_source_location(), ASSIGN, copy(), messaget::eom(), messaget::error(), irept::id(), irept::is_nil(), typet::source_location(), messaget::mstreamt::source_location, to_integer(), and exprt::type().
Referenced by do_function_call_symbol().
|
protected |
Definition at line 220 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(), typet::source_location(), messaget::mstreamt::source_location, typet::subtype(), symbolt::symbol_expr(), to_array_type(), and UNREACHABLE.
Referenced by do_function_call_symbol().
|
protected |
Definition at line 258 of file goto_convert_exceptions.cpp.
References symbolt::base_name, symbol_table_baset::insert(), symbolt::is_file_local, symbolt::is_lvalue, symbolt::is_thread_local, symbolt::name, symbol_table, symbol_table_baset::symbols, and symbolt::type.
Referenced by convert_CPROVER_throw(), and convert_CPROVER_try_catch().
|
protected |
Definition at line 196 of file goto_convert.cpp.
References goto_programt::instructiont::code, goto_convertt::targetst::computed_gotos, goto_program, irept::id(), goto_programt::insert_after(), goto_convertt::targetst::labels, exprt::op0(), exprt::operands(), OTHER, irept::set(), goto_programt::instructiont::source_location, targets, and goto_programt::instructiont::type.
Referenced by goto_convert_rec().
|
protected |
Definition at line 106 of file goto_convert.cpp.
References exprt::add_source_location(), goto_programt::instructiont::code, goto_programt::instructiont::complete_goto(), messaget::debug(), goto_programt::destructive_insert(), messaget::eom(), messaget::error(), exprt::find_source_location(), irept::get(), codet::get_statement(), goto_convertt::targetst::gotos, goto_programt::instructiont::is_start_thread(), goto_convertt::targetst::labels, messaget::mstreamt::source_location, goto_programt::instructiont::targets, targets, and unwind_destructor_stack().
Referenced by goto_convert_rec().
|
protected |
if(guard) goto target_true; else goto target_false;
Definition at line 1814 of file goto_convert.cpp.
References goto_programt::add_instruction(), boolean_negate(), clean_expr(), collect_operands(), irept::id(), exprt::op0(), exprt::operands(), and exprt::source_location().
Referenced by convert_while(), generate_conditional_branch(), and generate_ifthenelse().
|
protected |
Definition at line 1774 of file goto_convert.cpp.
References goto_programt::add_instruction(), clean_expr(), goto_programt::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 1614 of file goto_convert.cpp.
References goto_programt::add_instruction(), boolean_negate(), goto_programt::destructive_append(), generate_conditional_branch(), goto_programt::instructions, is_empty(), is_size_one(), is_skip(), and goto_programt::swap().
Referenced by clean_expr(), and convert_ifthenelse().
|
protected |
Generates the necessary goto-instructions to represent a thread-block.
Specifically, the following instructions are generated:
A: START_THREAD : C B: GOTO Z C: SKIP D: {THREAD BODY} E: END_THREAD Z: SKIP
thread_body | sequence of codet's that can be executed in parallel. | |
[out] | dest | resulting goto-instructions. |
Definition at line 2086 of file goto_convert.cpp.
References goto_programt::add_instruction(), convert(), goto_programt::destructive_append(), END_THREAD, exprt::source_location(), and START_THREAD.
Referenced by convert_label().
Definition at line 559 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 1949 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 1933 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 1892 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, | ||
const irep_idt & | mode | ||
) |
Definition at line 277 of file goto_convert.cpp.
References goto_convert_rec().
|
protected |
Definition at line 285 of file goto_convert.cpp.
References convert(), finish_catch_push_targets(), finish_computed_gotos(), finish_gotos(), and optimize_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 |
|
protected |
Definition at line 21 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 1998 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 62 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 1975 of file goto_convert.cpp.
References exprt::add_source_location(), convert_decl(), dstringt::empty(), get_fresh_aux_symbol(), PRECONDITION, symbol_table, and tmp_symbol_prefix.
Referenced by clean_expr(), do_cpp_new(), do_scanf(), make_temp_symbol(), remove_statement_expression(), and remove_temporary_object().
|
protected |
Rewrite "if(x) goto z; goto y; z:" into "if(!x) goto y;" This only works if the "goto y" is not a branch target.
Definition at line 235 of file goto_convert.cpp.
References boolean_negate(), goto_programt::instructions, and goto_programt::instructiont::nil_target.
Referenced by goto_convert_rec().
|
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(), exprt::type(), and UNREACHABLE.
Referenced by remove_side_effect().
|
protected |
Definition at line 449 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert_cpp_delete(), irept::find(), side_effect_exprt::get_statement(), irept::make_nil(), exprt::op0(), exprt::operands(), irept::set(), and exprt::source_location().
Referenced by remove_side_effect().
|
protected |
Definition at line 422 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), convert_decl(), exprt::find_source_location(), get_fresh_aux_symbol(), symbolt::location, irept::make_nil(), symbolt::symbol_expr(), symbol_table, tmp_symbol_prefix, and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 335 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(), get_fresh_aux_symbol(), irept::id(), id2string(), code_function_callt::lhs(), symbolt::location, namespacet::lookup(), irept::make_nil(), symbolt::mode, ns, exprt::op0(), exprt::op1(), exprt::operands(), exprt::source_location(), messaget::mstreamt::source_location, symbolt::symbol_expr(), symbol_table, tmp_symbol_prefix, to_symbol_expr(), and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 509 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 465 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), convert_decl(), get_fresh_aux_symbol(), symbolt::location, exprt::move_to_operands(), exprt::source_location(), symbolt::symbol_expr(), symbol_table, tmp_symbol_prefix, and exprt::type().
Referenced by remove_side_effect().
|
protected |
Definition at line 228 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), exprt::copy_to_operands(), goto_programt::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 140 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 627 of file goto_convert_side_effect.cpp.
References goto_programt::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_statement_expression(), remove_temporary_object(), exprt::source_location(), messaget::mstreamt::source_location, THROW, and exprt::type().
Referenced by clean_expr().
|
protected |
Definition at line 536 of file goto_convert_side_effect.cpp.
References exprt::add_source_location(), convert(), goto_programt::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 501 of file goto_convert_side_effect.cpp.
References convert(), messaget::eom(), messaget::error(), irept::find(), exprt::find_source_location(), irept::get(), irept::is_not_nil(), new_tmp_symbol(), exprt::op0(), exprt::operands(), replace_new_object(), messaget::mstreamt::source_location, symbolt::symbol_expr(), to_code(), and exprt::type().
Referenced by remove_side_effect().
Definition at line 411 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 107 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 280 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 290 of file goto_convert_exceptions.cpp.
References exprt::add_source_location(), and convert().
|
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_cpp_new(), do_function_call_symbol(), get_array_argument(), get_constant(), get_string_constant(), remove_assignment(), remove_function_call(), 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_tmp_symbol(), remove_cpp_new(), remove_function_call(), and remove_malloc().
|
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_start_thread(), 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(), make_compound_literal(), new_tmp_symbol(), remove_cpp_new(), remove_function_call(), and remove_malloc().