mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

#7117

Browse source 
probably overflow of unsigned for large capacity
This commit is contained in:
Nikolaj Bjorner 2024-02-14 17:08:09 +07:00
parent 155dfb10c4
commit 2b14793213
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/util/chashtable.h
View file

@ -161,8 +161,12 @@ protected:
unsigned curr_cellar = (m_capacity - m_slots);
unsigned new_slots = m_slots * 2;
unsigned new_cellar = curr_cellar * 2;
if (new_slots < m_slots || new_cellar < curr_cellar)
throw default_exception("table overflow");
while (true) {
unsigned new_capacity = new_slots + new_cellar;
if (new_capacity < new_slots)
throw default_exception("table overflow");
cell * new_table = alloc_table(new_capacity);
cell * next_cell = copy_table(m_table, m_slots, m_capacity,
new_table, new_slots, new_capacity,
@ -179,6 +183,8 @@ protected:
return;
}
dealloc_vect(new_table, new_capacity);
if (2*new_cellar < new_cellar)
throw default_exception("table overflow");
new_cellar *= 2;
}
}