CBMC
dfcc_loop_tags.cpp File Reference
#include "dfcc_loop_tags.h"
+ Include dependency graph for dfcc_loop_tags.cpp:

Go to the source code of this file.

Functions

void dfcc_set_loop_id (goto_programt::instructiont::targett &target, const std::size_t loop_id)
 
std::optional< std::size_t > dfcc_get_loop_id (const goto_programt::instructiont::const_targett &target)
 
bool dfcc_has_loop_id (const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
 
static void dfcc_set_loop_tag (goto_programt::instructiont::targett &target, const irep_idt &tag)
 
static bool has_loop_tag (const goto_programt::instructiont::const_targett &target, const irep_idt &tag)
 
void dfcc_set_loop_head (goto_programt::instructiont::targett &target)
 
bool dfcc_is_loop_head (const goto_programt::instructiont::const_targett &target)
 
void dfcc_set_loop_body (goto_programt::instructiont::targett &target)
 
bool dfcc_is_loop_body (const goto_programt::instructiont::const_targett &target)
 
void dfcc_set_loop_exiting (goto_programt::instructiont::targett &target)
 
bool dfcc_is_loop_exiting (const goto_programt::instructiont::const_targett &target)
 
void dfcc_set_loop_latch (goto_programt::instructiont::targett &target)
 
bool dfcc_is_loop_latch (const goto_programt::instructiont::const_targett &target)
 
void dfcc_set_loop_top_level (goto_programt::instructiont::targett &target)
 
bool dfcc_is_loop_top_level (const goto_programt::instructiont::const_targett &target)
 
void dfcc_remove_loop_tags (source_locationt &source_location)
 
void dfcc_remove_loop_tags (goto_programt::targett &target)
 
void dfcc_remove_loop_tags (goto_programt &goto_program)
 

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"
 

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,
const 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_tag()

static void dfcc_set_loop_tag ( goto_programt::instructiont::targett target,
const irep_idt tag 
)
static

Definition at line 43 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.

◆ has_loop_tag()

static bool has_loop_tag ( const goto_programt::instructiont::const_targett target,
const irep_idt tag 
)
static

Definition at line 50 of file dfcc_loop_tags.cpp.

Variable Documentation

◆ ID_loop_body

const irep_idt ID_loop_body = "loop-body"

Definition at line 14 of file dfcc_loop_tags.cpp.

◆ ID_loop_exiting

const irep_idt ID_loop_exiting = "loop-exiting"

Definition at line 16 of file dfcc_loop_tags.cpp.

◆ ID_loop_head

const irep_idt ID_loop_head = "loop-head"

Definition at line 13 of file dfcc_loop_tags.cpp.

◆ ID_loop_id

const irep_idt ID_loop_id = "loop-id"

Definition at line 12 of file dfcc_loop_tags.cpp.

◆ ID_loop_latch

const irep_idt ID_loop_latch = "loop-latch"

Definition at line 15 of file dfcc_loop_tags.cpp.

◆ ID_loop_top_level

const irep_idt ID_loop_top_level = "loop-top-level"

Definition at line 17 of file dfcc_loop_tags.cpp.