CBMC
|
#include "dfcc_loop_tags.h"
Go to the source code of this file.
Variables | |
const irep_idt | ID_loop_id = "loop-id" |
const irep_idt | ID_loop_head = "loop-head" |
const irep_idt | ID_loop_body = "loop-body" |
const irep_idt | ID_loop_latch = "loop-latch" |
const irep_idt | ID_loop_exiting = "loop-exiting" |
const irep_idt | ID_loop_top_level = "loop-top-level" |
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.
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.
bool dfcc_is_loop_body | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 72 of file dfcc_loop_tags.cpp.
bool dfcc_is_loop_exiting | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 82 of file dfcc_loop_tags.cpp.
bool dfcc_is_loop_head | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 62 of file dfcc_loop_tags.cpp.
bool dfcc_is_loop_latch | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 93 of file dfcc_loop_tags.cpp.
bool dfcc_is_loop_top_level | ( | const goto_programt::instructiont::const_targett & | target | ) |
Definition at line 104 of file dfcc_loop_tags.cpp.
void dfcc_remove_loop_tags | ( | goto_programt & | goto_program | ) |
Definition at line 125 of file dfcc_loop_tags.cpp.
void dfcc_remove_loop_tags | ( | goto_programt::targett & | target | ) |
Definition at line 120 of file dfcc_loop_tags.cpp.
void dfcc_remove_loop_tags | ( | source_locationt & | source_location | ) |
Definition at line 110 of file dfcc_loop_tags.cpp.
void dfcc_set_loop_body | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 67 of file dfcc_loop_tags.cpp.
void dfcc_set_loop_exiting | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 77 of file dfcc_loop_tags.cpp.
void dfcc_set_loop_head | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 57 of file dfcc_loop_tags.cpp.
void dfcc_set_loop_id | ( | goto_programt::instructiont::targett & | target, |
const std::size_t | loop_id | ||
) |
Definition at line 19 of file dfcc_loop_tags.cpp.
void dfcc_set_loop_latch | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 88 of file dfcc_loop_tags.cpp.
|
static |
Definition at line 43 of file dfcc_loop_tags.cpp.
void dfcc_set_loop_top_level | ( | goto_programt::instructiont::targett & | target | ) |
Definition at line 99 of file dfcc_loop_tags.cpp.
|
static |
Definition at line 50 of file dfcc_loop_tags.cpp.
const irep_idt ID_loop_body = "loop-body" |
Definition at line 14 of file dfcc_loop_tags.cpp.
const irep_idt ID_loop_exiting = "loop-exiting" |
Definition at line 16 of file dfcc_loop_tags.cpp.
const irep_idt ID_loop_head = "loop-head" |
Definition at line 13 of file dfcc_loop_tags.cpp.
const irep_idt ID_loop_id = "loop-id" |
Definition at line 12 of file dfcc_loop_tags.cpp.
const irep_idt ID_loop_latch = "loop-latch" |
Definition at line 15 of file dfcc_loop_tags.cpp.
const irep_idt ID_loop_top_level = "loop-top-level" |
Definition at line 17 of file dfcc_loop_tags.cpp.