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