Download raw body.
math/z3: update to 4.13.3; taken mantainership
ports@,
Here an update for math/z3 to the last version which includes patch to fix
building under clang.
I've increased SHARE_LIBS version because include files was changes.
And I've also would like to take care of this port.
Changes:
- https://github.com/Z3Prover/z3/releases/tag/z3-4.13.1
- https://github.com/Z3Prover/z3/releases/tag/z3-4.13.2
- https://github.com/Z3Prover/z3/releases/tag/z3-4.13.3
Tested on -current/amd64.
The diff:
Index: Makefile
===================================================================
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.34
diff -u -p -r1.34 Makefile
--- Makefile 3 Sep 2024 17:48:45 -0000 1.34
+++ Makefile 12 Oct 2024 15:28:11 -0000
@@ -1,13 +1,15 @@
COMMENT = Z3 theorem prover
-DIST_TUPLE = github Z3Prover z3 z3-4.13.0 .
+DIST_TUPLE = github Z3Prover z3 z3-4.13.3 .
PKGNAME = ${DISTNAME:S/z3-//}
-SHARED_LIBS = z3 4.11
+SHARED_LIBS = z3 4.12
CATEGORIES = math
WANTLIB += c m pthread ${COMPILER_LIBCXX}
+
+MAINTAINER = Kirill A. Korinsky <kirill@korins.ky>
# MIT
PERMIT_PACKAGE = Yes
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.15
diff -u -p -r1.15 distinfo
--- distinfo 3 Sep 2024 17:48:45 -0000 1.15
+++ distinfo 12 Oct 2024 15:28:11 -0000
@@ -1,2 +1,2 @@
-SHA256 (Z3Prover-z3-z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
-SIZE (Z3Prover-z3-z3-4.13.0.tar.gz) = 5520232
+SHA256 (Z3Prover-z3-z3-4.13.3.tar.gz) = 9Zyc9gDqV/tk/+/7/9Dy0riWhU8znoRvSPBp0jvBS6A=
+SIZE (Z3Prover-z3-z3-4.13.3.tar.gz) = 5583533
Index: patches/patch-src_util_memory_manager_cpp
===================================================================
RCS file: patches/patch-src_util_memory_manager_cpp
diff -N patches/patch-src_util_memory_manager_cpp
--- patches/patch-src_util_memory_manager_cpp 3 Sep 2024 17:48:45 -0000 1.1
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,111 +0,0 @@
-https://github.com/Z3Prover/z3/issues/6902
-Index: src/util/memory_manager.cpp
---- src/util/memory_manager.cpp.orig
-+++ src/util/memory_manager.cpp
-@@ -29,6 +29,8 @@ Copyright (c) 2015 Microsoft Corporation
- # define malloc_usable_size _msize
- #endif
-
-+#define SIZE_T_ALIGN 2
-+
- // The following two function are automatically generated by the mk_make.py script.
- // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
- // For example, rational.h contains
-@@ -278,7 +280,7 @@ void memory::deallocate(void * p) {
- size_t sz = malloc_usable_size(p);
- void * real_p = p;
- #else
-- size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
-+ size_t * sz_p = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
- size_t sz = *sz_p;
- void * real_p = reinterpret_cast<void*>(sz_p);
- #endif
-@@ -291,7 +293,7 @@ void memory::deallocate(void * p) {
-
- void * memory::allocate(size_t s) {
- #ifndef HAS_MALLOC_USABLE_SIZE
-- s = s + sizeof(size_t); // we allocate an extra field!
-+ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
- #endif
- g_memory_thread_alloc_size += s;
- g_memory_thread_alloc_count += 1;
-@@ -308,7 +310,7 @@ void * memory::allocate(size_t s) {
- return r;
- #else
- *(static_cast<size_t*>(r)) = s;
-- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
- #endif
- }
-
-@@ -320,10 +322,10 @@ void* memory::reallocate(void *p, size_t s) {
- if (sz >= s)
- return p;
- #else
-- size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
-+ size_t *sz_p = reinterpret_cast<size_t*>(p)-SIZE_T_ALIGN;
- size_t sz = *sz_p;
- void *real_p = reinterpret_cast<void*>(sz_p);
-- s = s + sizeof(size_t); // we allocate an extra field!
-+ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
- #endif
- g_memory_thread_alloc_size += s - sz;
- g_memory_thread_alloc_count += 1;
-@@ -341,7 +343,7 @@ void* memory::reallocate(void *p, size_t s) {
- return r;
- #else
- *(static_cast<size_t*>(r)) = s;
-- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
- #endif
- }
-
-@@ -358,7 +360,7 @@ void memory::deallocate(void * p) {
- size_t sz = malloc_usable_size(p);
- void * real_p = p;
- #else
-- size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
-+ size_t * sz_p = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
- size_t sz = *sz_p;
- void * real_p = reinterpret_cast<void*>(sz_p);
- #endif
-@@ -368,7 +370,7 @@ void memory::deallocate(void * p) {
-
- void * memory::allocate(size_t s) {
- #ifndef HAS_MALLOC_USABLE_SIZE
-- s = s + sizeof(size_t); // we allocate an extra field!
-+ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
- #endif
- g_memory_alloc_size += s;
- g_memory_alloc_count += 1;
-@@ -389,7 +391,7 @@ void * memory::allocate(size_t s) {
- return r;
- #else
- *(static_cast<size_t*>(r)) = s;
-- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
- #endif
- }
-
-@@ -401,10 +403,10 @@ void* memory::reallocate(void *p, size_t s) {
- if (sz >= s)
- return p;
- #else
-- size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
-+ size_t * sz_p = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
- size_t sz = *sz_p;
- void * real_p = reinterpret_cast<void*>(sz_p);
-- s = s + sizeof(size_t); // we allocate an extra field!
-+ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
- #endif
- g_memory_alloc_size += s - sz;
- g_memory_alloc_count += 1;
-@@ -425,7 +427,7 @@ void* memory::reallocate(void *p, size_t s) {
- return r;
- #else
- *(static_cast<size_t*>(r)) = s;
-- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
-+ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
- #endif
- }
-
--
wbr, Kirill
math/z3: update to 4.13.3; taken mantainership