cprover
fixedbvt Class Reference

#include <fixedbv.h>

Collaboration diagram for fixedbvt:
[legend]

Public Member Functions

 fixedbvt ()
 
 fixedbvt (const fixedbv_spect &_spec)
 
 fixedbvt (const constant_exprt &expr)
 
void from_integer (const mp_integer &i)
 
mp_integer to_integer () const
 
void from_expr (const constant_exprt &expr)
 
constant_exprt to_expr () const
 
void round (const fixedbv_spect &dest_spec)
 
std::string to_ansi_c_string () const
 
std::string format (const format_spect &format_spec) const
 
bool operator== (int i) const
 
bool is_zero () const
 
void negate ()
 
fixedbvtoperator/= (const fixedbvt &other)
 
fixedbvtoperator*= (const fixedbvt &other)
 
fixedbvtoperator+= (const fixedbvt &other)
 
fixedbvtoperator-= (const fixedbvt &other)
 
bool operator< (const fixedbvt &other) const
 
bool operator<= (const fixedbvt &other) const
 
bool operator> (const fixedbvt &other) const
 
bool operator>= (const fixedbvt &other) const
 
bool operator== (const fixedbvt &other) const
 
bool operator!= (const fixedbvt &other) const
 
const mp_integerget_value () const
 
void set_value (const mp_integer &_v)
 

Static Public Member Functions

static fixedbvt zero (const fixedbv_typet &type)
 

Public Attributes

fixedbv_spect spec
 

Protected Attributes

mp_integer v
 

Detailed Description

Definition at line 41 of file fixedbv.h.

Constructor & Destructor Documentation

§ fixedbvt() [1/3]

fixedbvt::fixedbvt ( )
inline

Definition at line 46 of file fixedbv.h.

§ fixedbvt() [2/3]

fixedbvt::fixedbvt ( const fixedbv_spect _spec)
inlineexplicit

Definition at line 50 of file fixedbv.h.

References from_expr(), from_integer(), to_expr(), and to_integer().

§ fixedbvt() [3/3]

fixedbvt::fixedbvt ( const constant_exprt expr)
explicit

Definition at line 21 of file fixedbv.cpp.

References from_expr().

Member Function Documentation

§ format()

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

Definition at line 119 of file fixedbv.cpp.

References integer2string(), format_spect::min_width, and power().

Referenced by format_constantt::operator()().

§ from_expr()

void fixedbvt::from_expr ( const constant_exprt expr)

§ from_integer()

void fixedbvt::from_integer ( const mp_integer i)

Definition at line 32 of file fixedbv.cpp.

References power().

Referenced by interpretert::evaluate(), from_integer(), and simplify_exprt::simplify_typecast().

§ get_value()

const mp_integer& fixedbvt::get_value ( ) const
inline

Definition at line 95 of file fixedbv.h.

Referenced by interpretert::evaluate().

§ is_zero()

bool fixedbvt::is_zero ( ) const
inline

Definition at line 71 of file fixedbv.h.

Referenced by simplify_exprt::simplify_div().

§ negate()

void fixedbvt::negate ( )

Definition at line 87 of file fixedbv.cpp.

Referenced by exprt::negate(), and simplify_exprt::simplify_unary_minus().

§ operator!=()

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

Definition at line 93 of file fixedbv.h.

References v.

§ operator*=()

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

Definition at line 92 of file fixedbv.cpp.

References fixedbv_spect::integer_bits, spec, v, and fixedbv_spect::width.

§ operator+=()

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

§ operator-=()

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

§ operator/=()

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

Definition at line 106 of file fixedbv.cpp.

References fixedbv_spect::get_fraction_bits(), power(), spec, and v.

§ operator<()

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

Definition at line 88 of file fixedbv.h.

References v.

§ operator<=()

bool fixedbvt::operator<= ( const fixedbvt other) const
inline

Definition at line 89 of file fixedbv.h.

References v.

§ operator==() [1/2]

bool fixedbvt::operator== ( int  i) const

Definition at line 114 of file fixedbv.cpp.

References power().

§ operator==() [2/2]

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

Definition at line 92 of file fixedbv.h.

References v.

§ operator>()

bool fixedbvt::operator> ( const fixedbvt other) const
inline

Definition at line 90 of file fixedbv.h.

References v.

§ operator>=()

bool fixedbvt::operator>= ( const fixedbvt other) const
inline

Definition at line 91 of file fixedbv.h.

References v.

§ round()

void fixedbvt::round ( const fixedbv_spect dest_spec)

Definition at line 54 of file fixedbv.cpp.

References fixedbv_spect::integer_bits, power(), and fixedbv_spect::width.

Referenced by simplify_exprt::simplify_typecast().

§ set_value()

void fixedbvt::set_value ( const mp_integer _v)
inline

Definition at line 96 of file fixedbv.h.

Referenced by interpretert::evaluate(), and simplify_exprt::simplify_typecast().

§ to_ansi_c_string()

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

Definition at line 62 of file fixedbv.h.

References operator==().

Referenced by expr2ct::convert_constant(), and xml().

§ to_expr()

§ to_integer()

mp_integer fixedbvt::to_integer ( ) const

Definition at line 37 of file fixedbv.cpp.

References power().

Referenced by simplify_exprt::simplify_typecast().

§ zero()

static fixedbvt fixedbvt::zero ( const fixedbv_typet type)
inlinestatic

Definition at line 76 of file fixedbv.h.

References fixedbv_spect::fixedbv_spect(), and operator-=().

Member Data Documentation

§ spec

§ v

mp_integer fixedbvt::v
protected

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