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.

Constructor & Destructor Documentation

◆ loop_idt() [1/2]

loop_idt::loop_idt ( const irep_idt & function_id,

const unsigned int loop_number

)

inline

Definition at line 29 of file loop_ids.h.

◆ loop_idt() [2/2]

loop_idt::loop_idt ( const loop_idt & other )

default

Member Function Documentation

◆ operator!=()

bool loop_idt::operator!= ( const loop_idt & o ) const

inline

Definition at line 44 of file loop_ids.h.

◆ operator<()

bool loop_idt::operator< ( const loop_idt & o ) const

inline

Definition at line 49 of file loop_ids.h.

◆ operator==()

bool loop_idt::operator== ( const loop_idt & o ) const

inline

Definition at line 39 of file loop_ids.h.

Member Data Documentation

◆ function_id

irep_idt loop_idt::function_id

Definition at line 36 of file loop_ids.h.

◆ loop_number

unsigned int loop_idt::loop_number

Definition at line 37 of file loop_ids.h.

The documentation for this struct was generated from the following file:

/home/runner/work/cbmc/cbmc/src/goto-programs/loop_ids.h