mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Eliminated reinterpret_casts. Partially fixes #24, #229.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2015-10-04 15:52:20 +01:00
parent c636c87e4d
commit 4626196907
2 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/util/hwf.cpp
View file

@ -85,8 +85,9 @@ hwf_manager::~hwf_manager()
{
}
#define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
#define DBL(X) (*reinterpret_cast<const double*>(&(X)))
// #define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
#define RAW(X) ({ uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); tmp; })
#define DBL(X) ({ double tmp; memcpy(&tmp, &(X), sizeof(double)); tmp; })
void hwf_manager::set(hwf & o, int value) {
o.value = (double) value;
@ -166,7 +167,7 @@ void hwf_manager::set(hwf & o, bool sign, uint64 significand, int exponent) {
uint64 raw = (sign?0x8000000000000000ull:0);
raw |= (((uint64)exponent) + 1023) << 52;
raw |= significand;
o.value = *reinterpret_cast<double*>(&raw);
memcpy(&o.value, &raw, sizeof(double));
}
void hwf_manager::set(hwf & o, hwf const & x) {

10
src/util/mpfx.cpp
View file

@ -199,8 +199,9 @@ void mpfx_manager::set(mpfx & n, uint64 v) {
else {
allocate_if_needed(n);
n.m_sign = 0;
unsigned * _v = reinterpret_cast<unsigned*>(&v);
unsigned * w = words(n);
unsigned * _v = 0;
memcpy(_v, &v, sizeof(unsigned*));
for (unsigned i = 0; i < m_total_sz; i++)
w[i] = 0;
w[m_frac_part_sz] = _v[0];
@ -679,7 +680,8 @@ int64 mpfx_manager::get_int64(mpfx const & n) const {
SASSERT(is_int64(n));
unsigned * w = words(n);
w += m_frac_part_sz;
uint64 r = *reinterpret_cast<uint64*>(w);
uint64 r = 0;
memcpy(&r, w, sizeof(uint64));
if (r == 0x8000000000000000ull) {
SASSERT(is_neg(n));
return INT64_MIN;
@ -693,7 +695,9 @@ uint64 mpfx_manager::get_uint64(mpfx const & n) const {
SASSERT(is_uint64(n));
unsigned * w = words(n);
w += m_frac_part_sz;
return *reinterpret_cast<uint64*>(w);
uint64 r = 0;
memcpy(&r, w, sizeof(uint64));
return r;
}
template<bool SYNCH>