From 2912c355e223dd3b49534c1392dae7a5513fdf9e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 4 Oct 2015 10:54:19 -0700
Subject: [PATCH] remove reinterpret_cast. Issue #229, issue #24
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/interp/iz3foci.cpp | 21 ++++++++++-----------
src/muz/pdr/pdr_util.cpp | 2 +-
src/muz/rel/dl_sparse_table.cpp | 2 +-
src/muz/rel/tbv.cpp | 2 +-
src/util/hwf.h | 4 ++--
5 files changed, 15 insertions(+), 16 deletions(-)
diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp
index e0773209b..3a873de2c 100755
--- a/src/interp/iz3foci.cpp
+++ b/src/interp/iz3foci.cpp
@@ -19,7 +19,6 @@
#include <sstream>
#include <iostream>
-#include <assert.h>
#include "iz3hash.h"
#include "foci2.h"
@@ -197,7 +196,7 @@ public:
std::cerr << "iZ3: unsupported Z3 operator in expression\n ";
print_expr(std::cerr,t);
std::cerr << "\n";
- assert(0 && "iZ3: unsupported Z3 operator");
+ SASSERT(0 && "iZ3: unsupported Z3 operator");
}
}
return res;
@@ -272,7 +271,7 @@ public:
}
break;
default:
- assert("unknown built-in op");
+ SASSERT(false && "unknown built-in op");
}
}
else if(foci->get_int(i,nval)){
@@ -280,15 +279,15 @@ public:
}
else if(foci->get_func(i,f)){
if(f == select_op){
- assert(n == 2);
+ SASSERT(n == 2);
res = make(Select,args[0],args[1]);
}
else if(f == store_op){
- assert(n == 3);
+ SASSERT(n == 3);
res = make(Store,args[0],args[1],args[2]);
}
else if(f == mod_op){
- assert(n == 2);
+ SASSERT(n == 2);
res = make(Mod,args[0],args[1]);
}
else {
@@ -298,20 +297,20 @@ public:
if(bar.second){
std::cout << "unknown function symbol:\n";
foci->show_ast(i);
- assert(0);
+ SASSERT(0);
}
res = make(func_decl,args);
}
}
else {
std::cerr << "iZ3: unknown FOCI expression kind\n";
- assert(0 && "iZ3: unknown FOCI expression kind");
+ SASSERT(0 && "iZ3: unknown FOCI expression kind");
}
return res;
}
int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
- assert((int)cnsts.size() == frames);
+ SASSERT((int)cnsts.size() == frames);
std::string lia("lia");
#ifdef _FOCI2
foci = foci2::create(lia);
@@ -320,7 +319,7 @@ public:
#endif
if(!foci){
std::cerr << "iZ3: cannot find foci lia solver.\n";
- assert(0);
+ SASSERT(0);
}
select_op = foci->mk_func("select");
store_op = foci->mk_func("store");
@@ -335,7 +334,7 @@ public:
}
int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents);
if(res == 0){
- assert((int)foci_itps.size() == frames-1);
+ SASSERT((int)foci_itps.size() == frames-1);
itps.resize(frames-1);
for(int i = 0; i < frames-1; i++){
// foci->show_ast(foci_itps[i]);
diff --git a/src/muz/pdr/pdr_util.cpp b/src/muz/pdr/pdr_util.cpp
index f8758d997..9af3ea8b4 100644
--- a/src/muz/pdr/pdr_util.cpp
+++ b/src/muz/pdr/pdr_util.cpp
@@ -73,7 +73,7 @@ namespace pdr {
}
std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) {
- return pp_cube(sz, reinterpret_cast<expr * const *>(lits), m);
+ return pp_cube(sz, (expr * const *)(lits), m);
}
std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {
diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index 2c806971f..24fda3e96 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -293,7 +293,7 @@ namespace datalog {
void key_to_reserve(const key_value & key) const {
m_keys.ensure_reserve();
- m_keys.write_into_reserve(reinterpret_cast<char *>(key.c_ptr()));
+ m_keys.write_into_reserve((char *)(key.c_ptr()));
}
offset_vector & get_matching_offset_vector(const key_value & key) {
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 6e030a823..568f63f51 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -43,7 +43,7 @@ void tbv_manager::reset() {
m.reset();
}
tbv* tbv_manager::allocate() {
- tbv* r = reinterpret_cast<tbv*>(m.allocate());
+ tbv* r = static_cast<tbv*>(m.allocate());
DEBUG_CODE(
if (s_debug_alloc) {
TRACE("doc", tout << allocated_tbvs.size() << " " << r << "\n";);
diff --git a/src/util/hwf.h b/src/util/hwf.h
index 7b17553d2..d2055d56e 100644
--- a/src/util/hwf.h
+++ b/src/util/hwf.h
@@ -131,11 +131,11 @@ public:
return (x.get_raw() & 0x8000000000000000ull) != 0;
}
- const uint64 sig(hwf const & x) const {
+ uint64 sig(hwf const & x) const {
return x.get_raw() & 0x000FFFFFFFFFFFFFull;
}
- const int exp(hwf const & x) const {
+ int exp(hwf const & x) const {
return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023;
}