diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index 82f08f42c40a25637bc37961e5811a4a122d3bbc..612984ff008a8fc15c050e5506c4396d3e7600cc 100644 --- a/src/plugins/e-acsl/.gitignore +++ b/src/plugins/e-acsl/.gitignore @@ -74,4 +74,5 @@ doc/doxygen/doxygen.cfg doc/doxygen/html doc/doxygen/warn.log benchmarking/tools/fc-time -contrib/jemalloc/include/jemalloc/jemalloc-e-acsl.h +lib/libgmp-e-acsl.a +lib/libjemalloc-e-acsl.a diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 3f38a160d1c680f48407dfc6fa7334509cdd3bb4..57f4369c4261c0a233b23fe05edf46c9a59da5de 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -46,6 +46,7 @@ endif ######################### PLUGIN_DIR ?=. +PLUGIN_LIB = $(PLUGIN_DIR)/lib PLUGIN_ENABLE:=@ENABLE_E_ACSL@ PLUGIN_DYNAMIC:=@DYNAMIC_E_ACSL@ PLUGIN_NAME:=E_ACSL @@ -144,41 +145,34 @@ clean:: # E-ACSL C Libs: libjemalloc, libgmp # ################################################ JEMALLOC_DIR = $(PLUGIN_DIR)/contrib/libjemalloc -JEMALLOC_LIBDIR = $(JEMALLOC_DIR)/lib JEMALLOC_LIBNAME = libjemalloc-e-acsl.a -EACSL_JEMALLOC_LIB = $(JEMALLOC_LIBDIR)/$(JEMALLOC_LIBNAME) +JEMALLOC_LIB = $(PLUGIN_LIB)/$(JEMALLOC_LIBNAME) -PUBLIC_PREFIX = "__e_acsl_native_" # Prefix of public jemalloc functions -PRIVATE_PREFIX = "__e_acsl_hidden_" # Suffix of private jemalloc functions -INSTALL_SUFFIX = "-e-acsl" # Suffix of generated jemalloc library - -$(EACSL_JEMALLOC_LIB): +$(JEMALLOC_LIB): cd $(JEMALLOC_DIR) && \ ./autogen.sh \ - --with-jemalloc-prefix="$(PUBLIC_PREFIX)" \ - --with-private-namespace="$(PRIVATE_PREFIX)" \ - --with-install-suffix="$(INSTALL_SUFFIX)" && \ + --with-jemalloc-prefix="__e_acsl_native_" \ + --with-private-namespace="__e_acsl_hidden_" \ + --with-install-suffix="-e-acsl" && \ $(MAKE) $(MAKEOPTS) lib/$(JEMALLOC_LIBNAME) + $(CP) $(JEMALLOC_DIR)/lib/$(JEMALLOC_LIBNAME) $@ GMP_DIR = $(PLUGIN_DIR)/contrib/libgmp -GMP_LIBDIR = $(GMP_DIR) GMP_LIBNAME = libgmp-e-acsl.a +GMP_LIB = $(PLUGIN_LIB)/$(GMP_LIBNAME) -EACSL_GMP_LIB = $(GMP_LIBDIR)/$(GMP_LIBNAME) - -$(EACSL_GMP_LIB): +$(GMP_LIB): cd $(GMP_DIR) && ./configure && $(MAKE) $(MAKEOPTS) - $(CP) $(GMP_DIR)/.libs/libgmp.a $(EACSL_GMP_LIB) + $(CP) $(GMP_DIR)/.libs/libgmp.a $@ -all:: $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB) +all:: $(JEMALLOC_LIB) $(GMP_LIB) clean:: $(PRINT_RM) e-acsl contrib libraries - $(RM) $(EACSL_JEMALLOC_LIB) + $(RM) $(JEMALLOC_LIB) $(GMP_LIB) if test -f $(JEMALLOC_DIR)/Makefile; \ then $(MAKE) -C$(JEMALLOC_DIR) distclean; \ fi - $(RM) $(EACSL_GMP_LIB) if test -f $(GMP_DIR)/Makefile; \ then $(MAKE) -C$(GMP_DIR) distclean; \ fi @@ -298,8 +292,8 @@ install:: $(FRAMAC_DATADIR)/manuals $(PRINT_INSTALL) E-ACSL libraries $(MKDIR) $(LIBDIR) - $(CP) $(EACSL_JEMALLOC_LIB) $(LIBDIR) - $(CP) $(EACSL_GMP_LIB) $(LIBDIR) + $(CP) $(JEMALLOC_LIB) $(LIBDIR) + $(CP) $(GMP_LIB) $(LIBDIR) $(PRINT_INSTALL) E-ACSL scripts $(MKDIR) $(BINDIR) $(CP) $(E_ACSL_DIR)/scripts/e-acsl-gcc.sh $(BINDIR)/ diff --git a/src/plugins/e-acsl/contrib/.gitignore b/src/plugins/e-acsl/contrib/.gitignore index 043b27ae2b6988c62c4faf790739cb5726bb8caf..6d926c47eaf8fa76bf33358a2410a63f2b5d256e 100644 --- a/src/plugins/e-acsl/contrib/.gitignore +++ b/src/plugins/e-acsl/contrib/.gitignore @@ -789,3 +789,4 @@ libgmp/tests/rand/Makefile libgmp/trialdivtab.h libgmp/tune/Makefile libgmp/tune/sqr_basecase.c +libjemalloc/include/jemalloc/jemalloc-e-acsl.h diff --git a/src/plugins/e-acsl/lib/.gitkeep b/src/plugins/e-acsl/lib/.gitkeep new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 7d76f35b53c42cc1245982c95bf6910647b0e0de..d1d6f74a66a3213666f301da545c85caa03262b5 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -113,6 +113,8 @@ Notes: # Base dir of this script BASEDIR="$(readlink -f `dirname $0`)" +# Directory with contrib libraries of E-ACSL +LIBDIR="$BASEDIR/../lib" # See if pygmentize if available for color highlighting and default to plain # cat command otherwise @@ -328,10 +330,6 @@ FRAMAC="$OPTION_FRAMAC" FRAMAC_SHARE="`$FRAMAC -print-share-path`" FRAMAC_PLUGIN="`$FRAMAC -print-plugin-path`" -# Name of the malloc library to use -LIBJEMALLOC="libjemalloc-e-acsl.a" -LIBGMP="libgmp-e-acsl.a" - # Check if this is a development or an installed version if [ -f "$BASEDIR/../E_ACSL.mli" ]; then # Development version @@ -346,14 +344,10 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then # Add the project directory to FRAMAC_PLUGINS, # otherwise Frama-C uses an installed version FRAMAC_FLAGS="-add-path=$DEVELOPMENT $FRAMAC_FLAGS" - LIBJEMALLOC="$BASEDIR/../contrib/libjemalloc/lib/$LIBJEMALLOC" - LIBGMP="$BASEDIR/../contrib/libgmp/libgmp-e-acsl.a" else # Installed version. FRAMAC_SHARE should not be used here as Frama-C # and E-ACSL may not be installed to the same location EACSL_SHARE="$BASEDIR/../share/frama-c/e-acsl/" - LIBJEMALLOC="$BASEDIR/../lib/$LIBJEMALLOC" - LIBGMP="$BASEDIR/../lib/$LIBGMP" fi # Architecture-dependent flags. Since by default Frama-C uses 32-bit @@ -450,9 +444,8 @@ LDFLAGS="$OPTION_LDFLAGS" EACSL_CFLAGS="" EACSL_CPPFLAGS=" -I$EACSL_SHARE - -D$EACSL_MACRO_ID - -D__FC_errno=(*__errno_location())" -EACSL_LDFLAGS="$LIBGMP -lm $LIBJEMALLOC -lpthread" + -D$EACSL_MACRO_ID" +EACSL_LDFLAGS="-lm $LIBDIR/libgmp-e-acsl.a $LIBDIR/libjemalloc-e-acsl.a -lpthread" # Output file names OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source