mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

fix issue #57: undefined behavior in bit_vector.h

Browse source
This commit is contained in:
Nuno Lopes 2015-05-10 22:30:07 +00:00
parent eae4d4e0df
commit 6645358fed
1 changed files with 8 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/bit_vector.h
View file

@ -75,8 +75,11 @@ public:
bit_vector(bit_vector const & source):
m_num_bits(source.m_num_bits),
m_capacity(source.m_capacity),
m_data(alloc_svect(unsigned, source.m_capacity)) {
memcpy(m_data, source.m_data, source.m_capacity * sizeof(unsigned));
m_data(0) {
if (source.m_data) {
m_data = alloc_svect(unsigned, m_capacity);
memcpy(m_data, source.m_data, m_capacity * sizeof(unsigned));
}
}
bit_vector(unsigned const * source, int num_bits):
@ -183,6 +186,9 @@ public:
bool operator!=(bit_vector const & other) const { return !operator==(other); }
bit_vector & operator=(bit_vector const & source) {
if (!source.m_data)
return *this;
m_num_bits = source.m_num_bits;
if (m_capacity < source.m_capacity) {
dealloc_svect(m_data);