diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index a1efed19e..f347a8e49 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -35,7 +35,7 @@ Revision History: parameter::~parameter() { if (m_kind == PARAM_RATIONAL) { - reinterpret_cast(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(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: diff --git a/src/ast/ast.h b/src/ast/ast.h index 3a3f08df2..e6beec7e6 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -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(m_symbol)); } - rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast(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; } diff --git a/src/muz/spacer/spacer_sym_mux.cpp b/src/muz/spacer/spacer_sym_mux.cpp index da8f8eeca..c311d9990 100644 --- a/src/muz/spacer/spacer_sym_mux.cpp +++ b/src/muz/spacer/spacer_sym_mux.cpp @@ -32,10 +32,8 @@ using namespace spacer; sym_mux::sym_mux(ast_manager & m, const std::vector & 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())); } } diff --git a/src/util/array_map.h b/src/util/array_map.h index c5163715e..f3f99d015 100644 --- a/src/util/array_map.h +++ b/src/util/array_map.h @@ -63,10 +63,7 @@ class array_map { } void really_flush() { - typename vector >::iterator it = m_map.begin(); - typename vector >::iterator end = m_map.end(); - for (; it != end; ++it) { - optional & e = *it; + for (optional & e : m_map) { if (e) { m_plugin.del_eh(e->m_key, e->m_data); e.set_invalid(); diff --git a/src/util/optional.h b/src/util/optional.h index 22757f3bd..eeff35260 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -23,24 +23,25 @@ Revision History: template class optional { - char m_obj[sizeof(T)]; + T* m_obj; char m_initialized; void construct(const T & val) { m_initialized = 1; - new (reinterpret_cast(m_obj)) T(val); + m_obj = alloc(T, val); } void destroy() { if (m_initialized == 1) { - reinterpret_cast(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(m_obj); + return m_obj; } else { return 0; @@ -80,22 +81,22 @@ public: T * operator->() { SASSERT(m_initialized==1); - return reinterpret_cast(m_obj); + return m_obj; } T const * operator->() const { SASSERT(m_initialized==1); - return reinterpret_cast(m_obj); + return m_obj; } const T & operator*() const { SASSERT(m_initialized==1); - return *reinterpret_cast(m_obj); + return *m_obj; } T & operator*() { SASSERT(m_initialized==1); - return *reinterpret_cast(m_obj); + return *m_obj; } optional & operator=(const T & val) {