CBMC
Public Member Functions | Public Attributes | List of all members
loop_idt Struct Reference

Loop id used to identify loops. More...

#include <loop_ids.h>

+ Collaboration diagram for loop_idt:

Public Member Functions

 loop_idt (const irep_idt &function_id, const unsigned int loop_number)
 
bool operator== (const loop_idt &o) const
 
bool operator< (const loop_idt &o) const
 

Public Attributes

irep_idt function_id
 
unsigned int loop_number
 

Detailed Description

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.

Constructor & Destructor Documentation

◆ loop_idt()

loop_idt::loop_idt ( const irep_idt &  function_id,
const unsigned int  loop_number 
)
inline

Definition at line 29 of file loop_ids.h.

Member Function Documentation

◆ operator<()

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

Definition at line 42 of file loop_ids.h.

◆ operator==()

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

Definition at line 37 of file loop_ids.h.

Member Data Documentation

◆ function_id

irep_idt loop_idt::function_id

Definition at line 34 of file loop_ids.h.

◆ loop_number

unsigned int loop_idt::loop_number

Definition at line 35 of file loop_ids.h.

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