cprover
|
#include <fixedbv.h>
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 () |
fixedbvt & | operator/= (const fixedbvt &other) |
fixedbvt & | operator*= (const fixedbvt &other) |
fixedbvt & | operator+= (const fixedbvt &other) |
fixedbvt & | operator-= (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_integer & | get_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 |
|
inlineexplicit |
|
explicit |
Definition at line 21 of file fixedbv.cpp.
References from_expr().
std::string fixedbvt::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 119 of file fixedbv.cpp.
References fixedbv_spect::get_fraction_bits(), integer2string(), format_spect::min_width, power(), spec, and v.
Referenced by format_constantt::operator()(), and to_ansi_c_string().
void fixedbvt::from_expr | ( | const constant_exprt & | expr | ) |
Definition at line 26 of file fixedbv.cpp.
References binary2integer(), constant_exprt::get_value(), id2string(), spec, to_fixedbv_type(), exprt::type(), and v.
Referenced by interpretert::evaluate(), and fixedbvt().
void fixedbvt::from_integer | ( | const mp_integer & | i | ) |
Definition at line 32 of file fixedbv.cpp.
References fixedbv_spect::get_fraction_bits(), power(), spec, and v.
Referenced by interpretert::evaluate(), from_integer(), and simplify_exprt::simplify_typecast().
|
inline |
|
inline |
Definition at line 71 of file fixedbv.h.
References v.
Referenced by simplify_exprt::simplify_div().
void fixedbvt::negate | ( | ) |
Definition at line 87 of file fixedbv.cpp.
References v.
Referenced by exprt::negate(), and simplify_exprt::simplify_unary_minus().
|
inline |
Definition at line 92 of file fixedbv.cpp.
References fixedbv_spect::integer_bits, round(), spec, v, and fixedbv_spect::width.
Definition at line 106 of file fixedbv.cpp.
References fixedbv_spect::get_fraction_bits(), power(), spec, and v.
|
inline |
|
inline |
bool fixedbvt::operator== | ( | int | i | ) | const |
Definition at line 114 of file fixedbv.cpp.
References fixedbv_spect::get_fraction_bits(), power(), spec, and v.
|
inline |
|
inline |
|
inline |
void fixedbvt::round | ( | const fixedbv_spect & | dest_spec | ) |
Definition at line 54 of file fixedbv.cpp.
References fixedbv_spect::integer_bits, power(), spec, v, and fixedbv_spect::width.
Referenced by operator*=(), and simplify_exprt::simplify_typecast().
|
inline |
Definition at line 96 of file fixedbv.h.
References v.
Referenced by interpretert::evaluate(), and simplify_exprt::simplify_typecast().
|
inline |
Definition at line 62 of file fixedbv.h.
References format().
Referenced by expr2ct::convert_constant(), and xml().
constant_exprt fixedbvt::to_expr | ( | ) | const |
Definition at line 43 of file fixedbv.cpp.
References integer2binary(), fixedbv_spect::integer_bits, fixedbv_typet::set_integer_bits(), constant_exprt::set_value(), bitvector_typet::set_width(), spec, v, and fixedbv_spect::width.
Referenced by from_integer(), exprt::mul(), exprt::negate(), simplify_exprt::simplify_div(), simplify_exprt::simplify_typecast(), and simplify_exprt::simplify_unary_minus().
mp_integer fixedbvt::to_integer | ( | ) | const |
Definition at line 37 of file fixedbv.cpp.
References fixedbv_spect::get_fraction_bits(), power(), spec, and v.
Referenced by simplify_exprt::simplify_typecast().
|
inlinestatic |
Definition at line 76 of file fixedbv.h.
References fixedbvt().
fixedbv_spect fixedbvt::spec |
Definition at line 44 of file fixedbv.h.
Referenced by interpretert::evaluate(), format(), from_expr(), from_integer(), from_integer(), operator*=(), operator/=(), operator==(), round(), simplify_exprt::simplify_typecast(), to_expr(), and to_integer().
|
protected |
Definition at line 100 of file fixedbv.h.
Referenced by format(), from_expr(), from_integer(), get_value(), is_zero(), negate(), operator!=(), operator*=(), operator/=(), operator<(), operator<=(), operator==(), operator>(), operator>=(), round(), set_value(), to_expr(), and to_integer().