mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

remove reinterpret cast occurrences that require disabling strict alias analysis #987 #1210

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-17 20:28:49 -07:00
parent 43c2ccb29a
commit ff47c8632b
5 changed files with 24 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast.cpp
View file

@ -35,7 +35,7 @@ Revision History:
parameter::~parameter() {
if (m_kind == PARAM_RATIONAL) {
reinterpret_cast<rational *>(m_rational)->~rational();
dealloc(m_rational);
}
}
@ -50,14 +50,14 @@ parameter& parameter::operator=(parameter const& other) {
return *this;
}
if (m_kind == PARAM_RATIONAL) {
reinterpret_cast<rational *>(m_rational)->~rational();
dealloc(m_rational);
}
m_kind = other.m_kind;
switch(other.m_kind) {
case PARAM_INT: m_int = other.get_int(); break;
case PARAM_AST: m_ast = other.get_ast(); break;
case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break;
case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break;
case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
case PARAM_RATIONAL: m_rational = alloc(rational, other.get_rational()); break;
case PARAM_DOUBLE: m_dval = other.m_dval; break;
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
default:

16
src/ast/ast.h
View file

@ -102,8 +102,8 @@ private:
union {
int m_int; // for PARAM_INT
ast* m_ast; // for PARAM_AST
char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL
char m_rational[sizeof(rational)]; // for PARAM_RATIONAL
void const* m_symbol; // for PARAM_SYMBOL
rational* m_rational; // for PARAM_RATIONAL
double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin)
unsigned m_ext_id; // for PARAM_EXTERNAL
};
@ -114,12 +114,10 @@ public:
explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {}
explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {}
explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {}
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); }
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); }
explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {}
explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {}
explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL) {
new (m_symbol) symbol(s);
}
explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {}
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
parameter(parameter const&);
@ -156,8 +154,8 @@ public:
int get_int() const { SASSERT(is_int()); return m_int; }
ast * get_ast() const { SASSERT(is_ast()); return m_ast; }
symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast<const symbol *>(m_symbol)); }
rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast<const rational *>(m_rational)); }
symbol get_symbol() const { SASSERT(is_symbol()); return symbol::mk_symbol_from_c_ptr(m_symbol); }
rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; }
double get_double() const { SASSERT(is_double()); return m_dval; }
unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; }

6
src/muz/spacer/spacer_sym_mux.cpp
View file

@ -32,10 +32,8 @@ using namespace spacer;
sym_mux::sym_mux(ast_manager & m, const std::vector<std::string> & suffixes)
: m(m), m_ref_holder(m), m_next_sym_suffix_idx(0), m_suffixes(suffixes)
{
unsigned suf_sz = m_suffixes.size();
for (unsigned i = 0; i < suf_sz; ++i) {
symbol suff_sym = symbol(m_suffixes[i].c_str());
m_used_suffixes.insert(suff_sym);
for (std::string const& s : m_suffixes) {
m_used_suffixes.insert(symbol(s.c_str()));
}
}

5
src/util/array_map.h
View file

@ -63,10 +63,7 @@ class array_map {
}
void really_flush() {
typename vector<optional<entry> >::iterator it = m_map.begin();
typename vector<optional<entry> >::iterator end = m_map.end();
for (; it != end; ++it) {
optional<entry> & e = *it;
for (optional<entry> & e : m_map) {
if (e) {
m_plugin.del_eh(e->m_key, e->m_data);
e.set_invalid();

19
src/util/optional.h
View file

@ -23,24 +23,25 @@ Revision History:
template<typename T>
class optional {
char m_obj[sizeof(T)];
T* m_obj;
char m_initialized;
void construct(const T & val) {
m_initialized = 1;
new (reinterpret_cast<void *>(m_obj)) T(val);
m_obj = alloc(T, val);
}
void destroy() {
if (m_initialized == 1) {
reinterpret_cast<T *>(m_obj)->~T();
dealloc(m_obj);
m_obj = 0;
}
m_initialized = 0;
}
public:
optional():
m_initialized(0) {}
m_obj(0), m_initialized(0) {}
explicit optional(const T & val) {
construct(val);
@ -65,7 +66,7 @@ public:
T * get() const {
if (m_initialized == 1) {
return reinterpret_cast<T *>(m_obj);
return m_obj;
}
else {
return 0;
@ -80,22 +81,22 @@ public:
T * operator->() {
SASSERT(m_initialized==1);
return reinterpret_cast<T *>(m_obj);
return m_obj;
}
T const * operator->() const {
SASSERT(m_initialized==1);
return reinterpret_cast<T const *>(m_obj);
return m_obj;
}
const T & operator*() const {
SASSERT(m_initialized==1);
return *reinterpret_cast<T const*>(m_obj);
return *m_obj;
}
T & operator*() {
SASSERT(m_initialized==1);
return *reinterpret_cast<T *>(m_obj);
return *m_obj;
}
optional & operator=(const T & val) {