CBMC
build_declaration_hops_inputst Struct Reference
+ Collaboration diagram for build_declaration_hops_inputst:

Public Attributes

irep_idt mode
 
irep_idt label
 
goto_programt::targett goto_instruction
 
goto_programt::targett label_instruction
 
node_indext label_scope_index = 0
 
node_indext end_scope_index = 0
 

Detailed Description

Definition at line 96 of file goto_convert.cpp.

Member Data Documentation

◆ end_scope_index

node_indext build_declaration_hops_inputst::end_scope_index = 0

Definition at line 103 of file goto_convert.cpp.

◆ goto_instruction

goto_programt::targett build_declaration_hops_inputst::goto_instruction

Definition at line 100 of file goto_convert.cpp.

◆ label

irep_idt build_declaration_hops_inputst::label

Definition at line 99 of file goto_convert.cpp.

◆ label_instruction

goto_programt::targett build_declaration_hops_inputst::label_instruction

Definition at line 101 of file goto_convert.cpp.

◆ label_scope_index

node_indext build_declaration_hops_inputst::label_scope_index = 0

Definition at line 102 of file goto_convert.cpp.

◆ mode

irep_idt build_declaration_hops_inputst::mode

Definition at line 98 of file goto_convert.cpp.


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