mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

revert the patch to remove no-strict-aliasing

Browse source 
VS 2012 doesnt support C++11 unions..
This commit is contained in:
Nuno Lopes 2017-08-14 23:00:59 +01:00
parent 197aefd111
commit 4b00bc636b
5 changed files with 49 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

51
src/util/optional.h
View file

@ -23,35 +23,32 @@ Revision History:
template<typename T>
class optional {
union {
T m_obj;
char m_dummy;
};
bool m_initialized;
char m_obj[sizeof(T)];
char m_initialized;
void construct(const T & val) {
m_initialized = true;
new (&m_obj) T(val);
m_initialized = 1;
new (reinterpret_cast<void *>(m_obj)) T(val);
}
void destroy() {
if (m_initialized) {
m_obj.~T();
if (m_initialized == 1) {
reinterpret_cast<T *>(m_obj)->~T();
}
m_initialized = false;
m_initialized = 0;
}
public:
optional():
m_initialized(false) {}
m_initialized(0) {}
explicit optional(const T & val) {
construct(val);
}
optional(const optional<T> & val):
m_initialized(false) {
if (val.m_initialized) {
m_initialized(0) {
if (val.m_initialized == 1) {
construct(*val);
}
}
@ -62,13 +59,13 @@ public:
static optional const & undef() { static optional u; return u; }
bool initialized() const { return m_initialized; }
operator bool() const { return m_initialized; }
bool operator!() const { return !m_initialized; }
bool initialized() const { return m_initialized == 1; }
operator bool() const { return m_initialized == 1; }
bool operator!() const { return m_initialized == 0; }
T * get() const {
if (m_initialized) {
return &m_obj;
if (m_initialized == 1) {
return reinterpret_cast<T *>(m_obj);
}
else {
return 0;
@ -76,29 +73,29 @@ public:
}
void set_invalid() {
if (m_initialized) {
if (m_initialized == 1) {
destroy();
}
}
T * operator->() {
SASSERT(m_initialized);
return &m_obj;
SASSERT(m_initialized==1);
return reinterpret_cast<T *>(m_obj);
}
T const * operator->() const {
SASSERT(m_initialized);
return &m_obj;
SASSERT(m_initialized==1);
return reinterpret_cast<T const *>(m_obj);
}
const T & operator*() const {
SASSERT(m_initialized);
return m_obj;
SASSERT(m_initialized==1);
return *reinterpret_cast<T const*>(m_obj);
}
T & operator*() {
SASSERT(m_initialized);
return m_obj;
SASSERT(m_initialized==1);
return *reinterpret_cast<T *>(m_obj);
}
optional & operator=(const T & val) {