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

[Vincent Lefevre]

On 2019-01-25 10:38:10 +0100, Niels Möller wrote:
> Vincent Lefevre  writes:
> > The code given by the autoconf manual is:
[...]
> >   # elif !defined HAVE_ALLOCA
> >   #  ifdef  __cplusplus
> >   extern "C"
> >   #  endif
> >   void *alloca (size_t);
> >   # endif
> >   #endif
> 
> The last case, declaring alloca, is that expecting that a replacement
> alloca.c is used as a fallback? As far as I see, we don't do that in
> gmp.

I don't understand this last case. It might also be a bug.
This is what I posted:

  http://lists.gnu.org/archive/html/bug-autoconf/2019-01/msg9.html

-- 
Vincent Lefèvre  - Web: 
100% accessible validated (X)HTML - Blog: 
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
___
gmp-bugs mailing list
gmp-bugs@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-bugs

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

[Niels Möller]

Vincent Lefevre  writes:

> The code given by the autoconf manual is:
>
>   #ifdef STDC_HEADERS
>   # include 
>   # include 
>   #else
>   # ifdef HAVE_STDLIB_H
>   #  include 
>   # endif
>   #endif
>   #ifdef HAVE_ALLOCA_H
>   # include 
>   #elif !defined alloca
>   # ifdef __GNUC__
>   #  define alloca __builtin_alloca
>   # elif defined _AIX
>   #  define alloca __alloca
>   # elif defined _MSC_VER
>   #  include 
>   #  define alloca _alloca
>   # elif !defined HAVE_ALLOCA
>   #  ifdef  __cplusplus
>   extern "C"
>   #  endif
>   void *alloca (size_t);
>   # endif
>   #endif

The last case, declaring alloca, is that expecting that a replacement
alloca.c is used as a fallback? As far as I see, we don't do that in
gmp.

Regards,
/Niels

-- 
Niels Möller. PGP-encrypted email is preferred. Keyid 368C6677.
Internet email is subject to wholesale government surveillance.
___
gmp-bugs mailing list
gmp-bugs@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-bugs

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

[DAVID MONNIAUX]

> I don't think this is correct, as alloca() may be available even
> though HAVE_ALLOCA is not defined (e.g. with MinGW).
But why would you declare alloca() as a function even though you're not going 
to use it (as far as I understand you don't use it if HAVE_ALLOCA is not set)?! 

> void *alloca (size_t);
Ok. The following patch also works for CompCert: 
diff -u -r gmp-6.1.2-orig/gmp-impl.h gmp-6.1.2/gmp-impl.h 
--- gmp-6.1.2-orig/gmp-impl.h 2016-12-16 16:45:27.0 +0100 
+++ gmp-6.1.2/gmp-impl.h 2019-01-24 15:36:04.121087498 +0100 
@@ -207,7 +207,7 @@ 
# if defined (_AIX) || defined (_IBMR2) 
#pragma alloca 
# else 
- char *alloca (); 
+ void *alloca (size_t); 
# endif 
# endif 
# endif 
___
gmp-bugs mailing list
gmp-bugs@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-bugs

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

[Vincent Lefevre]

On 2019-01-24 15:57:13 +0100, DAVID MONNIAUX wrote:
> > I don't think this is correct, as alloca() may be available even
> > though HAVE_ALLOCA is not defined (e.g. with MinGW).
> But why would you declare alloca() as a function even though you're
> not going to use it (as far as I understand you don't use it if
> HAVE_ALLOCA is not set)?!

This is the case where alloca() is defined only as a macro.
With your first patch:

#if HAVE_ALLOCA
...
#endif

with no #else case. Thus platforms that need a "#define alloca ..."
may miss the definition in the case HAVE_ALLOCA is not defined (the
autoconf manual is not clear about its definition).

I agree that

  # elif !defined HAVE_ALLOCA
  #  ifdef  __cplusplus
  extern "C"
  #  endif
  void *alloca (size_t);
  # endif

looks strange. I would have thought that the first line should
have been

  # elif defined HAVE_ALLOCA

Or there is another reason, but the code looks wrong. I've just
reported a bug for clarification.

-- 
Vincent Lefèvre  - Web: 
100% accessible validated (X)HTML - Blog: 
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
___
gmp-bugs mailing list
gmp-bugs@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-bugs

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

[Vincent Lefevre]

On 2019-01-24 08:46:12 +0100, DAVID MONNIAUX wrote:
> Fix: do not declare alloca() unless HAVE_ALLOCA is set (CompCert
> does not have alloca()). Patch below:

I don't think this is correct, as alloca() may be available even
though HAVE_ALLOCA is not defined (e.g. with MinGW).

The code given by the autoconf manual is:

  #ifdef STDC_HEADERS
  # include 
  # include 
  #else
  # ifdef HAVE_STDLIB_H
  #  include 
  # endif
  #endif
  #ifdef HAVE_ALLOCA_H
  # include 
  #elif !defined alloca
  # ifdef __GNUC__
  #  define alloca __builtin_alloca
  # elif defined _AIX
  #  define alloca __alloca
  # elif defined _MSC_VER
  #  include 
  #  define alloca _alloca
  # elif !defined HAVE_ALLOCA
  #  ifdef  __cplusplus
  extern "C"
  #  endif
  void *alloca (size_t);
  # endif
  #endif

(not tested with GMP and/or MPFR, but I had added a FIXME in MPFR
to consider switching to it).

-- 
Vincent Lefèvre  - Web: 
100% accessible validated (X)HTML - Blog: 
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)
___
gmp-bugs mailing list
gmp-bugs@gmplib.org
https://gmplib.org/mailman/listinfo/gmp-bugs

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.0 +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  
-# define alloca _alloca 
+# ifdef __DECC 
+# define alloca(x) __ALLOCA(x) 
# else 
-# if HAVE_ALLOCA_H 
-# include  
+# ifdef _MSC_VER 
+# include  
+# define alloca _alloca 
# else 
-# if defined (_AIX) || defined (_IBMR2) 
- #pragma alloca 
+# if HAVE_ALLOCA_H 
+# include  
# 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