cprover
loc_reft Class Reference

#include <loc_ref.h>

Public Member Functions

loc_reft next_loc () const
 
void increase ()
 
void decrease ()
 
bool is_nil () const
 
 loc_reft ()
 
loc_reftoperator++ ()
 
loc_reftoperator-- ()
 
bool operator< (const loc_reft other) const
 
bool operator!= (const loc_reft other) const
 
bool operator== (const loc_reft other) const
 

Static Public Member Functions

static loc_reft nil ()
 

Public Attributes

unsigned loc_number
 

Detailed Description

Definition at line 17 of file loc_ref.h.

Constructor & Destructor Documentation

◆ loc_reft()

loc_reft::loc_reft ( )
inline

Definition at line 44 of file loc_ref.h.

Referenced by nil().

Member Function Documentation

◆ decrease()

void loc_reft::decrease ( )
inline

Definition at line 34 of file loc_ref.h.

References loc_number.

Referenced by operator--().

◆ increase()

void loc_reft::increase ( )
inline

Definition at line 29 of file loc_ref.h.

References loc_number.

Referenced by next_loc(), and operator++().

◆ is_nil()

bool loc_reft::is_nil ( ) const
inline

Definition at line 39 of file loc_ref.h.

References loc_number, and nil().

Referenced by build_goto_trace(), and operator<<().

◆ next_loc()

loc_reft loc_reft::next_loc ( ) const
inline

Definition at line 22 of file loc_ref.h.

References increase().

Referenced by path_symext::function_call_rec().

◆ nil()

static loc_reft loc_reft::nil ( )
inlinestatic

Definition at line 48 of file loc_ref.h.

References loc_reft().

Referenced by locst::build(), and is_nil().

◆ operator!=()

bool loc_reft::operator!= ( const loc_reft  other) const
inline

Definition at line 70 of file loc_ref.h.

References loc_number.

◆ operator++()

loc_reft& loc_reft::operator++ ( )
inline

Definition at line 53 of file loc_ref.h.

References increase().

◆ operator--()

loc_reft& loc_reft::operator-- ( )
inline

Definition at line 59 of file loc_ref.h.

References decrease().

◆ operator<()

bool loc_reft::operator< ( const loc_reft  other) const
inline

Definition at line 65 of file loc_ref.h.

References loc_number.

◆ operator==()

bool loc_reft::operator== ( const loc_reft  other) const
inline

Definition at line 75 of file loc_ref.h.

References loc_number.

Member Data Documentation

◆ loc_number


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