|
CBMC
|
#include <goto_inline_class.h>
Collaboration diagram for goto_inlinet::goto_inline_logt::goto_inline_log_infot:Public Attributes | |
| unsigned | begin_location_number |
| unsigned | end_location_number |
| unsigned | call_location_number |
| irep_idt | function |
| goto_programt::const_targett | end |
Definition at line 100 of file goto_inline_class.h.
| unsigned goto_inlinet::goto_inline_logt::goto_inline_log_infot::begin_location_number |
Definition at line 104 of file goto_inline_class.h.
| unsigned goto_inlinet::goto_inline_logt::goto_inline_log_infot::call_location_number |
Definition at line 106 of file goto_inline_class.h.
| goto_programt::const_targett goto_inlinet::goto_inline_logt::goto_inline_log_infot::end |
Definition at line 108 of file goto_inline_class.h.
| unsigned goto_inlinet::goto_inline_logt::goto_inline_log_infot::end_location_number |
Definition at line 105 of file goto_inline_class.h.
| irep_idt goto_inlinet::goto_inline_logt::goto_inline_log_infot::function |
Definition at line 107 of file goto_inline_class.h.