diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h index 0ada2c250542..4b88e8b1a342 100644 --- a/src/include/lean/lean.h +++ b/src/include/lean/lean.h @@ -380,16 +380,11 @@ static inline unsigned lean_small_object_size(lean_object * o) { void free(void *); // avoid including big `stdlib.h` #endif -#if !defined(__STDC_VERSION_STDLIB_H__) || __STDC_VERSION_STDLIB_H__ < 202311L -void free_sized(void* ptr, size_t); -#endif - static inline void lean_free_small_object(lean_object * o) { #ifdef LEAN_SMALL_ALLOCATOR lean_free_small(o); #else - size_t* ptr = (size_t*)o - 1; - free_sized(ptr, *ptr + sizeof(size_t)); + free((size_t*)o - 1); #endif } diff --git a/src/library/module.cpp b/src/library/module.cpp index 77a7ea3bcc8c..91d65d22db0c 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -213,7 +213,7 @@ extern "C" LEAN_EXPORT object * lean_read_module_data(object * fname, object *) #endif buffer = static_cast(malloc(size - sizeof(olean_header))); free_data = [=]() { - free_sized(buffer, size - sizeof(olean_header)); + free(buffer); }; in.read(buffer, size - sizeof(olean_header)); if (!in) { diff --git a/src/runtime/alloc.cpp b/src/runtime/alloc.cpp index 38b3e3070275..6ac4804e5eaf 100644 --- a/src/runtime/alloc.cpp +++ b/src/runtime/alloc.cpp @@ -437,7 +437,7 @@ void dealloc(void * o, size_t sz) { LEAN_RUNTIME_STAT_CODE(g_num_dealloc++); sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA); if (LEAN_UNLIKELY(sz > LEAN_MAX_SMALL_OBJECT_SIZE)) { - return free_sized(o, sz); + return free(o); } dealloc_small_core(o); } diff --git a/src/runtime/buffer.h b/src/runtime/buffer.h index c3d4ecb72ebf..14facc8b08b7 100644 --- a/src/runtime/buffer.h +++ b/src/runtime/buffer.h @@ -27,11 +27,7 @@ class buffer { void free_memory() { if (m_buffer != reinterpret_cast(m_initial_buffer)) - #if __cpp_sized_deallocation >= 201309L - operator delete[](reinterpret_cast(m_buffer), sizeof(T) * m_capacity); - #else - delete[] reinterpret_cast(m_buffer); - #endif + delete[] reinterpret_cast(m_buffer); } void set_capacity(size_t new_capacity) { diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index cec3d073cffb..2bb6d81b630f 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -41,12 +41,6 @@ Author: Leonardo de Moura #define isinf(x) std::isinf(x) #endif -#if !defined(__STDC_VERSION_STDLIB_H__) || __STDC_VERSION_STDLIB_H__ < 202311L -extern "C" __attribute__((weak)) void free_sized(void *ptr, size_t) { - free(ptr); -} -#endif - // see `Task.Priority.max` #define LEAN_MAX_PRIO 8 @@ -204,7 +198,7 @@ static inline void lean_dealloc(lean_object * o, size_t sz) { #ifdef LEAN_SMALL_ALLOCATOR dealloc(o, sz); #else - free_sized(o, sz); + free(o); #endif }