|
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 539 of file goto_convert_class.h.
|
inlineexplicit |
Definition at line 543 of file goto_convert_class.h.
|
inline |
Definition at line 550 of file goto_convert_class.h.
| bool goto_convertt::leave_targett::leave_set |
Definition at line 557 of file goto_convert_class.h.
| node_indext goto_convertt::leave_targett::leave_stack_node |
Definition at line 558 of file goto_convert_class.h.
| goto_programt::targett goto_convertt::leave_targett::leave_target |
Definition at line 556 of file goto_convert_class.h.