Added a convenience script called `e-acsl-gcc` for instrumenting files

using E-ACSL plugin and their subsequent compilation using GCC.

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 #

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

+#!/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;