mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

play nice with sanitizers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-03 17:39:22 -07:00
parent 6f65051f2c
commit f4472927c0
5 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/macros/quasi_macros.h
View file

@ -65,7 +65,6 @@ public:
/**
\brief Find pure function macros and apply them.
*/
// bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
bool operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
bool operator()(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector & deps);

7
src/util/mpq.h
View file

@ -136,10 +136,17 @@ public:
void del(mpz & a) { mpz_manager<SYNCH>::del(a); }
void del(mpq & a) {
del(a.m_num);
del(a.m_den);
}
static void del(mpq_manager* m, mpq & a) {
mpz_manager<SYNCH>::del(m, a.m_num);
mpz_manager<SYNCH>::del(m, a.m_den);
}
void get_numerator(mpq const & a, mpz & n) { set(n, a.m_num); }

5
src/util/mpz.cpp
View file

@ -230,9 +230,10 @@ mpz_manager<SYNCH>::sign_cell::sign_cell(mpz_manager& m, mpz const& a):
template<bool SYNCH>
void mpz_manager<SYNCH>::del(mpz & a) {
void mpz_manager<SYNCH>::del(mpz_manager<SYNCH>* m, mpz & a) {
if (a.m_ptr) {
deallocate(a.m_owner == mpz_self, a.m_ptr);
SASSERT(m);
m->deallocate(a.m_owner == mpz_self, a.m_ptr);
a.m_ptr = nullptr;
a.m_kind = mpz_small;
a.m_owner = mpz_self;

4
src/util/mpz.h
View file

@ -401,7 +401,9 @@ public:
static mpz mk_z(int val) { return mpz(val); }
void del(mpz & a);
void del(mpz & a) { del(this, a); }
static void del(mpz_manager* m, mpz & a);
void add(mpz const & a, mpz const & b, mpz & c);

2
src/util/rational.h
View file

@ -63,7 +63,7 @@ public:
struct ui64 {};
rational(uint64_t i, ui64) { m().set(m_val, i); }
~rational() { m().del(m_val); }
~rational() { synch_mpq_manager::del(g_mpq_manager, m_val); }
mpq const & to_mpq() const { return m_val; }