Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head, body, exiting, latch. More...
#include <goto-programs/goto_program.h>
Include dependency graph for dfcc_loop_tags.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Detailed Description
Functions that allow to tag GOTO instructions with loop identifiers and loop instruction type: head, body, exiting, latch.
Definition in file dfcc_loop_tags.h.
Function Documentation
◆ dfcc_get_loop_id()
| std::optional<std::size_t> dfcc_get_loop_id | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 27 of file dfcc_loop_tags.cpp.
◆ dfcc_has_loop_id()
| bool dfcc_has_loop_id | ( | const goto_programt::instructiont::const_targett & | target, |
| std::size_t | loop_id | ||
| ) |
Definition at line 35 of file dfcc_loop_tags.cpp.
◆ dfcc_is_loop_body()
| bool dfcc_is_loop_body | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 72 of file dfcc_loop_tags.cpp.
◆ dfcc_is_loop_exiting()
| bool dfcc_is_loop_exiting | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 82 of file dfcc_loop_tags.cpp.
◆ dfcc_is_loop_head()
| bool dfcc_is_loop_head | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 62 of file dfcc_loop_tags.cpp.
◆ dfcc_is_loop_latch()
| bool dfcc_is_loop_latch | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 93 of file dfcc_loop_tags.cpp.
◆ dfcc_is_loop_top_level()
| bool dfcc_is_loop_top_level | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 104 of file dfcc_loop_tags.cpp.
◆ dfcc_remove_loop_tags() [1/3]
| void dfcc_remove_loop_tags | ( | goto_programt & | goto_program | ) |
Definition at line 125 of file dfcc_loop_tags.cpp.
◆ dfcc_remove_loop_tags() [2/3]
| void dfcc_remove_loop_tags | ( | goto_programt::targett & | target | ) |
Definition at line 120 of file dfcc_loop_tags.cpp.
◆ dfcc_remove_loop_tags() [3/3]
| void dfcc_remove_loop_tags | ( | source_locationt & | source_location | ) |
Definition at line 110 of file dfcc_loop_tags.cpp.
◆ dfcc_set_loop_body()
| void dfcc_set_loop_body | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 67 of file dfcc_loop_tags.cpp.
◆ dfcc_set_loop_exiting()
| void dfcc_set_loop_exiting | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 77 of file dfcc_loop_tags.cpp.
◆ dfcc_set_loop_head()
| void dfcc_set_loop_head | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 57 of file dfcc_loop_tags.cpp.
◆ dfcc_set_loop_id()
| void dfcc_set_loop_id | ( | goto_programt::instructiont::targett & | target, |
| std::size_t | loop_id | ||
| ) |
Definition at line 19 of file dfcc_loop_tags.cpp.
◆ dfcc_set_loop_latch()
| void dfcc_set_loop_latch | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 88 of file dfcc_loop_tags.cpp.
◆ dfcc_set_loop_top_level()
| void dfcc_set_loop_top_level | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 99 of file dfcc_loop_tags.cpp.
