From 0433a5d28b90e13c6a9a63e204c03f9fca61e502 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Mon, 22 Aug 2016 17:05:09 +0200
Subject: [PATCH] --enable-full-gmp option in configure to switch between
 portable distribution of the GMP library (mini-gmp) and the full GMP library
 at build time

---
 src/plugins/e-acsl/Makefile.in  | 19 ++++++++++++++++++-
 src/plugins/e-acsl/configure.ac |  8 ++++++++
 2 files changed, 26 insertions(+), 1 deletion(-)

diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 74a0fbf8092..a20ffddc2b3 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -167,14 +167,31 @@ $(EACSL_JEMALLOC_LIB):
 	$(MKDIR) $(EACSL_LIBDIR)
 	$(CP) $(EACSL_JEMALLOC_DIR)/lib/$(EACSL_JEMALLOC_LIBNAME) $@
 
-EACSL_GMP_DIR := $(PLUGIN_DIR)/contrib/libgmp
+
 EACSL_GMP_LIBNAME = libgmp-e-acsl.a
 EACSL_GMP_LIB = $(EACSL_LIBDIR)/$(EACSL_GMP_LIBNAME)
+EACSL_GMP_DIR := $(PLUGIN_DIR)/contrib/libgmp
+EACSL_GMP_MINI = mini-gmp.o
 
+ifeq (@FULL_GMP@, no)
+############
+# Mini GMP #
+############
+$(EACSL_GMP_LIB): $(EACSL_GMP_DIR)/mini-gmp/mini-gmp.c
+	echo 'CC          $< '
+	$(CC) $< -c -O2 -g3 -o$(EACSL_GMP_MINI)
+	echo 'AR          $@'
+	$(AR) crus $(EACSL_GMP_LIB) $(EACSL_GMP_MINI)
+	ranlib $(EACSL_GMP_LIB)
+else
+############
+# Full GMP #
+############
 $(EACSL_GMP_LIB):
 	cd $(EACSL_GMP_DIR) && ./configure && $(MAKE) $(MAKEOPTS)
 	$(MKDIR) $(EACSL_LIBDIR)
 	$(CP) $(EACSL_GMP_DIR)/.libs/libgmp.a $@
+endif
 
 all:: $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
 
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index 9424a1e4eae..dd8cb6c01ca 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -103,11 +103,19 @@ AC_CHECK_PROG(DOXYGEN,doxygen,doxygen,no)
 AC_CHECK_PROG(HAVE_DOT,dot,yes,no)
 AC_OUTPUT(PLUGIN_RELATIVE_PATH(doc/doxygen/doxygen.cfg), [  ])
 
+# GMP
+#####
+AC_ARG_ENABLE(full-gmp,
+    AS_HELP_STRING([--enable-full-gmp],
+    ["Disable runtime assertions in the RTL"]),
+    [FULL_GMP="yes"],[FULL_GMP="no"])
+
 #######################
 # Generating Makefile #
 #######################
 
 AC_SUBST(MAY_RUN_TESTS)
 AC_SUBST(OCAMLVERSION)
+AC_SUBST(FULL_GMP)
 
 write_plugin_config(Makefile)
-- 
GitLab