CBMC
bv_arithmetict Class Reference

#include <bv_arithmetic.h>

+ Collaboration diagram for bv_arithmetict:

Public Member Functions

 bv_arithmetict (const bv_spect &_spec)
 
 bv_arithmetict ()
 
 bv_arithmetict (const constant_exprt &expr)
 
void negate ()
 
void make_zero ()
 
bool is_zero () const
 
void from_integer (const mp_integer &i)
 
void change_spec (const bv_spect &dest_spec)
 
mp_integer to_integer () const
 
void print (std::ostream &out) const
 
std::string to_ansi_c_string () const
 
std::string format (const format_spect &format_spec) const
 
constant_exprt to_expr () const
 
void from_expr (const constant_exprt &expr)
 
bv_arithmetictoperator/= (const bv_arithmetict &other)
 
bv_arithmetictoperator*= (const bv_arithmetict &other)
 
bv_arithmetictoperator+= (const bv_arithmetict &other)
 
bv_arithmetictoperator-= (const bv_arithmetict &other)
 
bv_arithmetictoperator%= (const bv_arithmetict &other)
 
bool operator< (const bv_arithmetict &other)
 
bool operator<= (const bv_arithmetict &other)
 
bool operator> (const bv_arithmetict &other)
 
bool operator>= (const bv_arithmetict &other)
 
bool operator== (const bv_arithmetict &other)
 
bool operator!= (const bv_arithmetict &other)
 
bool operator== (int i)
 
std::ostream & operator<< (std::ostream &out)
 
void unpack (const mp_integer &i)
 
mp_integer pack () const
 

Public Attributes

bv_spect spec
 

Protected Member Functions

void adjust ()
 

Protected Attributes

mp_integer value
 

Detailed Description

Definition at line 49 of file bv_arithmetic.h.

Constructor & Destructor Documentation

◆ bv_arithmetict() [1/3]

bv_arithmetict::bv_arithmetict ( const bv_spect _spec)
inlineexplicit

Definition at line 54 of file bv_arithmetic.h.

◆ bv_arithmetict() [2/3]

bv_arithmetict::bv_arithmetict ( )
inline

Definition at line 59 of file bv_arithmetic.h.

◆ bv_arithmetict() [3/3]

bv_arithmetict::bv_arithmetict ( const constant_exprt expr)
inlineexplicit

Definition at line 63 of file bv_arithmetic.h.

Member Function Documentation

◆ adjust()

void bv_arithmetict::adjust ( )
protected

Definition at line 66 of file bv_arithmetic.cpp.

◆ change_spec()

void bv_arithmetict::change_spec ( const bv_spect dest_spec)

Definition at line 174 of file bv_arithmetic.cpp.

◆ format()

std::string bv_arithmetict::format ( const format_spect format_spec) const

Definition at line 51 of file bv_arithmetic.cpp.

◆ from_expr()

void bv_arithmetict::from_expr ( const constant_exprt expr)

Definition at line 180 of file bv_arithmetic.cpp.

◆ from_integer()

void bv_arithmetict::from_integer ( const mp_integer i)

Definition at line 60 of file bv_arithmetic.cpp.

◆ is_zero()

bool bv_arithmetict::is_zero ( ) const
inline

Definition at line 75 of file bv_arithmetic.h.

◆ make_zero()

void bv_arithmetict::make_zero ( )
inline

Definition at line 70 of file bv_arithmetic.h.

◆ negate()

void bv_arithmetict::negate ( )

◆ operator!=()

bool bv_arithmetict::operator!= ( const bv_arithmetict other)

Definition at line 169 of file bv_arithmetic.cpp.

◆ operator%=()

bv_arithmetict & bv_arithmetict::operator%= ( const bv_arithmetict other)

Definition at line 129 of file bv_arithmetic.cpp.

◆ operator*=()

bv_arithmetict & bv_arithmetict::operator*= ( const bv_arithmetict other)

Definition at line 99 of file bv_arithmetic.cpp.

◆ operator+=()

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

Definition at line 109 of file bv_arithmetic.cpp.

◆ operator-=()

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

Definition at line 119 of file bv_arithmetic.cpp.

◆ operator/=()

bv_arithmetict & bv_arithmetict::operator/= ( const bv_arithmetict other)

Definition at line 87 of file bv_arithmetic.cpp.

◆ operator<()

bool bv_arithmetict::operator< ( const bv_arithmetict other)

Definition at line 139 of file bv_arithmetic.cpp.

◆ operator<<()

std::ostream& bv_arithmetict::operator<< ( std::ostream &  out)
inline

Definition at line 111 of file bv_arithmetic.h.

◆ operator<=()

bool bv_arithmetict::operator<= ( const bv_arithmetict other)

Definition at line 144 of file bv_arithmetic.cpp.

◆ operator==() [1/2]

bool bv_arithmetict::operator== ( const bv_arithmetict other)

Definition at line 159 of file bv_arithmetic.cpp.

◆ operator==() [2/2]

bool bv_arithmetict::operator== ( int  i)

Definition at line 164 of file bv_arithmetic.cpp.

◆ operator>()

bool bv_arithmetict::operator> ( const bv_arithmetict other)

Definition at line 149 of file bv_arithmetic.cpp.

◆ operator>=()

bool bv_arithmetict::operator>= ( const bv_arithmetict other)

Definition at line 154 of file bv_arithmetic.cpp.

◆ pack()

mp_integer bv_arithmetict::pack ( ) const

Definition at line 75 of file bv_arithmetic.cpp.

◆ print()

void bv_arithmetict::print ( std::ostream &  out) const

Definition at line 46 of file bv_arithmetic.cpp.

◆ to_ansi_c_string()

std::string bv_arithmetict::to_ansi_c_string ( ) const
inline

Definition at line 86 of file bv_arithmetic.h.

◆ to_expr()

constant_exprt bv_arithmetict::to_expr ( ) const

Definition at line 82 of file bv_arithmetic.cpp.

◆ to_integer()

mp_integer bv_arithmetict::to_integer ( ) const
inline

Definition at line 82 of file bv_arithmetic.h.

◆ unpack()

void bv_arithmetict::unpack ( const mp_integer i)
inline

Definition at line 117 of file bv_arithmetic.h.

Member Data Documentation

◆ spec

bv_spect bv_arithmetict::spec

Definition at line 52 of file bv_arithmetic.h.

◆ value

mp_integer bv_arithmetict::value
protected

Definition at line 122 of file bv_arithmetic.h.


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