CBMC
|
#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.
std::string fixedbvt::format | ( | const format_spect & | format_spec | ) | const |
Definition at line 134 of file fixedbv.cpp.
void fixedbvt::from_expr | ( | const constant_exprt & | expr | ) |
Definition at line 26 of file fixedbv.cpp.
void fixedbvt::from_integer | ( | const mp_integer & | i | ) |
Definition at line 32 of file fixedbv.cpp.
|
inline |
void fixedbvt::negate | ( | ) |
Definition at line 90 of file fixedbv.cpp.
|
inline |
Definition at line 95 of file fixedbv.cpp.
Definition at line 109 of file fixedbv.cpp.
Definition at line 115 of file fixedbv.cpp.
Definition at line 121 of file fixedbv.cpp.
|
inline |
|
inline |
|
inline |
bool fixedbvt::operator== | ( | int | i | ) | const |
Definition at line 129 of file fixedbv.cpp.
|
inline |
|
inline |
void fixedbvt::round | ( | const fixedbv_spect & | dest_spec | ) |
Definition at line 52 of file fixedbv.cpp.
|
inline |
constant_exprt fixedbvt::to_expr | ( | ) | const |
Definition at line 43 of file fixedbv.cpp.
mp_integer fixedbvt::to_integer | ( | ) | const |
Definition at line 37 of file fixedbv.cpp.
|
inlinestatic |
fixedbv_spect fixedbvt::spec |
|
protected |