cprover
|
#include <fixedbv.h>
Public Member Functions | |
fixedbv_spect () | |
fixedbv_spect (std::size_t _width, std::size_t _integer_bits) | |
fixedbv_spect (const fixedbv_typet &type) | |
std::size_t | get_fraction_bits () const |
Public Attributes | |
std::size_t | integer_bits |
std::size_t | width |
|
inline |
Definition at line 24 of file fixedbv.h.
Referenced by fixedbv_spect(), fixedbvt::from_expr(), and fixedbvt::zero().
|
inline |
Definition at line 28 of file fixedbv.h.
References fixedbv_spect().
|
explicit |
Definition at line 15 of file fixedbv.cpp.
References fixedbv_typet::get_integer_bits(), bitvector_typet::get_width(), integer_bits, and width.
|
inline |
Definition at line 35 of file fixedbv.h.
References integer_bits.
Referenced by smt1_convt::convert_div(), smt2_convt::convert_div(), smt1_convt::convert_mult(), smt2_convt::convert_mult(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), fixedbvt::operator/=(), and simplify_exprt::simplify_typecast().
std::size_t fixedbv_spect::integer_bits |
Definition at line 22 of file fixedbv.h.
Referenced by smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), fixedbv_spect(), get_fraction_bits(), fixedbvt::operator*=(), and fixedbvt::round().
std::size_t fixedbv_spect::width |
Definition at line 22 of file fixedbv.h.
Referenced by smt1_convt::convert_constant(), smt2_convt::convert_constant(), smt1_convt::convert_div(), smt2_convt::convert_div(), smt1_convt::convert_mult(), smt2_convt::convert_mult(), smt1_convt::convert_typecast(), smt2_convt::convert_typecast(), fixedbv_spect(), fixedbvt::operator*=(), and fixedbvt::round().