cprover
goto_convertt::targetst Struct Reference

#include <goto_convert_class.h>

Collaboration diagram for goto_convertt::targetst:
[legend]

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
 

Detailed Description

Definition at line 294 of file goto_convert_class.h.

Constructor & Destructor Documentation

◆ targetst()

goto_convertt::targetst::targetst ( )
inline

Definition at line 313 of file goto_convert_class.h.

Member Function Documentation

◆ set_break()

void goto_convertt::targetst::set_break ( goto_programt::targett  _break_target)
inline

◆ set_continue()

void goto_convertt::targetst::set_continue ( goto_programt::targett  _continue_target)
inline

◆ set_default()

void goto_convertt::targetst::set_default ( goto_programt::targett  _default_target)
inline

◆ set_leave()

void goto_convertt::targetst::set_leave ( goto_programt::targett  _leave_target)
inline

◆ set_return()

void goto_convertt::targetst::set_return ( goto_programt::targett  _return_target)
inline

Definition at line 344 of file goto_convert_class.h.

References return_set, and return_target.

Referenced by goto_convert_functionst::convert_function().

◆ set_throw()

void goto_convertt::targetst::set_throw ( goto_programt::targett  _throw_target)
inline

Member Data Documentation

◆ break_set

◆ break_stack_size

std::size_t goto_convertt::targetst::break_stack_size

Definition at line 310 of file goto_convert_class.h.

Referenced by goto_convertt::convert_break(), and set_break().

◆ break_target

◆ cases

◆ cases_map

◆ computed_gotos

computed_gotost goto_convertt::targetst::computed_gotos

◆ continue_set

◆ continue_stack_size

std::size_t goto_convertt::targetst::continue_stack_size

Definition at line 310 of file goto_convert_class.h.

Referenced by goto_convertt::convert_continue(), and set_continue().

◆ continue_target

◆ default_set

bool goto_convertt::targetst::default_set

◆ default_target

◆ destructor_stack

◆ gotos

gotost goto_convertt::targetst::gotos

◆ has_return_value

bool goto_convertt::targetst::has_return_value

◆ labels

labelst goto_convertt::targetst::labels

◆ leave_set

◆ leave_stack_size

std::size_t goto_convertt::targetst::leave_stack_size

Definition at line 310 of file goto_convert_class.h.

Referenced by goto_convertt::convert_msc_leave(), and set_leave().

◆ leave_target

◆ return_set

bool goto_convertt::targetst::return_set

Definition at line 296 of file goto_convert_class.h.

Referenced by goto_convertt::convert_return(), and set_return().

◆ return_target

goto_programt::targett goto_convertt::targetst::return_target

◆ throw_set

◆ throw_stack_size

std::size_t goto_convertt::targetst::throw_stack_size

Definition at line 310 of file goto_convert_class.h.

Referenced by goto_convertt::convert_CPROVER_throw(), and set_throw().

◆ throw_target


The documentation for this struct was generated from the following file: