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);
> >
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
>
> 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="