CBMC
Public Member Functions | Public Attributes | List of all members
goto_convertt::targetst Struct Reference

#include <goto_convert_class.h>

+ Collaboration diagram for goto_convertt::targetst:

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

goto_programt * prefix = nullptr
 
goto_programt * suffix = nullptr
 
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
 
scope_treet scope_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
 
node_indext break_stack_node
 
node_indext continue_stack_node
 
node_indext throw_stack_node
 
node_indext leave_stack_node
 

Detailed Description

Definition at line 397 of file goto_convert_class.h.

Constructor & Destructor Documentation

◆ targetst()

goto_convertt::targetst::targetst ( )
inline

Definition at line 419 of file goto_convert_class.h.

Member Function Documentation

◆ set_break()

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

Definition at line 434 of file goto_convert_class.h.

◆ set_continue()

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

Definition at line 441 of file goto_convert_class.h.

◆ set_default()

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

Definition at line 448 of file goto_convert_class.h.

◆ set_leave()

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

Definition at line 467 of file goto_convert_class.h.

◆ set_return()

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

Definition at line 454 of file goto_convert_class.h.

◆ set_throw()

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

Definition at line 460 of file goto_convert_class.h.

Member Data Documentation

◆ break_set

bool goto_convertt::targetst::break_set

Definition at line 402 of file goto_convert_class.h.

◆ break_stack_node

node_indext goto_convertt::targetst::break_stack_node

Definition at line 416 of file goto_convert_class.h.

◆ break_target

goto_programt::targett goto_convertt::targetst::break_target

Definition at line 413 of file goto_convert_class.h.

◆ cases

casest goto_convertt::targetst::cases

Definition at line 410 of file goto_convert_class.h.

◆ cases_map

cases_mapt goto_convertt::targetst::cases_map

Definition at line 411 of file goto_convert_class.h.

◆ computed_gotos

computed_gotost goto_convertt::targetst::computed_gotos

Definition at line 407 of file goto_convert_class.h.

◆ continue_set

bool goto_convertt::targetst::continue_set

Definition at line 402 of file goto_convert_class.h.

◆ continue_stack_node

node_indext goto_convertt::targetst::continue_stack_node

Definition at line 416 of file goto_convert_class.h.

◆ continue_target

goto_programt::targett goto_convertt::targetst::continue_target

Definition at line 413 of file goto_convert_class.h.

◆ default_set

bool goto_convertt::targetst::default_set

Definition at line 402 of file goto_convert_class.h.

◆ default_target

goto_programt::targett goto_convertt::targetst::default_target

Definition at line 414 of file goto_convert_class.h.

◆ gotos

gotost goto_convertt::targetst::gotos

Definition at line 406 of file goto_convert_class.h.

◆ has_return_value

bool goto_convertt::targetst::has_return_value

Definition at line 402 of file goto_convert_class.h.

◆ labels

labelst goto_convertt::targetst::labels

Definition at line 405 of file goto_convert_class.h.

◆ leave_set

bool goto_convertt::targetst::leave_set

Definition at line 403 of file goto_convert_class.h.

◆ leave_stack_node

node_indext goto_convertt::targetst::leave_stack_node

Definition at line 417 of file goto_convert_class.h.

◆ leave_target

goto_programt::targett goto_convertt::targetst::leave_target

Definition at line 414 of file goto_convert_class.h.

◆ prefix

goto_programt* goto_convertt::targetst::prefix = nullptr

Definition at line 399 of file goto_convert_class.h.

◆ return_set

bool goto_convertt::targetst::return_set

Definition at line 402 of file goto_convert_class.h.

◆ return_target

goto_programt::targett goto_convertt::targetst::return_target

Definition at line 413 of file goto_convert_class.h.

◆ scope_stack

scope_treet goto_convertt::targetst::scope_stack

Definition at line 408 of file goto_convert_class.h.

◆ suffix

goto_programt* goto_convertt::targetst::suffix = nullptr

Definition at line 400 of file goto_convert_class.h.

◆ throw_set

bool goto_convertt::targetst::throw_set

Definition at line 403 of file goto_convert_class.h.

◆ throw_stack_node

node_indext goto_convertt::targetst::throw_stack_node

Definition at line 416 of file goto_convert_class.h.

◆ throw_target

goto_programt::targett goto_convertt::targetst::throw_target

Definition at line 414 of file goto_convert_class.h.

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