diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index b7ee31318d8e38db3d6183335b13c8ef7ffed676..f8c4eff5eba91504deed0da7181f8cb476eed47a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,6 +15,9 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2016/01/22] Add an e-acsl-gcc.sh option (--rte|-a) allowing to
+          annotate the source program with memory-safety assertions prior to
+          instrumentation.
 -  E-ACSL       [2016/05/23] Re-implementation of the type system which
 	        improves the efficiency of the generated code over integers.
 -* E-ACSL       [2016/05/23] Fix bug #2191 about complicate structs and
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
index 9648bdc10443ed063e1ec625b99d5978f5ad47c9..fbce9931bcf00300153c7fa8f859b757c20762f9 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -79,6 +79,10 @@ names of the executables generated from the original
 and the modified programs are
 \fIa.out\fP and \fIa.out.e-acsl\fP respectively.
 .TP
+.B --oexec-e-acsl=\fI<FILE>
+name of the executable file generated from the \fBE-ACSL\fP-instrumented file.
+Unless specified, the executable is named as inidicated by the \fB--oexec\fP option.
+.TP
 .B -f, --frama-c-only
 run input source files through \fBFrama-C\fP without \fBE-ACSL\fP instrumentations.
 .TP
@@ -111,6 +115,20 @@ redirect all output to a given file.
 .B -F, --frama-c-extra=\fI<FLAGS>
 pass an extra option to a \fBFrama-C\fP invocation.
 .TP
+.B -a, --rte=\fI<OPTSTRING>
+annotate a source program with assertions using a run of an RTE plugin prior to
+E-ACSL. \fIOPTSTRING\fP is a comma-separated string that specifies the types of
+generated assertions.
+Valid arguments are:
+  \fImem\fP \- valid pointer or array accesses.
+  \fIint\fP \- integer overflows.
+  \fIfloat\fP \- casts from floating-point to integer.
+  \fIdiv\fP \- division by zero.
+  \fIret\fP \- return value in non-void functions.
+  \fIprecond\fP \- function calls based on contracts.
+  \fIshift\fP \- left and right shifts by a value out of bounds.
+  \fIall\fP \- all of the above.
+.TP
 .B -m, --memory-model=\fI<model>
 memory model (i.e., a runtime library for checking memory related annotations)
 to be linked against the instrumented file.
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
new file mode 100644
index 0000000000000000000000000000000000000000..fa4a92dbe1e991564dacefcd311f1bf73778d34e
--- /dev/null
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp
@@ -0,0 +1,57 @@
+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C's E-ACSL plug-in.                    #
+#                                                                        #
+#  Copyright (C) 2012-2016                                               #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  you can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file license/LGPLv2.1).             #
+#                                                                        #
+##########################################################################
+
+# Bash completion for e-acsl-gcc.sh
+
+_eacsl_gcc() {
+  local cur prev opts base
+  COMPREPLY=()
+  cur="${COMP_WORDS[COMP_CWORD]}"
+  prev="${COMP_WORDS[COMP_CWORD-1]}"
+
+  opts="
+    -i -C -p -d -o -O -v -f -E -L -M -l -e -g -q -s -F -P -N -D -I -G -X -a
+    -h -c -msegment -mbittree
+    --verbose= --debug= --debug-log= --logfile= --quiet --production --help
+    --ocode= --oexec= --oexec-e-acsl=
+    --ld-flags= --cpp-flags= --extra-cpp-args=
+    --frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model=
+    --compile --compile-only --print --frama-c-only --instrumented-only
+    --gmp --full-mmodel --rte --no-int-overflow --no-stdlib --frama-c-stdlib"
+
+  case ${prev} in
+    -*)
+      COMPREPLY=($(compgen -W "${opts}" -- ${cur}))
+      return 0
+    ;;
+    *)
+      COMPREPLY=($(compgen -W "${opts}" -- ${cur}))
+      [[ $COMPREPLY == *= ]] && compopt -o nospace
+      return 0
+    ;;
+  esac
+
+  return 0
+}
+complete -F _eacsl_gcc e-acsl-gcc.sh
+
+
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index d1d6f74a66a3213666f301da545c85caa03262b5..eae3b80c4d7ffead7d38980ab8d3623c124e9226 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -33,6 +33,14 @@ error () {
   fi
 }
 
+# Check whether the first line reported by running command $1 has an identifier
+# specified by $2. E.g., check whether readlink used by the script is GNU and
+# getopt comes from util-linux.
+required_tool() {
+  "$1" --version 2>&1 | head -1 | grep "$2" > /dev/null
+  error "$1 is not $2" $?
+}
+
 # Check if a given executable name can be found by in the PATH
 has_tool() {
   which "$@" >/dev/null 2>&1 && return 0 || return 1
@@ -44,13 +52,67 @@ check_tool() {
    { has_tool "$1" || test -e "$1"; } || error "No executable $1 found";
 }
 
+# build and output option string for RTE plugin based on a comma-delimited
+# option string
+rte_options() {
+  local optstring="$1"
+  local start="-rte -rte-warn"
+  local opts="-rte-no-all"
+  # RTE integer overflow options coming from Frama-C, presently
+  # they are enabled by default, so they should be negated
+  local intopts="-no-warn-signed-overflow -no-warn-unsigned-overflow"
+  local vopts="mem,int,float,div,ret,precond,shift,all"
+  local all=""
+
+  for opt in $(echo $optstring | tr ',' ' '); do
+    case $opt in
+      mem) # valid pointer or array access
+        opts="$opts -rte-mem"
+      ;;
+      int) # integer overflows
+        intopts=""
+      ;;
+      float) # casts from floating-point to integer
+        opts="$opts -rte-float-to-int"
+      ;;
+      div) # division by zero
+        opts="$opts -rte-div"
+      ;;
+      ret) # return
+      ;;
+      precond) # function calls based on contracts
+        opts="$opts -rte-precond"
+      ;;
+      shift) # left and right shifts by a value out of bounds
+        opts="$opts -rte-shift"
+      ;;
+      all) # all assertions
+        all=1
+      ;;
+      *)
+        return 1;
+      ;;
+    esac
+  done
+
+  if [ -n "$all" ]; then
+    echo $start -rte-all -then
+  else
+    echo $start $opts $intopts -then
+  fi
+  return 0;
+}
+
+# Check if getopt is GNU
+required_tool getopt "util-linux"
+required_tool readlink "GNU coreutils"
+
 # Getopt options
 LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:,
   frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
   ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,production,no-stdlib,
