> 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 (
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 d
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 th
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="