diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index f8c4eff5eba91504deed0da7181f8cb476eed47a..8ca2fc45509d1c9495fbd02d4b97a81c43fcae87 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,7 +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
+-* E-ACSL       [2016/07/13] Add an e-acsl-gcc.sh option (--print--models)
+	        allowing to print the names of the supported memory models.
+-* E-ACSL       [2016/05/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
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 fbce9931bcf00300153c7fa8f859b757c20762f9..73a08a9da7101ee065c7182248dd9392a39bc840 100644
--- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -139,6 +139,9 @@ Valid arguments are:
 
 By default the Patricia trie  memory model is used.
 .TP
+.B --print-models
+Print the names of the supported memory models
+.TP
 .B -P, --production
 generate an optimized executable with all debug features disabled.
 Unoptimized executables (default) may lead to a significant
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index eae3b80c4d7ffead7d38980ab8d3623c124e9226..aeea5a51d0e1e27152219ad4e7686f8b737a6e66 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -70,7 +70,7 @@ rte_options() {
         opts="$opts -rte-mem"
       ;;
       int) # integer overflows
-        intopts=""
+        intopts="-warn-signed-overflow -warn-unsigned-overflow"
       ;;
       float) # casts from floating-point to integer
         opts="$opts -rte-float-to-int"
@@ -103,15 +103,17 @@ rte_options() {
   return 0;
 }
 
-# Check if getopt is GNU
+# Check if the following tools are GNU and abort otherwise
 required_tool getopt "util-linux"
 required_tool readlink "GNU coreutils"
+required_tool find "GNU findutils"
 
 # 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:,oexec-e-acsl:"
+  debug-log:,frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:,
+  print-mmodels"
 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:"
@@ -134,6 +136,7 @@ OPTION_EACSL_OUTPUT_EXEC=""              # Name of E-ACSL executable
 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_PRINT_MMODELS=                    # Print memory model names
 OPTION_GMP=                              # Use GMP integers everywhere
 OPTION_DEBUG_MACRO="-DE_ACSL_DEBUG"      # Debug macro
 OPTION_DEBUG_LOG_MACRO=""                # Specification of debug log file
@@ -365,15 +368,15 @@ do
       OPTION_EACSL_MMODELS="`echo $1 | sed -s 's/,/ /g'`"
       shift;
     ;;
+    # Print names of the supported memody models.
+    --print-mmodels)
+      shift;
+      OPTION_PRINT_MMODELS="1"
+    ;;
   esac
 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"
@@ -417,6 +420,10 @@ CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
 # GCC machine option
 GCCMACHDEP="-m$MACHDEPFLAGS"
 
+# Macro that identifies E-ACSL compilation. Passed to Frama-C
+# and GCC runs but not to the original compilation
+EACSL_MACRO_ID="__E_ACSL__"
+
 # Frama-C and related flags
 FRAMAC_CPP_EXTRA="
   $OPTION_FRAMAC_CPP_EXTRA
@@ -437,32 +444,38 @@ fi
 error "Cannot find required $EACSL_SHARE/e_acsl_mmodel_api.h header" \
   `test -f "$EACSL_SHARE/e_acsl_mmodel_api.h"; echo $?`
 
-# Echo the name of the source file corresponding to the name of a memory model
-# or report an error of the given model does not exist.
+# Echo the absolute path of the source file corresponding to a memory model
+# given by the first argument, or report an error of the given model does not
+# exist. In case no argument is supplied, output the names of the memory models
+# supported in this distribution.
 mmodel_sources() {
-  model=""
-  case "$1" in
-    bittree) model="bittree_model/e_acsl_bittree_mmodel.c" ;;
-    segment) model="segment_model/e_acsl_segment_mmodel.c" ;;
-    *) error "Memory model '$1' does not exist" ;;
-  esac
-  model="$EACSL_SHARE/$model"
-  if ! [ -f "$model" ]; then
-    error "Memory model '$1' exists but not available in this distribution"
+  local model="$1"
+  local models=$(find $EACSL_SHARE -maxdepth 1 \
+     -name '*_model'  -type d -exec basename {} \; | sed 's/_model$//')
+
+  if [ -n "$model" ]; then
+    model=$(echo $models | tr ' ' '\n' | grep "^$model$")
+    if [ -n "$model" ]; then
+      echo "$EACSL_SHARE/$model"_model/e_acsl_"$model"_mmodel.c
+    else
+      error "Memory model '$1' is not available in this distribution"
+    fi
   else
-    echo "$model"
+    echo $models
   fi
 }
 
+# If specified, print the names of the supported memory models and exit
+if [ -n "$OPTION_PRINT_MMODELS" ]; then
+  mmodel_sources
+  exit 0
+fi
+
 # Once EACSL_SHARE is defined check the memory models provided at inputs
 for mod in $OPTION_EACSL_MMODELS; do
   mmodel_sources $mod > /dev/null
 done
 
