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

Vincent Lefevre vincent at
Thu Jan 24 15:48:08 UTC 2019

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:


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 <vincent at> - Web: <>
100% accessible validated (X)HTML - Blog: <>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)

More information about the gmp-bugs mailing list