mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 07:23:58 +00:00
Code Activity

fix gcc compiler warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-05-16 12:04:10 +01:00
commit 5632900f35
9 changed files with 23 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

15
scripts/mk_util.py
View file

@ -1746,7 +1746,6 @@ def mk_config():
'OBJ_EXT=.obj\n' 'OBJ_EXT=.obj\n'
'LIB_EXT=.lib\n' 'LIB_EXT=.lib\n'
'AR=lib\n' 'AR=lib\n'
'AR_FLAGS=/nologo /LTCG\n'
'AR_OUTFLAG=/OUT:\n' 'AR_OUTFLAG=/OUT:\n'
'EXE_EXT=.exe\n' 'EXE_EXT=.exe\n'
'LINK=cl\n' 'LINK=cl\n'
@ -1765,23 +1764,25 @@ def mk_config():
extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) extra_opt = ' %s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH)
if DEBUG_MODE: if DEBUG_MODE:
config.write( config.write(
'AR_FLAGS=/nologo\n'
'LINK_FLAGS=/nologo /MDd\n' 'LINK_FLAGS=/nologo /MDd\n'
'SLINK_FLAGS=/nologo /LDd\n') 'SLINK_FLAGS=/nologo /LDd\n')
if not VS_X64: if not VS_X64:
config.write( config.write(
'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt) 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2\n' % extra_opt)
config.write( config.write(
'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else: else:
config.write( config.write(
'CXXFLAGS=/c /GL /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt) 'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _AMD64_ /D _DEBUG /D Z3DEBUG %s /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze-\n' % extra_opt)
config.write( config.write(
'LINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n' 'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT\n'
'SLINK_EXTRA_FLAGS=/link /LTCG /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n') 'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE:NO\n')
else: else:
# Windows Release mode # Windows Release mode
config.write( config.write(
'AR_FLAGS=/nologo /LTCG\n'
'LINK_FLAGS=/nologo /MD\n' 'LINK_FLAGS=/nologo /MD\n'
'SLINK_FLAGS=/nologo /LD\n') 'SLINK_FLAGS=/nologo /LD\n')
if TRACE: if TRACE:

3
src/math/polynomial/upolynomial_factorization.cpp
View file

@ -719,12 +719,11 @@ void hensel_lift_quadratic(z_manager& upm, numeral_vector const & C,
// we create a new Z_p manager, since we'll be changing the input one // we create a new Z_p manager, since we'll be changing the input one
zp_manager zp_upm(nm); zp_manager zp_upm(nm);
zp_upm.set_zp(zpe_upm.m().p()); zp_upm.set_zp(zpe_upm.m().p());
zp_numeral_manager & zp_nm = zp_upm.m();
// get the U, V, such that A*U + B*V = 1 (mod p) // get the U, V, such that A*U + B*V = 1 (mod p)
scoped_mpz_vector U(nm), V(nm), D(nm); scoped_mpz_vector U(nm), V(nm), D(nm);
zp_upm.ext_gcd(A.size(), A.c_ptr(), B.size(), B.c_ptr(), U, V, D); zp_upm.ext_gcd(A.size(), A.c_ptr(), B.size(), B.c_ptr(), U, V, D);
SASSERT(D.size() == 1 && zp_nm.is_one(D[0])); SASSERT(D.size() == 1 && zp_upm.m().is_one(D[0]));
// we start lifting from (a = p, b = p, r = p) // we start lifting from (a = p, b = p, r = p)
scoped_mpz_vector A_lifted(nm), B_lifted(nm); scoped_mpz_vector A_lifted(nm), B_lifted(nm);

4
src/muz/fp/datalog_parser.cpp
View file

@ -89,8 +89,8 @@ public:
:m_eof(false), :m_eof(false),
m_eof_behind_buffer(false), m_eof_behind_buffer(false),
m_next_index(0), m_next_index(0),
m_data_size(0), m_ok(true),
m_ok(true) { m_data_size(0) {
m_data.resize(2*s_expansion_step); m_data.resize(2*s_expansion_step);
resize_data(0); resize_data(0);
#if _WINDOWS #if _WINDOWS

5
src/muz/pdr/pdr_context.cpp
View file

@ -150,9 +150,9 @@ namespace pdr {
} }
datalog::rule const& pred_transformer::find_rule(model_core const& model) const { datalog::rule const& pred_transformer::find_rule(model_core const& model) const {
datalog::rule_manager& rm = ctx.get_context().get_rule_manager();
obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end(); obj_map<expr, datalog::rule const*>::iterator it = m_tag2rule.begin(), end = m_tag2rule.end();
TRACE("pdr_verbose", TRACE("pdr_verbose",
datalog::rule_manager& rm = ctx.get_context().get_rule_manager();
for (; it != end; ++it) { for (; it != end; ++it) {
expr* pred = it->m_key; expr* pred = it->m_key;
tout << mk_pp(pred, m) << ":\n"; tout << mk_pp(pred, m) << ":\n";
@ -1137,9 +1137,6 @@ namespace pdr {
if (n->get_model_ptr()) { if (n->get_model_ptr()) {
models.insert(n->state(), n->get_model_ptr()); models.insert(n->state(), n->get_model_ptr());
rules.insert(n->state(), n->get_rule()); rules.insert(n->state(), n->get_rule());
//pred_transformer& pt = n->pt();
//context& ctx = pt.get_context();
//datalog::context& dctx = ctx.get_context();
} }
todo.pop_back(); todo.pop_back();
todo.append(n->children().size(), n->children().c_ptr()); todo.append(n->children().size(), n->children().c_ptr());

1
src/opt/opt_context.cpp
View file

@ -1343,7 +1343,6 @@ namespace opt {
break; break;
} }
case O_MAXSMT: { case O_MAXSMT: {
maxsmt& ms = *m_maxsmts.find(obj.m_id);
rational value(0); rational value(0);
for (unsigned i = 0; i < obj.m_terms.size(); ++i) { for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
VERIFY(m_model->eval(obj.m_terms[i], val)); VERIFY(m_model->eval(obj.m_terms[i], val));

2
src/opt/opt_solver.cpp
View file

@ -41,9 +41,9 @@ namespace opt {
m_params(p), m_params(p),
m_context(mgr, m_params), m_context(mgr, m_params),
m(mgr), m(mgr),
m_dump_benchmarks(false),
m_fm(fm), m_fm(fm),
m_objective_sorts(m), m_objective_sorts(m),
m_dump_benchmarks(false),
m_first(true) { m_first(true) {
m_params.updt_params(p); m_params.updt_params(p);
m_params.m_relevancy_lvl = 0; m_params.m_relevancy_lvl = 0;

1
src/tactic/nlsat_smt/nl_purify_tactic.cpp
View file

@ -631,7 +631,6 @@ public:
m(m), m(m),
m_util(m), m_util(m),
m_params(p), m_params(p),
m_produce_proofs(false),
m_fmc(0), m_fmc(0),
m_cancel(false), m_cancel(false),
m_nl_tac(mk_nlsat_tactic(m, p)), m_nl_tac(mk_nlsat_tactic(m, p)),

5
src/util/inf_rational.h
View file

@ -63,10 +63,7 @@ class inf_rational {
return s; return s;
} }
inf_rational(): inf_rational() {}
m_first(rational()),
m_second(rational())
{}
inf_rational(const inf_rational & r): inf_rational(const inf_rational & r):
m_first(r.m_first), m_first(r.m_first),

12
src/util/rational.cpp
View file

@ -24,9 +24,9 @@ Revision History:
#endif #endif
synch_mpq_manager * rational::g_mpq_manager = 0; synch_mpq_manager * rational::g_mpq_manager = 0;
rational rational::m_zero(0); rational rational::m_zero;
rational rational::m_one(1); rational rational::m_one;
rational rational::m_minus_one(-1); rational rational::m_minus_one;
vector<rational> rational::m_powers_of_two; vector<rational> rational::m_powers_of_two;
void mk_power_up_to(vector<rational> & pws, unsigned n) { void mk_power_up_to(vector<rational> & pws, unsigned n) {
@ -56,11 +56,17 @@ rational rational::power_of_two(unsigned k) {
void rational::initialize() { void rational::initialize() {
if (!g_mpq_manager) { if (!g_mpq_manager) {
g_mpq_manager = alloc(synch_mpq_manager); g_mpq_manager = alloc(synch_mpq_manager);
m().set(m_zero.m_val, 0);
m().set(m_one.m_val, 1);
m().set(m_minus_one.m_val, -1);
} }
} }
void rational::finalize() { void rational::finalize() {
m_powers_of_two.finalize(); m_powers_of_two.finalize();
m_zero.~rational();
m_one.~rational();
m_minus_one.~rational();
dealloc(g_mpq_manager); dealloc(g_mpq_manager);
g_mpq_manager = 0; g_mpq_manager = 0;
} }