CBMC
goto_inlinet::goto_inline_logt::goto_inline_log_infot Class Reference

#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
 

Detailed Description

Definition at line 110 of file goto_inline_class.h.

Member Data Documentation

◆ begin_location_number

unsigned goto_inlinet::goto_inline_logt::goto_inline_log_infot::begin_location_number

Definition at line 114 of file goto_inline_class.h.

◆ call_location_number

unsigned goto_inlinet::goto_inline_logt::goto_inline_log_infot::call_location_number

Definition at line 116 of file goto_inline_class.h.

◆ end

goto_programt::const_targett goto_inlinet::goto_inline_logt::goto_inline_log_infot::end

Definition at line 118 of file goto_inline_class.h.

◆ end_location_number

unsigned goto_inlinet::goto_inline_logt::goto_inline_log_infot::end_location_number

Definition at line 115 of file goto_inline_class.h.

◆ function

irep_idt goto_inlinet::goto_inline_logt::goto_inline_log_infot::function

Definition at line 117 of file goto_inline_class.h.


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