cprover
|
#include <goto_convert_class.h>
Public Member Functions | |
targetst () | |
void | set_break (goto_programt::targett _break_target) |
void | set_continue (goto_programt::targett _continue_target) |
void | set_default (goto_programt::targett _default_target) |
void | set_return (goto_programt::targett _return_target) |
void | set_throw (goto_programt::targett _throw_target) |
void | set_leave (goto_programt::targett _leave_target) |
Public Attributes | |
bool | return_set |
bool | has_return_value |
bool | break_set |
bool | continue_set |
bool | default_set |
bool | throw_set |
bool | leave_set |
labelst | labels |
gotost | gotos |
computed_gotost | computed_gotos |
destructor_stackt | destructor_stack |
casest | cases |
cases_mapt | cases_map |
goto_programt::targett | return_target |
goto_programt::targett | break_target |
goto_programt::targett | continue_target |
goto_programt::targett | default_target |
goto_programt::targett | throw_target |
goto_programt::targett | leave_target |
std::size_t | break_stack_size |
std::size_t | continue_stack_size |
std::size_t | throw_stack_size |
std::size_t | leave_stack_size |
Definition at line 367 of file goto_convert_class.h.
|
inline |
Definition at line 386 of file goto_convert_class.h.
|
inline |
Definition at line 401 of file goto_convert_class.h.
References break_set, break_stack_size, break_target, and destructor_stack.
Referenced by goto_convertt::convert_dowhile(), goto_convertt::convert_for(), goto_convertt::convert_switch(), and goto_convertt::convert_while().
|
inline |
Definition at line 408 of file goto_convert_class.h.
References continue_set, continue_stack_size, continue_target, and destructor_stack.
Referenced by goto_convertt::convert_dowhile(), goto_convertt::convert_for(), and goto_convertt::convert_while().
|
inline |
Definition at line 415 of file goto_convert_class.h.
References default_set, and default_target.
Referenced by goto_convertt::convert_switch(), and goto_convertt::convert_switch_case().
|
inline |
Definition at line 434 of file goto_convert_class.h.
References destructor_stack, leave_set, leave_stack_size, and leave_target.
Referenced by goto_convertt::convert_msc_try_finally().
|
inline |
Definition at line 421 of file goto_convert_class.h.
References return_set, and return_target.
Referenced by goto_convert_functionst::convert_function().
|
inline |
Definition at line 427 of file goto_convert_class.h.
References destructor_stack, throw_set, throw_stack_size, and throw_target.
Referenced by goto_convertt::convert_CPROVER_try_catch().
bool goto_convertt::targetst::break_set |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convertt::break_continue_targetst::break_continue_targetst(), goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::convert_break(), goto_convertt::break_continue_targetst::restore(), goto_convertt::break_switch_targetst::restore(), and set_break().
std::size_t goto_convertt::targetst::break_stack_size |
Definition at line 383 of file goto_convert_class.h.
Referenced by goto_convertt::convert_break(), and set_break().
goto_programt::targett goto_convertt::targetst::break_target |
Definition at line 380 of file goto_convert_class.h.
Referenced by goto_convertt::break_continue_targetst::break_continue_targetst(), goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::convert_break(), goto_convertt::break_continue_targetst::restore(), goto_convertt::break_switch_targetst::restore(), and set_break().
casest goto_convertt::targetst::cases |
Definition at line 377 of file goto_convert_class.h.
Referenced by goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), and goto_convertt::break_switch_targetst::restore().
cases_mapt goto_convertt::targetst::cases_map |
Definition at line 378 of file goto_convert_class.h.
Referenced by goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::convert_gcc_switch_case_range(), goto_convertt::convert_switch(), goto_convertt::convert_switch_case(), and goto_convertt::break_switch_targetst::restore().
computed_gotost goto_convertt::targetst::computed_gotos |
Definition at line 374 of file goto_convert_class.h.
Referenced by goto_convertt::convert_gcc_computed_goto(), and goto_convertt::finish_computed_gotos().
bool goto_convertt::targetst::continue_set |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convertt::break_continue_targetst::break_continue_targetst(), goto_convertt::convert_continue(), goto_convertt::break_continue_targetst::restore(), and set_continue().
std::size_t goto_convertt::targetst::continue_stack_size |
Definition at line 383 of file goto_convert_class.h.
Referenced by goto_convertt::convert_continue(), and set_continue().
goto_programt::targett goto_convertt::targetst::continue_target |
Definition at line 380 of file goto_convert_class.h.
Referenced by goto_convertt::break_continue_targetst::break_continue_targetst(), goto_convertt::convert_continue(), goto_convertt::break_continue_targetst::restore(), and set_continue().
bool goto_convertt::targetst::default_set |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::break_switch_targetst::restore(), and set_default().
goto_programt::targett goto_convertt::targetst::default_target |
Definition at line 380 of file goto_convert_class.h.
Referenced by goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::convert_switch(), goto_convertt::break_switch_targetst::restore(), and set_default().
destructor_stackt goto_convertt::targetst::destructor_stack |
Definition at line 375 of file goto_convert_class.h.
Referenced by goto_convertt::break_switch_targetst::break_switch_targetst(), goto_convertt::convert_block(), goto_convertt::convert_CPROVER_try_catch(), goto_convertt::convert_CPROVER_try_finally(), goto_convertt::convert_decl(), goto_convertt::convert_goto(), goto_convertt::convert_label(), goto_convertt::convert_msc_leave(), goto_convertt::convert_msc_try_finally(), goto_convertt::convert_start_thread(), goto_convertt::leave_targett::leave_targett(), goto_convertt::make_compound_literal(), set_break(), set_continue(), set_leave(), set_throw(), goto_convertt::throw_targett::throw_targett(), and goto_convertt::unwind_destructor_stack().
gotost goto_convertt::targetst::gotos |
Definition at line 373 of file goto_convert_class.h.
Referenced by goto_convertt::convert_goto(), goto_convertt::convert_start_thread(), and goto_convertt::finish_gotos().
bool goto_convertt::targetst::has_return_value |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convert_functionst::convert_function(), and goto_convertt::convert_return().
labelst goto_convertt::targetst::labels |
Definition at line 372 of file goto_convert_class.h.
Referenced by goto_convertt::convert_label(), goto_convertt::finish_computed_gotos(), and goto_convertt::finish_gotos().
bool goto_convertt::targetst::leave_set |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convertt::convert_msc_leave(), goto_convertt::leave_targett::leave_targett(), goto_convertt::leave_targett::restore(), and set_leave().
std::size_t goto_convertt::targetst::leave_stack_size |
Definition at line 383 of file goto_convert_class.h.
Referenced by goto_convertt::convert_msc_leave(), and set_leave().
goto_programt::targett goto_convertt::targetst::leave_target |
Definition at line 380 of file goto_convert_class.h.
Referenced by goto_convertt::convert_msc_leave(), goto_convertt::leave_targett::leave_targett(), goto_convertt::leave_targett::restore(), and set_leave().
bool goto_convertt::targetst::return_set |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convertt::convert_return(), and set_return().
goto_programt::targett goto_convertt::targetst::return_target |
Definition at line 380 of file goto_convert_class.h.
Referenced by goto_convertt::convert_CPROVER_throw(), goto_convertt::convert_return(), and set_return().
bool goto_convertt::targetst::throw_set |
Definition at line 369 of file goto_convert_class.h.
Referenced by goto_convertt::convert_CPROVER_throw(), goto_convertt::throw_targett::restore(), set_throw(), and goto_convertt::throw_targett::throw_targett().
std::size_t goto_convertt::targetst::throw_stack_size |
Definition at line 383 of file goto_convert_class.h.
Referenced by goto_convertt::convert_CPROVER_throw(), and set_throw().
goto_programt::targett goto_convertt::targetst::throw_target |
Definition at line 380 of file goto_convert_class.h.
Referenced by goto_convertt::convert_CPROVER_throw(), goto_convertt::throw_targett::restore(), set_throw(), and goto_convertt::throw_targett::throw_targett().