Merge branch 'kostyantyn/feature/release' into 'master'

A few fixes before 0.7 release

See merge request !98

src/plugins/e-acsl/.gitignore

@@ -73,7 +73,7 @@ doc/doxygen/html
 doc/doxygen/warn.log
 lib/libeacsl-jemalloc.a
 lib/libeacsl-gmp.a
-lib/libeacsl-bittree-rtl-opt.a
-lib/libeacsl-segment-rtl-opt.a
-lib/libeacsl-bittree-rtl-debug.a
-lib/libeacsl-segment-rtl-debug.a
+lib/libeacsl-rtl-bittree.a
+lib/libeacsl-rtl-segment.a
+lib/libeacsl-rtl-bittree-dbg.a
+lib/libeacsl-rtl-segment-dbg.a

src/plugins/e-acsl/Makefile.in

@@ -189,39 +189,38 @@ RTLFLAGS = -std=c99 -Wall -Wno-unused -Wno-attributes -I$(EACSL_SHARE) \
 RTLOPT 	 = $(RTLFLAGS) -O2
 RTLDEBUG = $(RTLFLAGS) -DE_ACSL_DEBUG -g3 -O0
 
-# Build a static library
+# Build a static E-ACSL library
   # $1 Compile-time flags
   # $2 Library path
-  # $3 Source files
+  # $3 Source file
 MKRTL = \
-	echo "Making $2"; \
+  echo "Making $2"; \
   object=$$(basename -s .a $2).o && \
   echo ' CC $3' && \
   $(CC) $1 -c -o$$object $3 && \
+  (cd $(EACSL_LIBDIR) && $(AR) -x $(EACSL_GMP_LIBNAME)) && \
+  (cd $(EACSL_LIBDIR) && $(AR) -x $(EACSL_JEMALLOC_LIBNAME)) && \
   echo ' AR $2' && \
