Loading...

Searching...

No Matches

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 62 of file goto_rw.h.

Member Typedef Documentation

◆ value_type

using range_spect::value_type = int

Definition at line 65 of file goto_rw.h.

Constructor & Destructor Documentation

◆ range_spect()

range_spect::range_spect ( value_type v )

inlineexplicit

Definition at line 67 of file goto_rw.h.

Member Function Documentation

◆ is_unknown()

bool range_spect::is_unknown ( ) const

inline

Definition at line 76 of file goto_rw.h.

◆ operator*()

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

inline

Definition at line 157 of file goto_rw.h.

◆ operator+()

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

inline

Definition at line 129 of file goto_rw.h.

◆ operator+=()

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

inline

Definition at line 136 of file goto_rw.h.

◆ operator-()

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

inline

Definition at line 143 of file goto_rw.h.

◆ operator-=()

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

inline

Definition at line 150 of file goto_rw.h.

◆ operator<()

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

inline

Definition at line 100 of file goto_rw.h.

◆ operator<=()

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

inline

Definition at line 106 of file goto_rw.h.

◆ operator==()

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

inline

Definition at line 124 of file goto_rw.h.

◆ operator>()

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

inline

Definition at line 112 of file goto_rw.h.

◆ operator>=()

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

inline

Definition at line 118 of file goto_rw.h.

◆ to_range_spect()

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

inlinestatic

Definition at line 81 of file goto_rw.h.

◆ unknown()

static range_spect range_spect::unknown ( )

inlinestatic

Definition at line 71 of file goto_rw.h.

Friends And Related Symbol Documentation

◆ operator<<

std::ostream & operator<< ( std::ostream & os,

const range_spect & r

)

friend

Definition at line 169 of file goto_rw.h.

Member Data Documentation

◆ v

value_type range_spect::v

private

Definition at line 165 of file goto_rw.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/goto_rw.h