diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 137e7566d6a7509d8cb6f50c5282b3a651b0e7bd..4653f55a9036d5fe0f03fea88186a4af3ea018bb 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -135,6 +135,7 @@ install::
$(E_ACSL_DIR)/doc/manuals/e-acsl-implementation.pdf \
$(E_ACSL_DIR)/doc/manuals/e-acsl-manual.pdf \
$(FRAMAC_SHARE)/manuals
+ find scripts -maxdepth 1 -type f -executable -exec $(CP) {} $(BINDIR) \;
uninstall::
$(PRINT_RM) E-ACSL share files
@@ -143,6 +144,7 @@ uninstall::
$(RM) $(FRAMAC_SHARE)/manuals/e-acsl.pdf \
$(FRAMAC_SHARE)/manuals/e-acsl-implementation.pdf \
$(FRAMAC_SHARE)/manuals/e-acsl-manual.pdf
+ find scripts -maxdepth 1 -type f -executable -execdir $(RM) $(BINDIR)/{} \;
################################
# Building source distribution #
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc b/src/plugins/e-acsl/scripts/e-acsl-gcc
new file mode 100755
index 0000000000000000000000000000000000000000..1c8d7dfd8e69915953690b05eceb47fd757968a0
--- /dev/null
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc
@@ -0,0 +1,299 @@
+#!/bin/sh -e
+
+# Convenience wrapper for small runs of E-ACSL Frama-C plugin
+
+# Print a message to STDERR and exit
+error () {
+ echo "e-acsl-gcc: fatal error: $1" 1>&2
+ exit 1;
+}
+
+# Check if an executable can be found by in the PATH
+has_tool() {
+ which "$@" >/dev/null 2>&1 && return 0 || return 1
+}
+
+# Abort if a given executable cannot be found in the $PATH
+check_tool() {
+ has_tool "$1" && echo "$1" \
+ || error "Cannot find '$1' executable in the \$PATH"
+}
+
+# Getopt options
+LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:, \
+ frama-c-only,extra-cpp-args,rtl,frama-c-stdlib,full-mmodel,gmp,
+ ld-flags:,cpp-flags:"
+SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g"
+# Prefix for an error message due to wrong arguments
+ERROR="ERROR parsing arguments:"
+
+# Gcc
+CC="`check_tool 'gcc'`"
+CFLAGS="-std=c99 -w -g3 -O2 -fno-builtin"
+CPPFLAGS=""
+LDFLAGS=""
+# Frama-C
+FRAMAC="`check_tool 'frama-c'`"
+FRAMAC_FLAGS="-implicit-function-declaration ignore"
+
+# E-ACSL source that needed for compilation
+FRAMA_C_SHARE="`frama-c -print-share-path`"
+EACSL_SHARE="`$FRAMAC -print-share-path`/e-acsl"
+RTL="$EACSL_SHARE/e_acsl.c \
+ $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
+ $EACSL_SHARE/memory_model/e_acsl_bittree.c \
+"
+
+# Frama-c machdep option
+ARCH="$(uname -m | tr -d '\n')"
+case $ARCH in
+ x86_64)
+ MACHDEPFLAGS="86_64"
+ ;;
+ i686)
+ MACHDEPFLAGS="86_32"
+ ;;
+ *)
+ error "Unsupported archirtecture: $ARCH"
+ ;;
+esac
+
+# -machdep option sent to frama-c
+MACHDEP="-machdep gcc_x$MACHDEPFLAGS"
+# Macro for correct preprocessing of Frama-C generated code
+CPPMACHDEP="-D__FC_MACHDEP_X$MACHDEPFLAGS"
+
+# CPP and LD flags for compilation of E-ACSL-generated sources
+EACSL_CPP_FLAGS="
+ -D__FC_errno=(*__errno_location())
+ -D__builtin_printf=printf
+ -D__builtin_memcpy=memcpy"
+EACSL_LD_FLAGS="-lgmp -lm"
+
+# Variables holding getopt options
+OPTION_INSTRUMENT=1 # Perform E-ACSL instrumentation
+OPTION_PRINT= # Output instrumented code
+OPTION_DEBUG= # Set frama-c debug flag
+OPTION_VERBOSE= # Set frama-c verbose flag
+OPTION_COMPILE= # Compile instrumented program
+OPTION_OCODE="a.out.frama.c" # Name of the translated file
+OPTION_OEXEC="a.out" # Generated executable name
+OPTION_EACSL="-e-acsl -then-on 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
+OPTION_EXTRA_CPP="-I$FRAMA_C_SHARE/libc $CPPMACHDEP" # Extra CPP flags
+
+manpage() {
+ echo "NAME"
+ echo " e-acsl-gcc -- convenience wrapper instrumentation of C files with"
+ echo " the E-ACSL Frama-C plugin and their subsequent compilation using"
+ echo " GNU compiler collection (GCC)"
+ echo "SYNOPSIS"
+ echo " e-acsl-gcc <OPTIONS> <C-FILES>"
+ echo "OPTIONS"
+ echo " -h, --help"
+ echo " show this help page"
+ echo " -c, --compile"
+ echo " compile generated and original files"
+ echo " -C, --compile-only"
+ echo " compile input files as if they were generated by E-ACSL"
+ echo " -p, --print"
+ echo " output the code generated by E-ACSL to STDOUT"
+ echo " -d, --debug <N>"
+ echo " pass a value to Frama-C -debug option"
+ echo " -o, --ocode <FILENAME>"
+ echo " name of the output source file"
+ echo " -O, --oexec <FILENAME>"
+ echo " name of the compiled executable"
+ echo " -v, --verbose <N>"
+ echo " pass a value to Frama-C -verbose option"
+ echo " -f, --frama-c-only"
+ echo " run input source files through Frama-C without E-ACSL"
+ echo " -E, --extra-cpp-args <FLAGS>"
+ echo " pass additional arguments to the Frama-C pre-processor"
+ echo " -R, --rtl"
+ echo " output E_ACSL runtime libraries to STDOUT"
+ echo " -L, --frama-c-stdlib"
+ echo " use Frama-C standard library"
+ echo " -M, --full-mmodel"
+ echo " maximise memory-related instrumentation"
+ echo " -g, --gmp"
+ echo " always use GMP integers instead of C integral types"
+ echo " -l, --ld-flags <FLAGS>"
+ echo " pass the specified flags to the linker"
+ echo " -e, --cpp-flags <FLAGS>"
+ echo " pass the specified flags to the pre-processor (compile-time)"
+ exit 1
+}
+
+# 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" -- "$@"`
+
+# Print and exit if getopt fails
+if [ $? != 0 ]; then
+ exit 1;
+fi
+
+# Set all options in $@ before -- and other after
+eval set -- "$ARGS"
+
+# Switch statements for other options
+for i in $@
+do
+ case "$i" in
+ # Do compile instrumented code
+ --help|-h)
+ shift;
+ manpage;
+ ;;
+ # Do compile instrumented code
+ --compile|-c)
+ shift;
+ OPTION_COMPILE=1
+ ;;
+ # Print the result of instrumenation
+ --print|-p)
+ shift;
+ OPTION_PRINT=1
+ ;;
+ # Set Frama-C debug flag
+ --debug|-d)
+ shift;
+ if [ "$1" -eq "$1" ] 2>/dev/null; then
+ OPTION_DEBUG="-debug $1"
+ else
+ error "-d|--debug option requires integer argument"
+ fi
+ shift;
+ ;;
+ # Set Frama-C verbose flag
+ --verbose|-v)
+ shift;
+ if [ "$1" -eq "$1" ] 2>/dev/null; then
+ OPTION_VERBOSE="-verbose $1"
+ else
+ error "-v|--verbose option requires integer argument"
+ fi
+ shift;
+ ;;
+ # Specify the name of the default source file where instrumented
+ # code is to be written
+ --ocode|-o)
+ shift;
+ OPTION_OCODE="$1"
+ shift
+ ;;
+ # Specify the base name of the executable generated from the
+ # instrumented and non-instrumented sources.
+ --oexec|-O)
+ shift;
+ OPTION_OEXEC="$1"
+ shift
+ ;;
+ # Additional CPP arguments
+ --extra-cpp-args|-E)
+ shift;
+ OPTION_EXTRA_CPP="$OPTION_EXTRA_CPP$1"
+ shift;
+ ;;
+ # Additional flags passed to the linker
+ --ld-flags|-l)
+ shift;
+ LDFLAGS="$LDFLAGS $1"
+ shift;
+ ;;
+ # Additional flags passed to the pre-processor (compile-time)
+ --cpp-flags|-e)
+ shift;
+ CPPFLAGS="$CPPFLAGS $1"
+ shift;
+ ;;
+ # Do not perform the instrumentation, only compile the provided sources
+ # This option assumes that the source files provided at input have
+ # already been instrumented
+ --compile-only|-C)
+ shift;
+ OPTION_INSTRUMENT=
+ OPTION_COMPILE="1"
+ ;;
+ # Run only frama-c related instrumentation
+ --frama-c-only|-f)
+ shift;
+ OPTION_EACSL=
+ ;;
+ # Output the RTL files
+ --rtl|-R)
+ echo $RTL
+ exit 0;
+ ;;
+ # Do use Frama-C stdlib, which is the default behaviour of Frama-C
+ --frama-c-stdlib|-L)
+ shift;
+ OPTION_FRAMA_STDLIB=""
+ ;;
+ # Use as much memory-related instrumentation as possible
+ -M|--full-mmodel)
+ shift;
+ OPTION_FULL_MMODEL="-e-acsl-full-mmodel"
+ ;;
+ # Use GMP everywhere
+ -g|--gmp)
+ shift;
+ OPTION_GMP="-e-acsl-gmp-only"
+ ;;
+ esac
+done
+shift;
+
+# Bail if no files to translate are given
+if test -z "$1"; then
+ error "no input files";
+fi
+
+# Instrument
+if [ -n "$OPTION_INSTRUMENT" ]; then
+ (set -x; \
+ $FRAMAC \
+ $FRAMAC_FLAGS \
+ $MACHDEP \
+ -cpp-extra-args="$OPTION_EXTRA_CPP" \
+ -e-acsl-share $EACSL_SHARE \
+ $OPTION_VERBOSE \
+ $OPTION_DEBUG \
+ $OPTION_FRAMA_STDLIB \
+ $OPTION_FULL_MMODEL \
+ $OPTION_GMP \
+ "$@" \
+ $OPTION_EACSL \
+ -print \
+ -ocode "$OPTION_OCODE");
+ # Print translated code
+ if [ -n "$OPTION_PRINT" ]; then
+ $CAT $OPTION_OCODE
+ fi
+fi
+
+# Compile
+if test -n "$OPTION_COMPILE" ; then
+ # Compile original files only if the instrumentation option is given,
+ # otherwise the provided sources are assumed to be E-ACSL instrumented
+ # files
+ if [ -n "$OPTION_INSTRUMENT" ]; then
+ (set -x; $CC $CPPFLAGS $CFLAGS "$@" -o "$OPTION_OEXEC" $LDFLAGS)
+ else
+ OPTION_OCODE="$@"
+ fi
+ # Compile and link E-ACSL-instrumented file
+ (set -x; $CC $CPPFLAGS $CFLAGS $EACSL_CPP_FLAGS $RTL \
+ "$OPTION_OCODE" -o "$OPTION_OEXEC.e-acsl" $LDFLAGS $EACSL_LD_FLAGS)
+fi
+exit 0;