-  $(AR) crus $2 $$object && \
-  $(RM) -f $$object && \
+  $(AR) crus $2 $$object $(EACSL_LIBDIR)/*.o && \
+  $(RM) -f $$object $(EACSL_LIBDIR)/*.o && \
   ranlib $2
 
-$(EACSL_LIBDIR)/libeacsl-%-rtl-opt.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC)
-	$(call MKRTL, $(RTLOPT),$@,$<,Optimized bittree)
+$(EACSL_LIBDIR)/libeacsl-rtl-%.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC) $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
+	$(call MKRTL, $(RTLOPT), $@, $<)
 
-$(EACSL_LIBDIR)/libeacsl-%-rtl-debug.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC)
-	$(call MKRTL,$(RTLDEBUG),$@,$<,debug)
+$(EACSL_LIBDIR)/libeacsl-rtl-%-dbg.a: $(EACSL_SHARE)/%_model/e_acsl_*_mmodel.c $(EACSL_RTL_SRC) $(EACSL_JEMALLOC_LIB) $(EACSL_GMP_LIB)
+	$(call MKRTL, $(RTLDEBUG), $@, $<)
 
 EACSL_RTL = \
-	$(EACSL_LIBDIR)/libeacsl-bittree-rtl-opt.a \
-	$(EACSL_LIBDIR)/libeacsl-bittree-rtl-debug.a
-
-ifneq ($(wildcard $(EACSL_SHARE)/segment_model),)
-EACSL_RTL += \
-	$(EACSL_LIBDIR)/libeacsl-segment-rtl-opt.a \
-	$(EACSL_LIBDIR)/libeacsl-segment-rtl-debug.a
-endif
+	$(EACSL_LIBDIR)/libeacsl-rtl-bittree.a \
+	$(EACSL_LIBDIR)/libeacsl-rtl-segment.a \
+	$(EACSL_LIBDIR)/libeacsl-rtl-bittree-dbg.a \
+	$(EACSL_LIBDIR)/libeacsl-rtl-segment-dbg.a
 
 clean::
 	$(PRINT_RM) E-ACSL runtime library
 	$(RM) $(EACSL_RTL)
+	$(RM) $(EACSL_LIBDIR)/*.o
 
 all:: $(EACSL_RTL)
 

src/plugins/e-acsl/scripts/e-acsl-gcc.sh

@@ -153,26 +153,31 @@ rte_options() {
 #    model. In this case the following function prints the full path to a static
 #    library representing this memory model.
 mmodel_lib() {
-  local rt_feature="opt"
+  local rtfeature=""
   if [ -n "$OPTION_RT_DEBUG" ]; then
-    rt_feature="debug"
+    rtfeature="-dbg"
     OPTION_CFLAGS="$OPTION_CFLAGS -O0 -fno-omit-frame-pointer"
   else
     OPTION_CFLAGS="$OPTION_CFLAGS -O2"
   fi
 
-  local models="$(find $LIBDIR/ -name 'libeacsl-*-rtl-opt.a' -exec basename {} \; \
-    | sed 's/^libeacsl-\(.*\)-rtl-opt.a/\1/')"
+  # Supported models
+  local models="segment bittree"
 
   if [ -n "$1" ]; then
     local modelname="$(echo $models | tr ' ' '\n' | grep "^$1$")"
-    local modelpath="$(realpath $LIBDIR/libeacsl-$modelname-rtl-$rt_feature.a 2>/dev/null)"
+    local modelpath="$(realpath $LIBDIR/libeacsl-rtl-$modelname$rtfeature.a 2>/dev/null)"
 
-    if [ -n "$modelpath" ]; then
-      echo $modelpath
-    else
-      error "Memory model '$1'-$rt_feature is not available in this distribution"
+    # Bail if the name of the specified memory model does not match any of the
+    # supported ones
+    if [ -z "$modelname" ]; then
+      error "Memory model '$1' is not available in this distribution"
+    fi
+    # Bail if the library for a specified memory model is not found
+    if [ -z "$modelpath" ]; then
+      error "Library '$modelpath' not found"
     fi
+    echo $modelpath
   else
     echo $models
   fi
@@ -445,6 +450,11 @@ do
 done
 shift;
 
+# Bail if no files to translate are given
+if [ -z "$1" ]; then
+  error "no input files";
+fi
+
 # Check Frama-C and GCC executable names
 check_tool "$OPTION_FRAMAC"
 check_tool "$OPTION_CC"
@@ -505,13 +515,14 @@ fi
 
 # Once EACSL_SHARE is defined check the memory models provided at inputs
 for mod in $OPTION_EACSL_MMODELS; do
-  mmodel_lib $mod
+  mmodel_lib $mod >/dev/null
 done
 
 # Gcc and related flags
 CC="$OPTION_CC"
 CFLAGS="$OPTION_CFLAGS
-  -std=c99 $GCCMACHDEP -g3 -fno-builtin -fno-merge-constants
+  -std=c99 $GCCMACHDEP -g3
+  -fno-builtin -fno-merge-constants
   -Wall \
   -Wno-long-long \
   -Wno-attributes \
@@ -538,13 +549,10 @@ fi
 CPPFLAGS="$OPTION_CPPFLAGS"
 LDFLAGS="$OPTION_LDFLAGS"
 
-LIBGMP="$(realpath $LIBDIR/libeacsl-jemalloc.a)"
-LIBJEMALLOC="$(realpath $LIBDIR/libeacsl-gmp.a)"
-
 # C, CPP and LD flags for compilation of E-ACSL-generated sources
 EACSL_CFLAGS=""
 EACSL_CPPFLAGS="-I$EACSL_SHARE"
-EACSL_LDFLAGS="-lm $LIBGMP $LIBJEMALLOC -lpthread"
+EACSL_LDFLAGS="-lm -lpthread"
 
 # Output file names
 OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source
@@ -566,11 +574,6 @@ if [ -n "$OPTION_EACSL" ]; then
     -then-last"
 fi
 
-# Bail if no files to translate are given
-if [ -z "$1" ]; then
-  error "no input files";
-fi
-
 # Instrument
 if [ -n "$OPTION_INSTRUMENT" ]; then
   ($OPTION_ECHO; \
@@ -621,7 +624,7 @@ if [ -n "$OPTION_COMPILE" ]; then
       OUTPUT_EXEC="$EACSL_OUTPUT_EXEC"
     fi
     # Sources of the selected memory model
-    EACSL_RTL=`mmodel_lib "$mod"`
+    EACSL_RTL=$(mmodel_lib "$mod")
     ($OPTION_ECHO;
      $CC \
        $CFLAGS $CPPFLAGS \
@@ -635,4 +638,3 @@ if [ -n "$OPTION_COMPILE" ]; then
   done
 fi
 exit 0;
-

src/plugins/e-acsl/share/e-acsl/e_acsl_assert.h

@@ -52,7 +52,9 @@ static void vabort(char *fmt, ...);
   vassert_fail(expr, __LINE__, __FILE__, fmt, __VA_ARGS__)
 
 static void exec_abort(int line, const char *file) {
+#ifdef E_ACSL_DEBUG
   trace();
+#endif
   kill(getpid(), SIGABRT);
 }