-  debug-log:,frama-c:,gcc:,e-acsl-share:,instrumented-only,rte,no-int-overflow,
-  oexec-e-acsl:"
-SHORTOPTIONS="i,h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:,I:,G:,X,a"
+  debug-log:,frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:"
+SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:,I:,G:,X,a:"
 # Prefix for an error message due to wrong arguments
 ERROR="ERROR parsing arguments:"
 
@@ -69,7 +131,7 @@ OPTION_COMPILE=                          # Compile instrumented program
 OPTION_OUTPUT_CODE="a.out.frama.c"       # Name of the translated file
 OPTION_OUTPUT_EXEC="a.out"               # Generated executable name
 OPTION_EACSL_OUTPUT_EXEC=""              # Name of E-ACSL executable
-OPTION_EACSL="-e-acsl -then-last"        # Specifies E-ACSL run
+OPTION_EACSL="-e-acsl"                   # Specifies E-ACSL run
 OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
 OPTION_FULL_MMODEL=                      # Instrument as much as possible
 OPTION_GMP=                              # Use GMP integers everywhere
@@ -116,14 +178,6 @@ 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
-if has_tool 'pygmentize'; then
-  CAT="pygmentize -g -O style=colorful,linenos=1"
-else
-  CAT="cat"
-fi
-
 # Run getopt
 ARGS=`getopt -n "$ERROR" -l "$LONGOPTIONS" -o "$SHORTOPTIONS" -- "$@"`
 
@@ -209,6 +263,7 @@ do
       OPTION_OUTPUT_EXEC="$1"
       shift
     ;;
+    # Specify the output name of the E-ACSL generated executable
     --oexec-e-acsl)
       shift;
       OPTION_EACSL_OUTPUT_EXEC="$1"
@@ -281,13 +336,13 @@ do
     # Supply Frama-C executable name
     -I|--frama-c)
       shift;
-      OPTION_FRAMAC="$1"
+      OPTION_FRAMAC="$(which $1)"
       shift;
     ;;
     # Supply GCC executable name
     -G|--gcc)
       shift;
-      OPTION_CC="$1"
+      OPTION_CC="$(which $1)"
       shift;
     ;;
     # Specify EACSL_SHARE directory (where C runtime library lives) by hand
@@ -298,12 +353,10 @@ do
       shift;
     ;;
     --rte|-a)
-      shift
-      OPTION_RTE="-rte -rte-mem -rte-no-float-to-int"
-    ;;
-    --no-int-overflow|-i)
-        shift
-        FRAMAC_FLAGS="-no-warn-signed-overflow -no-warn-unsigned-overflow $FRAMAC_FLAGS"
+      shift;
+      OPTION_RTE=`rte_options $1`
+      error "Invalid argument $1 to --rte|-a option" $?
+      shift;
     ;;
     # A memory model  (or models) to link against
     -m|--memory-model)
@@ -343,7 +396,7 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then
   EACSL_SHARE="$DEVELOPMENT/share/e-acsl"
   # Add the project directory to FRAMAC_PLUGINS,
   # otherwise Frama-C uses an installed version
-  FRAMAC_FLAGS="-add-path=$DEVELOPMENT $FRAMAC_FLAGS"
+  FRAMAC_FLAGS="-add-path=$DEVELOPMENT/top -add-path=$DEVELOPMENT $FRAMAC_FLAGS"
 else
   # Installed version. FRAMAC_SHARE should not be used here as Frama-C
   # and E-ACSL may not be installed to the same location
@@ -458,6 +511,15 @@ else
     EACSL_OUTPUT_EXEC="$OPTION_EACSL_OUTPUT_EXEC"
 fi
 
+# Build E-ACSL plugin argument string
+if [ -n "$OPTION_EACSL" ]; then
+  OPTION_EACSL="
+    $OPTION_EACSL
+    $OPTION_GMP
+    $OPTION_FULL_MMODEL
+    -then-last"
+fi
+
 # Instrument
 if [ -n "$OPTION_INSTRUMENT" ]; then
   ($OPTION_ECHO; \
@@ -466,20 +528,17 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
     $MACHDEP \
     -cpp-extra-args="$OPTION_FRAMAC_CPP_EXTRA" \
     -e-acsl-share=$EACSL_SHARE \
+    $OPTION_FRAMA_STDLIB \
     $OPTION_VERBOSE \
     $OPTION_DEBUG \
-    $OPTION_FRAMA_STDLIB \
-    $OPTION_FULL_MMODEL \
-    $OPTION_GMP \
-    $OPTION_RTE \
     "$@" \
+    $OPTION_RTE \
     $OPTION_EACSL \
-    -print \
-    -ocode "$OPTION_OUTPUT_CODE");
+    -print -ocode "$OPTION_OUTPUT_CODE");
     error "aborted by Frama-C" $?;
   # Print translated code
   if [ -n "$OPTION_PRINT" ]; then
-    $CAT $OPTION_OUTPUT_CODE
+    cat $OPTION_OUTPUT_CODE
   fi
 fi