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

2019-01-25 Thread 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); > >

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

2019-01-25 Thread 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

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

2019-01-24 Thread 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

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

2019-01-24 Thread 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

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

2019-01-24 Thread 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

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

2019-01-24 Thread 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