CBMC
|
#include <goto_convert_class.h>
Public Member Functions | |
leave_targett (const targetst &targets) | |
void | restore (targetst &targets) |
Public Attributes | |
goto_programt::targett | leave_target |
bool | leave_set |
node_indext | leave_stack_node |
Definition at line 556 of file goto_convert_class.h.
|
inlineexplicit |
Definition at line 560 of file goto_convert_class.h.
|
inline |
Definition at line 567 of file goto_convert_class.h.
bool goto_convertt::leave_targett::leave_set |
Definition at line 574 of file goto_convert_class.h.
node_indext goto_convertt::leave_targett::leave_stack_node |
Definition at line 575 of file goto_convert_class.h.
goto_programt::targett goto_convertt::leave_targett::leave_target |
Definition at line 573 of file goto_convert_class.h.