CBMC
|
#include <fixedbv.h>
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.
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.
Definition at line 129 of file fixedbv.cpp.
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 |