compilation fails with CompCert-3.4 on Linux x86-64; patch proposed
david.monniaux at univ-grenoble-alpes.fr
Thu Jan 24 14:57:13 UTC 2019
> 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 (size_t);
Ok. The following patch also works for CompCert:
diff -u -r gmp-6.1.2-orig/gmp-impl.h gmp-6.1.2/gmp-impl.h
--- gmp-6.1.2-orig/gmp-impl.h 2016-12-16 16:45:27.000000000 +0100
+++ gmp-6.1.2/gmp-impl.h 2019-01-24 15:36:04.121087498 +0100
@@ -207,7 +207,7 @@
# if defined (_AIX) || defined (_IBMR2)
- char *alloca ();
+ void *alloca (size_t);
More information about the gmp-bugs