mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix crash in qe_array ref counting due to wrong assignment operator of ptr_vector being called

Browse source 
thanks to Arie Gurfinkel for reporting this
This commit is contained in:
Nuno Lopes 2020-06-09 10:02:27 +01:00
parent 5f9973d8c4
commit ec1e733ef2
3 changed files with 2 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/qe/qe_arrays.cpp
View file

@ -967,7 +967,7 @@ namespace qe {
else {
r.reset();
}
rs.push_back(r);
rs.push_back(std::move(r));
}
return rs;
}

5
src/util/ref_vector.h
View file

@ -327,10 +327,7 @@ public:
// prevent abuse:
ref_vector & operator=(ref_vector const & other) = delete;
ref_vector & operator=(ref_vector && other) {
super::operator=(std::move(other));
return *this;
}
ref_vector & operator=(ref_vector && other) = default;
bool operator==(ref_vector const& other) const {
if (other.size() != this->size()) return false;

12
src/util/vector.h
View file

@ -587,13 +587,7 @@ public:
ptr_vector():vector<T *, false>() {}
ptr_vector(unsigned s):vector<T *, false>(s) {}
ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
ptr_vector(ptr_vector && other) noexcept : vector<T*, false>(std::move(other)) {}
ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
ptr_vector & operator=(ptr_vector const & source) {
vector<T *, false>::operator=(source);
return *this;
}
};
template<typename T, typename SZ = unsigned>
@ -602,13 +596,7 @@ public:
svector():vector<T, false, SZ>() {}
svector(SZ s):vector<T, false, SZ>(s) {}
svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
svector(svector const & source):vector<T, false, SZ>(source) {}
svector(svector && other) noexcept : vector<T, false, SZ>(std::move(other)) {}
svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
svector & operator=(svector const & source) {
vector<T, false, SZ>::operator=(source);
return *this;
}
};