CBMC
|
Public Member Functions | |
caset (const goto_programt &goto_program, const exprt &v, goto_programt::const_targett sel, goto_programt::const_targett st) | |
Public Attributes | |
const exprt | value |
goto_programt::const_targett | case_selector |
goto_programt::const_targett | case_start |
goto_programt::const_targett | case_last |
Definition at line 34 of file goto_program2code.h.
|
inline |
Definition at line 41 of file goto_program2code.h.
goto_programt::const_targett goto_program2codet::caset::case_last |
Definition at line 39 of file goto_program2code.h.
goto_programt::const_targett goto_program2codet::caset::case_selector |
Definition at line 37 of file goto_program2code.h.
goto_programt::const_targett goto_program2codet::caset::case_start |
Definition at line 38 of file goto_program2code.h.
const exprt goto_program2codet::caset::value |
Definition at line 36 of file goto_program2code.h.