CBMC
dfcc_loop_tags.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for loop contracts
4 
5 Author: Qinheping Hu, qinhh@amazon.com
6 Author: Remi Delmas, delmasrd@amazon.com
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_LOOP_TAGS_H
16 
18 
19 void dfcc_set_loop_id(
21  std::size_t loop_id);
22 
23 bool dfcc_has_loop_id(
25  std::size_t loop_id);
26 
27 std::optional<std::size_t>
29 
33 
37 
41 
45 
49 
50 void dfcc_remove_loop_tags(source_locationt &source_location);
51 void dfcc_remove_loop_tags(goto_programt &goto_program);
53 #endif
std::list< instructiont >::const_iterator const_targett
Definition: goto_program.h:382
std::list< instructiont >::iterator targett
The target for gotos and for start_thread nodes.
Definition: goto_program.h:381
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
bool dfcc_has_loop_id(const goto_programt::instructiont::const_targett &target, std::size_t loop_id)
void dfcc_set_loop_exiting(goto_programt::instructiont::targett &target)
void dfcc_set_loop_latch(goto_programt::instructiont::targett &target)
bool dfcc_is_loop_head(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_latch(const goto_programt::instructiont::const_targett &target)
void dfcc_remove_loop_tags(source_locationt &source_location)
bool dfcc_is_loop_top_level(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_top_level(goto_programt::instructiont::targett &target)
void dfcc_set_loop_body(goto_programt::instructiont::targett &target)
std::optional< std::size_t > dfcc_get_loop_id(const goto_programt::instructiont::const_targett &target)
bool dfcc_is_loop_exiting(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_id(goto_programt::instructiont::targett &target, std::size_t loop_id)
bool dfcc_is_loop_body(const goto_programt::instructiont::const_targett &target)
void dfcc_set_loop_head(goto_programt::instructiont::targett &target)
Concrete Goto Program.