From e22a67c12c23923a93ea46256f43087e2bce5b8c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Nov 2016 15:27:46 +0000 Subject: [PATCH 1/5] Whitespace --- src/api/z3_replayer.cpp | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 651cb730f..56f6d7bb6 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -14,7 +14,7 @@ Author: Leonardo de Moura (leonardo) 2011-09-22 Notes: - + --*/ #include"vector.h" #include"map.h" @@ -76,13 +76,13 @@ struct z3_replayer::imp { } if (m_args[pos].m_kind != k) { std::stringstream strm; - strm << "expecting " << kind2string(k) << " at position " + strm << "expecting " << kind2string(k) << " at position " << pos << " but got " << kind2string(m_args[pos].m_kind); throw z3_replayer_exception(strm.str().c_str()); } } - struct value { + struct value { value_kind m_kind; union { __int64 m_int; @@ -129,7 +129,7 @@ struct z3_replayer::imp { break; case DOUBLE: out << v.m_double; - break; + break; case STRING: out << v.m_str; break; @@ -160,7 +160,7 @@ struct z3_replayer::imp { char curr() const { return m_curr; } void new_line() { m_line++; } void next() { m_curr = m_stream.get(); } - + void read_string_core(char delimiter) { if (curr() != delimiter) throw z3_replayer_exception("invalid string/symbol"); @@ -258,7 +258,7 @@ struct z3_replayer::imp { } bool is_double_char() const { - return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E'; + return curr() == '-' || curr() == '.' || ('0' <= curr() && curr() <= '9') || curr() == 'e' || curr() == 'E'; } #if (!defined(strtof)) @@ -376,7 +376,7 @@ struct z3_replayer::imp { } } else if (k == OBJECT) { - TRACE("z3_replayer_bug", + TRACE("z3_replayer_bug", tout << "args: "; display_args(tout); tout << "\n"; tout << "push_back, sz: " << sz << ", m_obj_arrays.size(): " << m_obj_arrays.size() << "\n"; for (unsigned i = asz - sz; i < asz; i++) { @@ -421,7 +421,7 @@ struct z3_replayer::imp { break; case 'R': // reset - next(); + next(); TRACE("z3_replayer", tout << "[" << m_line << "] " << "R\n";); reset(); break; @@ -432,7 +432,7 @@ struct z3_replayer::imp { if (m_ptr == 0) { m_args.push_back(0); } - else { + else { void * obj = 0; if (!m_heap.find(m_ptr, obj)) throw z3_replayer_exception("invalid pointer"); @@ -493,7 +493,7 @@ struct z3_replayer::imp { next(); skip_blank(); read_double(); TRACE("z3_replayer", tout << "[" << m_line << "] " << "D " << m_double << "\n";); m_args.push_back(value(DOUBLE, m_double)); - break; + break; case 'p': case 's': case 'u': @@ -696,15 +696,15 @@ struct z3_replayer::imp { m_unsigned_arrays.reset(); m_int_arrays.reset(); } - - + + }; z3_replayer::z3_replayer(std::istream & in) { m_imp = alloc(imp, *this, in); register_z3_replayer_cmds(*this); } - + z3_replayer::~z3_replayer() { dealloc(m_imp); } From 1188e6df47f3d284910313911bf9e95a326abc23 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 8 Nov 2016 15:28:20 +0000 Subject: [PATCH 2/5] Typo --- src/api/z3_replayer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 56f6d7bb6..277fedb4a 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -72,7 +72,7 @@ struct z3_replayer::imp { void check_arg(unsigned pos, value_kind k) const { if (pos >= m_args.size()) { TRACE("z3_replayer", tout << "too few arguments " << m_args.size() << " expecting " << kind2string(k) << "\n";); - throw z3_replayer_exception("invalid argument reference2"); + throw z3_replayer_exception("invalid argument reference"); } if (m_args[pos].m_kind != k) { std::stringstream strm; From b47c67dee3df0502e8bb5a61b6a2e60ac9a379d6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 21:15:43 +0000 Subject: [PATCH 3/5] Bugfix for Z3_fpa_get_numeral_*_uint64. Relates to #570. --- src/api/api_fpa.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 5d423c725..a039de63c 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -968,6 +968,10 @@ extern "C" { Z3_TRY; LOG_Z3_fpa_get_numeral_significand_uint64(c, t, n); RESET_ERROR_CODE(); + if (n == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); @@ -1028,6 +1032,10 @@ extern "C" { Z3_TRY; LOG_Z3_fpa_get_numeral_exponent_int64(c, t, n); RESET_ERROR_CODE(); + if (n == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); family_id fid = mk_c(c)->get_fpa_fid(); From ca81e803cbd2524741be48ea9d27d1cb647842dd Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Nov 2016 21:33:42 +0000 Subject: [PATCH 4/5] Bugfix for Z3_fpa_get_numeral_sign. Relates to #570. --- src/api/api_fpa.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index a039de63c..8e122ff01 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -909,6 +909,10 @@ extern "C" { Z3_TRY; LOG_Z3_fpa_get_numeral_sign(c, t, sgn); RESET_ERROR_CODE(); + if (sgn == 0) { + SET_ERROR_CODE(Z3_INVALID_ARG); + return 0; + } ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); From 2df5a4e3f9df926b5d29eab0b5aaddbe4827aeb3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 12 Nov 2016 15:01:54 +0000 Subject: [PATCH 5/5] typo --- src/api/z3_replayer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 277fedb4a..e5fbf5720 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -30,7 +30,7 @@ void register_z3_replayer_cmds(z3_replayer & in); void throw_invalid_reference() { TRACE("z3_replayer", tout << "invalid argument reference\n";); - throw z3_replayer_exception("invalid argument reference1"); + throw z3_replayer_exception("invalid argument reference"); } struct z3_replayer::imp {