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.

Referenced by operator--().

§ increase()

void loc_reft::increase ( )
inline

Definition at line 29 of file loc_ref.h.

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

§ is_nil()

bool loc_reft::is_nil ( ) const
inline

§ 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: