#include <scope_tree.h>
Collaboration diagram for scope_treet::declaration_statet:Public Attributes | |
| goto_programt::targett | instruction |
| This is an iterator which points to the instruction where the declaration takes place. More... | |
| std::unordered_set< irep_idt, irep_id_hash > | accounted_flags |
| In order to handle user goto statements which jump into a scope the declaration may need to be followed by instructions which handle flags which are intended to cause control flow to continue to a specific point within that scope. More... | |
Detailed Description
Definition at line 95 of file scope_tree.h.
Member Data Documentation
◆ accounted_flags
| std::unordered_set<irep_idt, irep_id_hash> scope_treet::declaration_statet::accounted_flags |
In order to handle user goto statements which jump into a scope the declaration may need to be followed by instructions which handle flags which are intended to cause control flow to continue to a specific point within that scope.
The addition of the checks for each flag is performed in a lazy fashion, as each goto which jumps into a scope is finalised. In the case where multiple goto statements jump to the same label, a flag and its associated control flow may be reused. This set is used to track which flags have been accounted for in the code following this declaration. Each additional goto for the same label may need to account for more declarations. This is due to the possibility of different goto statements causing additional declarations to be added to the scope.
Definition at line 111 of file scope_tree.h.
◆ instruction
| goto_programt::targett scope_treet::declaration_statet::instruction |
This is an iterator which points to the instruction where the declaration takes place.
Definition at line 99 of file scope_tree.h.
The documentation for this struct was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/ansi-c/goto-conversion/scope_tree.h
