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

[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 the autoconf manual is:

          #ifdef STDC_HEADERS
          # include <stdlib.h>
          # include <stddef.h>
          #else
          # ifdef HAVE_STDLIB_H
          #  include <stdlib.h>
          # endif
          #endif
          #ifdef HAVE_ALLOCA_H
          # include <alloca.h>
          #elif !defined alloca
          # ifdef __GNUC__
          #  define alloca __builtin_alloca
          # elif defined _AIX
          #  define alloca __alloca
          # elif defined _MSC_VER
          #  include <malloc.h>
          #  define alloca _alloca
          # elif !defined HAVE_ALLOCA
          #  ifdef  __cplusplus
          extern "C"
          #  endif
          void *alloca (size_t);
          # endif
          #endif

(not tested with GMP and/or MPFR, but I had added a FIXME in MPFR
to consider switching to it).

-- 
Vincent Lefèvre <vincent at vinc17.net> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)