Hi, GMP-6.1.2 fails to compile with CompCert (compcert.inria.fr) on Linux x86-64. The reason is that one of the header files in GMP declares alloca() with a prototype that conflicts with the one in the system headers.
Steps to reproduce: $ CC=/opt/CompCert/3.4/x86_64-linux/bin/ccomp CFLAGS="-O3 -Wall -fall" ../gmp-6.1.2-old/configure --disable-shared $ make ../../gmp-6.1.2-old/gmp-impl.h:210: error: redefinition of 'alloca' with a different type: 'void *(size_t __size)' vs 'char *()' 1 error detected. Makefile:448: recipe for target 'set_str.lo' failed Fix: do not declare alloca() unless HAVE_ALLOCA is set (CompCert does not have alloca()). Patch below: diff -u -r gmp-6.1.2-old/gmp-impl.h gmp-6.1.2/gmp-impl.h --- gmp-6.1.2-old/gmp-impl.h 2016-12-16 16:45:27.000000000 +0100 +++ gmp-6.1.2/gmp-impl.h 2019-01-24 07:45:26.742693456 +0100 @@ -190,24 +190,26 @@ from gmp.h. */ -#ifndef alloca -# ifdef __GNUC__ -# define alloca __builtin_alloca -# else -# ifdef __DECC -# define alloca(x) __ALLOCA(x) +#if HAVE_ALLOCA +# ifndef alloca +# ifdef __GNUC__ +# define alloca __builtin_alloca # else -# ifdef _MSC_VER -# include <malloc.h> -# define alloca _alloca +# ifdef __DECC +# define alloca(x) __ALLOCA(x) # else -# if HAVE_ALLOCA_H -# include <alloca.h> +# ifdef _MSC_VER +# include <malloc.h> +# define alloca _alloca # else -# if defined (_AIX) || defined (_IBMR2) - #pragma alloca +# if HAVE_ALLOCA_H +# include <alloca.h> # else - char *alloca (); +# if defined (_AIX) || defined (_IBMR2) + #pragma alloca +# else + char *alloca (); +# endif # endif # endif # endif @@ -215,7 +217,6 @@ # endif #endif - /* if not provided by gmp-mparam.h */ #ifndef GMP_LIMB_BYTES #define GMP_LIMB_BYTES SIZEOF_MP_LIMB_T Cheers Directeur de recherche au CNRS, laboratoire VERIMAG, équipe PACSS http://www-verimag.imag.fr/~monniaux/ _______________________________________________ gmp-bugs mailing list gmp-bugs@gmplib.org https://gmplib.org/mailman/listinfo/gmp-bugs