CBMC
|
Loop id used to identify loops. More...
#include <loop_ids.h>
Public Member Functions | |
loop_idt (const irep_idt &function_id, const unsigned int loop_number) | |
loop_idt (const loop_idt &other)=default | |
bool | operator== (const loop_idt &o) const |
bool | operator!= (const loop_idt &o) const |
bool | operator< (const loop_idt &o) const |
Public Attributes | |
irep_idt | function_id |
unsigned int | loop_number |
Loop id used to identify loops.
It consists of two arguments: function_id
the function id stored as keys of function_mapt
; and loop_number
the index of loop indicated by loop_number
of backward goto instruction.
Definition at line 27 of file loop_ids.h.
|
inline |
Definition at line 29 of file loop_ids.h.
|
default |
|
inline |
Definition at line 44 of file loop_ids.h.
|
inline |
Definition at line 49 of file loop_ids.h.
|
inline |
Definition at line 39 of file loop_ids.h.
irep_idt loop_idt::function_id |
Definition at line 36 of file loop_ids.h.
unsigned int loop_idt::loop_number |
Definition at line 37 of file loop_ids.h.