From 8d67681ec63f0e632bd17c08e11f47e12e3a7dd3 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 3 Aug 2016 11:16:18 +0200
Subject: [PATCH] [Makefile] Added --enable-optimized-rtl option to the
configure script. This option allows to specify debug or production build of
E-ACSL runtime library.
---
src/plugins/e-acsl/Makefile.in | 11 +++++++++--
src/plugins/e-acsl/configure.ac | 11 +++++++++--
src/plugins/e-acsl/doc/Changelog | 1 +
3 files changed, 19 insertions(+), 4 deletions(-)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 9646bad6a6e..61b9ea700c1 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -180,8 +180,15 @@ e-acsl-distclean::
################################################
EACSL_SHARE := $(EACSL_PLUGIN_DIR)/share/e-acsl
-RTLFAGS := -std=c99 -Wall -Wno-unused -Wno-attributes -I$(EACSL_SHARE) \
- -g3 -O2 -fno-omit-frame-pointer -DE_ACSL_DEBUG -DE_ACSL_BUILTINS
+
+RTLFAGS = -std=c99 -Wall -Wno-unused -Wno-attributes -I$(EACSL_SHARE) \
+ -fno-omit-frame-pointer -DE_ACSL_BUILTINS
+
+ifeq (@OPTIMIZED_RTL@,no)
+RTLFAGS += -DE_ACSL_DEBUG -g3 -O0
+else
+RTLFAGS += -O3
+endif
# Build a static library
# $1 Compile-time flags
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index c1f310d918f..586e1c0b5f1 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -110,10 +110,18 @@ AC_ARG_ENABLE(full-gmp,
["Disable runtime assertions in the RTL"]),
[FULL_GMP="yes"],[FULL_GMP="no"])
+# RTL
+#####
+AC_ARG_ENABLE(optimized-rtl,
+ AS_HELP_STRING([--enable-optimized-rtl],
+ ["Disable runtime assertions in the RTL"]),
+ [OPTIMIZED_RTL="yes"],[OPTIMIZED_RTL="no"])
+
#######################
# Generating Makefile #
#######################
+AC_SUBST(OPTIMIZED_RTL)
AC_SUBST(MAY_RUN_TESTS)
AC_SUBST(OCAMLVERSION)
AC_SUBST(FULL_GMP)
@@ -138,5 +146,4 @@ fi
AC_MSG_NOTICE([Configure libjemalloc])
(cd plugin_dir/contrib/libjemalloc && ./autogen.sh \
--with-jemalloc-prefix="__e_acsl_native_" \
- --with-private-namespace="__e_acsl_hidden_" \
- --with-install-suffix="-e-acsl")
+ --with-private-namespace="__e_acsl_hidden_")
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 06bf83df0a3..995c81193f6 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,7 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+-* E-ACSL [2016/08/02] Added --enable-optimized-rtl option to configure
-* E-ACSL [2016/08/02] Removed --production|-P, --no-stdlib|-N and
--debug-log|-D options of e-acsl-gcc.sh.
-* E-ACSL [2016/07/21] Enable reporting of stack traces during assertion
--
GitLab