CBMC
Public Types | Public Member Functions | Static Public Member Functions | Private Attributes | Friends | List of all members
range_spect Class Reference

Data type to describe upper and lower bounds of the range of bits that a read or write access may affect. More...

#include <goto_rw.h>

Public Types

using value_type = int
 

Public Member Functions

 range_spect (value_type v)
 
bool is_unknown () const
 
bool operator< (const range_spect &other) const
 
bool operator<= (const range_spect &other) const
 
bool operator> (const range_spect &other) const
 
bool operator>= (const range_spect &other) const
 
bool operator== (const range_spect &other) const
 
range_spect operator+ (const range_spect &other) const
 
range_spect & operator+= (const range_spect &other)
 
range_spect operator- (const range_spect &other) const
 
range_spect & operator-= (const range_spect &other)
 
range_spect operator* (const range_spect &other) const
 

Static Public Member Functions

static range_spect unknown ()
 
static range_spect to_range_spect (const mp_integer &size)
 

Private Attributes

value_type v
 

Friends

std::ostream & operator<< (std::ostream &, const range_spect &)
 

Detailed Description

Data type to describe upper and lower bounds of the range of bits that a read or write access may affect.

Each of the bounds may be not known or not constant, which is expressed using range_spect::unknown.

Definition at line 60 of file goto_rw.h.

Member Typedef Documentation

◆ value_type

using range_spect::value_type = int

Definition at line 63 of file goto_rw.h.

Constructor & Destructor Documentation

◆ range_spect()

range_spect::range_spect ( value_type  v)
inlineexplicit

Definition at line 65 of file goto_rw.h.

Member Function Documentation

◆ is_unknown()

bool range_spect::is_unknown ( ) const
inline

Definition at line 74 of file goto_rw.h.

◆ operator*()

range_spect range_spect::operator* ( const range_spect &  other) const
inline

Definition at line 155 of file goto_rw.h.

◆ operator+()

range_spect range_spect::operator+ ( const range_spect &  other) const
inline

Definition at line 127 of file goto_rw.h.

◆ operator+=()

range_spect& range_spect::operator+= ( const range_spect &  other)
inline

Definition at line 134 of file goto_rw.h.

◆ operator-()

range_spect range_spect::operator- ( const range_spect &  other) const
inline

Definition at line 141 of file goto_rw.h.

◆ operator-=()

range_spect& range_spect::operator-= ( const range_spect &  other)
inline

Definition at line 148 of file goto_rw.h.

◆ operator<()

bool range_spect::operator< ( const range_spect &  other) const
inline

Definition at line 98 of file goto_rw.h.

◆ operator<=()

bool range_spect::operator<= ( const range_spect &  other) const
inline

Definition at line 104 of file goto_rw.h.

◆ operator==()

bool range_spect::operator== ( const range_spect &  other) const
inline

Definition at line 122 of file goto_rw.h.

◆ operator>()

bool range_spect::operator> ( const range_spect &  other) const
inline

Definition at line 110 of file goto_rw.h.

◆ operator>=()

bool range_spect::operator>= ( const range_spect &  other) const
inline

Definition at line 116 of file goto_rw.h.

◆ to_range_spect()

static range_spect range_spect::to_range_spect ( const mp_integer &  size)
inlinestatic

Definition at line 79 of file goto_rw.h.

◆ unknown()

static range_spect range_spect::unknown ( )
inlinestatic

Definition at line 69 of file goto_rw.h.

Friends And Related Function Documentation

◆ operator<<

std::ostream& operator<< ( std::ostream &  os,
const range_spect &  r 
)
friend

Definition at line 167 of file goto_rw.h.

Member Data Documentation

◆ v

value_type range_spect::v
private

Definition at line 163 of file goto_rw.h.

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