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

fix boundary case according to analysis #477, e.g., size = 252, PTR_ALIGNMENT=2, slot_id = 64 = NUM_SLOTS

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-09 00:42:50 -08:00
parent 5db84575f6
commit 71fff8ffa2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/small_object_allocator.cpp
View file

@ -77,7 +77,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
SASSERT(m_alloc_size >= size); SASSERT(m_alloc_size >= size);
SASSERT(p); SASSERT(p);
m_alloc_size -= size; m_alloc_size -= size;
if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) { if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
memory::deallocate(p); memory::deallocate(p);
return; return;
} }
@ -96,7 +96,7 @@ void * small_object_allocator::allocate(size_t size) {
return memory::allocate(size); return memory::allocate(size);
#endif #endif
m_alloc_size += size; m_alloc_size += size;
if (size > SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
return memory::allocate(size); return memory::allocate(size);
#ifdef Z3DEBUG #ifdef Z3DEBUG
size_t osize = size; size_t osize = size;