-# Macro that identifies E-ACSL compilation. Passed to Frama-C
-# and GCC runs but not to the original compilation
-EACSL_MACRO_ID="__E_ACSL__"
-
 # Gcc and related flags
 CC="$OPTION_CC"
 CFLAGS="$OPTION_CFLAGS
@@ -520,6 +533,11 @@ 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; \
diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
index 23298becc5864e468a4c9a16d70426e3617d1cf1..f32206df2e74609cf15c65d8b7852cb267496a55 100755
--- a/src/plugins/e-acsl/scripts/testrun.sh
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -52,11 +52,13 @@ GMP="$3"    # Whether to issue an additional run with -e-acsl-gmp-only
 EXTRA="$4"  # Extra e-acsl-gcc.sh flags
 DEBUG="$5"  # Debug option
 
+EACSLGCC="$(dirname $0)/e-acsl-gcc.sh" # E-ACSL wrapper script
+MODELS="$($EACSLGCC --print-mmodels)" # Supported memory models
+
 ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository
 TESTDIR="$ROOTDIR/tests/$PREFIX" # Test suite directory
 RESDIR=$TESTDIR/result # Result directory within the test suite
 TESTFILE=`ls $TESTDIR/$TEST.[ic]` # Source test file
-MODEL="bittree" # Memory model to link against
 
 LOG="$RESDIR/$TEST.testrun" # Base name for log files
 OUT="$RESDIR/gen_$TEST"     # Base name for instrumented files
@@ -95,16 +97,17 @@ trap "clean" EXIT HUP INT QUIT TERM
 # Run executable and report results
 #  $1 - path to an executable
 #  $2 - path to a log file
-#  $3 - type of the executable (i.e., generated from original or instrumented
-#    sources)
+#  $3 - memory model the executable has been linked against
 run_executable() {
   local executable="$1"
   local log="$2"
-  local type="$3"
+  local model="$3"
+
+  debug "Run: $executable"
+  debug "Log: $log"
 
-  debug "Run and log $executable"
   if ! `$executable > $log 2>&1`; then
-    error "[$3 run]: Runtime failure in test case $TEST:" $log
+    error "[$3 model] Runtime failure in test case '$TEST'" $log
   fi
 }
 
@@ -115,26 +118,36 @@ run_test() {
   local logfile=$LOG.$RUNS.elog # Log file for e-acsl-gcc.sh output
   local oexec=$OUT.$RUNS.out # Generated executable name
   local oexeclog=$LOG.$RUNS.rlog # Log for executable output
-  local extra="$1" # Additional arguments to e-acsl-gcc.sh
+  local model="$1" # Memory model to link against
+  local extra="$2" # Additional arguments to e-acsl-gcc.sh
 
-  # Command for instrumenting the source file and compiling the original
-  # and the instrumented code
-  EACSL_GCC="./scripts/e-acsl-gcc.sh \
-    --compile $TESTFILE --ocode=$ocode --logfile=$logfile \
-    --instrumented-only --memory-model=$MODEL --oexec=$oexec $extra"
+  # e-acsl-gcc.sh reports models as space-separated string. Make a
+  # comma-separated one otherwise the following does not work
+  MODELSTR="$(echo $MODELS | tr ' ' ',')"
 
-  debug "Run $EACSL_GCC"
-  $EACSL_GCC || error "Command $EACSL_GCC failed" "$logfile"
+  # Command for instrumenting the source file
+  COMMAND="$EACSLGCC $TESTFILE --ocode=$ocode --logfile=$logfile $extra"
 
-  # Log outputs of the generated executables
-  run_executable $oexec.e-acsl  $oexeclog.e-acsl "Instrumented"
+  debug "Run $COMMAND"
+  $COMMAND || error "Command $COMMAND failed" "$logfile"
+
+  # Compile instrumented source and run executable
+  for model in $MODELS; do
+    # Command for compiling the instrumented file with a given memory model
+    COMMAND="$EACSLGCC --compile-only --memory-model=$model --logfile=$logfile \
+      --oexec-e-acsl=$oexec-$model $ocode"
+    debug "Run $COMMAND"
+    $COMMAND || error "Command $COMMAND failed" "$logfile"
+    run_executable $oexec-$model $oexeclog-$model $model
+  done
 
   RUNS=$((RUNS+1))
 }
 
+run_test $model "$EXTRA"
 # Run GMP tests if specified
-run_test "$EXTRA"
 if [ -n "$GMP" ]; then
-  run_test "--gmp $EXTRA"
+  run_test $model "--gmp $EXTRA"
 fi
+
 exit 0