compilation fails with CompCert-3.4 on Linux x86-64; patch proposed

[DAVID MONNIAUX]

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/