cprover
goto_convert_new_switch_case.cpp File Reference

Program Transformation. More...

#include "goto_convert_class.h"
#include <cassert>
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <util/simplify_expr.h>
#include <util/rename.h>
#include <util/c_types.h>
#include "goto_convert.h"
#include "destructor.h"
Include dependency graph for goto_convert_new_switch_case.cpp:

Go to the source code of this file.

Functions

static bool is_empty (const goto_programt &goto_program)
 
static bool has_and_or (const exprt &expr)
 if(guard) goto target; More...
 
void goto_convert (const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
 
void goto_convert (symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
 

Detailed Description

Program Transformation.

Definition in file goto_convert_new_switch_case.cpp.

Function Documentation

§ goto_convert() [1/2]

void goto_convert ( const codet code,
symbol_tablet symbol_table,
goto_programt dest,
message_handlert message_handler 
)

§ goto_convert() [2/2]

void goto_convert ( symbol_tablet symbol_table,
goto_programt dest,
message_handlert message_handler 
)

§ has_and_or()

§ is_empty()

static bool is_empty ( const goto_programt goto_program)
static

Definition at line 28 of file goto_convert_new_switch_case.cpp.

References goto_program_templatet< codeT, guardT >::add_instruction(), exprt::add_source_location(), code_function_callt::arguments(), ASSERT, code_assertt::assertion(), ASSIGN, ASSUME, code_assumet::assumption(), ATOMIC_BEGIN, ATOMIC_END, code_whilet::body(), code_fort::body(), boolean_negate(), goto_convertt::targetst::break_set, goto_convertt::targetst::break_stack_size, goto_convertt::targetst::break_target, goto_convertt::case_guard(), code_switch_caset::case_op(), goto_convertt::targetst::cases, goto_convertt::targetst::cases_map, goto_convertt::clean_expr(), code_switch_caset::code(), goto_convertt::collect_operands(), goto_convertt::targetst::computed_gotos, code_ifthenelset::cond(), code_whilet::cond(), code_fort::cond(), if_exprt::cond(), goto_convertt::targetst::continue_set, goto_convertt::targetst::continue_stack_size, goto_convertt::targetst::continue_target, goto_convertt::convert(), goto_convertt::convert_asm(), goto_convertt::convert_assert(), goto_convertt::convert_assign(), goto_convertt::convert_assume(), goto_convertt::convert_atomic_begin(), goto_convertt::convert_atomic_end(), goto_convertt::convert_block(), goto_convertt::convert_bp_abortif(), goto_convertt::convert_bp_enforce(), goto_convertt::convert_break(), goto_convertt::convert_continue(), goto_convertt::convert_cpp_delete(), goto_convertt::convert_CPROVER_throw(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), goto_convertt::convert_decl_type(), goto_convertt::convert_dowhile(), goto_convertt::convert_end_thread(), goto_convertt::convert_expression(), goto_convertt::convert_for(), goto_convertt::convert_function_call(), goto_convertt::convert_gcc_computed_goto(), goto_convertt::convert_gcc_local_label(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_goto(), goto_convertt::convert_ifthenelse(), goto_convertt::convert_init(), goto_convertt::convert_label(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_except(), goto_convertt::convert_msc_try_finally(), goto_convertt::convert_non_deterministic_goto(), goto_convertt::convert_return(), goto_convertt::convert_skip(), goto_convertt::convert_specc_event(), goto_convertt::convert_specc_notify(), goto_convertt::convert_specc_par(), goto_convertt::convert_specc_wait(), goto_convertt::convert_start_thread(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), goto_convertt::convert_try_catch(), goto_convertt::convert_while(), goto_convertt::copy(), exprt::copy_to_operands(), DEAD, DECL, goto_convertt::targetst::default_target, goto_program_templatet< codeT, guardT >::destructive_append(), goto_convertt::targetst::destructor_stack, goto_convertt::do_cpp_new(), goto_convertt::do_function_call(), goto_convertt::do_java_new(), goto_convertt::do_java_new_array(), code_ifthenelset::else_case(), code_blockt::end_location(), END_THREAD, messaget::eom(), messaget::error(), if_exprt::false_case(), irept::find(), exprt::find_source_location(), goto_convertt::finish_computed_gotos(), goto_convertt::finish_gotos(), forall_expr, forall_goto_program_instructions, Forall_goto_program_instructions, forall_irep, forall_operands, Forall_operands, code_function_callt::function(), goto_convertt::generate_conditional_branch(), goto_convertt::generate_ifthenelse(), irept::get(), get_destructor(), code_labelt::get_label(), codet::get_statement(), goto_convertt::get_string_constant(), irept::get_sub(), GOTO, goto_convertt::goto_convert(), goto_convertt::goto_convert_rec(), goto_convertt::targetst::gotos, has_prefix(), goto_convertt::targetst::has_return_value, code_returnt::has_return_value(), irept::id(), id2string(), code_fort::init(), goto_program_templatet< codeT, guardT >::insert_after(), goto_program_templatet< codeT, guardT >::instructions, code_switch_caset::is_default(), irept::is_nil(), irept::is_not_nil(), symbolt::is_static_lifetime, exprt::is_true(), code_fort::iter(), goto_convertt::targetst::labels, code_assignt::lhs(), binary_relation_exprt::lhs(), code_function_callt::lhs(), goto_convertt::lookup(), namespacet::lookup(), make_next_state(), irept::make_nil(), exprt::make_not(), exprt::make_typecast(), exprt::move_to_operands(), symbolt::name, goto_convertt::needs_cleaning(), goto_convertt::ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), OTHER, pointer_type(), goto_convertt::replace_new_object(), exprt::reserve_operands(), goto_convertt::targetst::return_set, goto_convertt::targetst::return_target, code_returnt::return_value(), code_assignt::rhs(), binary_relation_exprt::rhs(), irept::set(), goto_convertt::targetst::set_break(), goto_convertt::targetst::set_continue(), goto_convertt::targetst::set_default(), codet::set_statement(), simplify(), SKIP, exprt::source_location(), START_THREAD, typet::subtype(), irept::swap(), goto_program_templatet< codeT, guardT >::swap(), goto_convertt::targets, code_ifthenelset::then_case(), 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(), to_code_type(), to_code_while(), to_if_expr(), to_side_effect_expr(), if_exprt::true_case(), symbolt::type, exprt::type(), goto_convertt::unwind_destructor_stack(), and code_switcht::value().