e-acscl wrapper:

    - Added man page
    - Fixed memory model option

src/plugins/e-acsl/Makefile.in

@@ -138,6 +138,7 @@ install::
 	$(PRINT_INSTALL) E-ACSL scripts
 	$(MKDIR) $(BINDIR)
 	$(CP) $(E_ACSL_DIR)/scripts/e-acsl-gcc.sh $(BINDIR)/
+	$(CP) $(E_ACSL_DIR)/man/e-acsl-gcc.sh.1 $(MANDIR)/man1/
 
 uninstall::
 	$(PRINT_RM) E-ACSL share files
@@ -148,6 +149,7 @@ uninstall::
 	      $(FRAMAC_SHARE)/manuals/e-acsl-manual.pdf
 	$(PRINT_RM) E-ACSL scripts
 	$(RM) $(BINDIR)/e-acsl-gcc.sh
+	$(RM) $(MANDIR)/man1/e-acsl-gcc.sh.1
 
 ################################
 # Building source distribution #
@@ -165,6 +167,8 @@ EACSL_DISTRIB_FILES=\
 	configure.ac Makefile.in \
 	doc/Changelog \
 	$(DOC_FILES) \
+	scripts/e-acsl-gcc.sh \
+	man/e-acsl-gcc.sh.1 \
 	share/e-acsl/*.[ch] \
 	share/e-acsl/memory_model/e_acsl_bittree.[ch] \
 	share/e-acsl/memory_model/e_acsl_mmodel*.[ch] \

src/plugins/e-acsl/man/e-acsl-gcc.sh.1

+.\"
+.\"
+.\"  This file is part of Frama-C.
+.\"
+.\"  Copyright (C) 2007-2015
+.\"    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 licenses/LGPLv2.1).
+.\"
+.\"
+
+.TH E-ACSL-GCC.SH 1 2016-02-02
+
+.SH NAME
+.B e-acsl-gcc.sh
+\- instrument and compile C files with E-ACSL
+.SH SYNOPSIS
+.B e-acsl-gcc.sh
+[
+.I options
+]
+.I files
+.SH DESCRIPTION
+.B e-acsl-gcc.sh
+is convenience wrapper for instrumentation of C programs using the
+E-ACSL Frama-C plugin and their subsequent compilation using the GNU compiler
+collection (GCC).
+.SH OPTIONS
+.B -h, --help
+show help page.
+.TP
+.B -c, --compile
+compile generated and original files.
+.TP
+.B -C, --compile-only
+compile input files as if they were generated by E-ACSL.
+.TP
+.B -p, --print
+output the code generated by E-ACSL to \fISTDOUT\fP.
+.TP \fI \fP
+.B -d, --debug=\fI<N>
+pass a value to Frama-C -debug option.
+.TP
+.B -o, --ocode=\fI<FILENAME>
+name of the output source file. Defaults to \fIa.out.frama.c\fP.
+.TP
+.B -O, --oexec=\fI<FILENAME>
+name of the executable generated from the un-instrumented code.
+Executable compiled from the E-ACSL instrumented sources is
+appended \fI.e.acsl\fP suffix.
+Unless specified, the
+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 -v, --verbose=\fI<N>
+pass a value to the Frama-C -verbose option.
+.TP
+.B -f, --frama-c-only
+run input source files through Frama-C without E-ACSL instrumentations.
+.TP
+.B -E, --extra-cpp-args=\fI<FLAGS>
+pass additional arguments to the Frama-C pre-processor.
+.TP
+.B -L, --frama-c-stdlib
+use Frama-C standard library instead of the system-wide one.
+.TP
+.B -M, --full-mmodel
+maximise memory-related instrumentation.
+.TP
+.B -g, --gmp
+always use GMP integers instead of C integral types.
+.TP
+.B -l, --ld-flags=\fI<FLAGS>
+pass the specified flags to the linker.
+.TP
+.B -e, --cpp-flags=\fI<FLAGS>
+pass the specified flags to the pre-processor at compile-time.
+For instrumentation-time proprocessor flags see \fB--extra-cpp-args\fP option.
+.TP
+.B -q, --quiet
+suppress any output except errors and warnings.
+.TP
+.B -s, --logfile=\fI<FILE>
+redirect all output to a given file.
+.TP
+.B -F, --frama-c-extra=\fI<OPTION>
+pass an extra option to frama-c invocation.
+.TP
+.B -m, --memory-model=\fI<bittree|tree|list|splaytree>
+memory model (i.e., runtime library for checking memory related annotations)
+to be linked against the instrumented file.
+
+Valid arguments are:
+  bittree     \- memory modelling using a Patricie trie ADT.
+  splaytree   \- memory modelling using a splay tree ADT.
+  list        \- memory modelling using a linked-list ADT.
+  tree        \- memory modelling using a binary tree ADT.
+
+By default Patricia trie  memory model is used.
+.TP
+.B -P, --production
+Compile optimized executatle without debug features.
+Note that un-optimized executables may lead to significant
+performance slowdown.
+.TP
+.B -N, --no-stdlib
+If specified the E-ACSL run-time library uses custom
+implementations of standard library functions (such as memset).
+By default GCC builtins are used (e.g., \fB__builtin_memset\fP).
+.TP
+.B -D, --debug-log=\fI<FILE>
+Specify the name of the file for logging of debugging output of
+modified modified executables. If '-' is specified then the
+output is redirected to the \fISTDERR\fP. By default
+\fI/tmp/e-acsl.log\fP file is used. Note that this option is meaningful
+in the absence of the -P flag, which diables debug logging for
+performance reasons.
+
+.SH EXIT STATUS
+.TP
+.B 0
+Successful execution
+.TP
+.B 1
+Invalid user input
+.TP
+.B frama-c or gcc error code
+Instrumentation- or compile-time error
+
+.SH EXAMPLES
+
+Instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP
+
+.B e-acsl-gcc.sh foo.c
+
+Instrument \fIfoo.c\fP, output the instrumented code to \fIgen_foo.c\fP and
+compile \fIfoo.c\fP into \fIfoo\fP and \fIgen_foo.c\fP into \fIfoo.e-acsl\fP.
+The \fB-P\fP option specifies that the instrumentation should omit debug
+functionality.
+
+.B e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo foo.c
+
+Assume \fIgen_foo.c\fP has been instrumented by E-ACSL and compile it into
+\fIa.out.e-acsl\fP using \fBsplaytree\fB memory model instead of the default
+one.
+
+.B e-acsl-gcc.sh --memory-model=splaytree -C gen_foo.c
+
+.SH SEE ALSO
+\fBgcc\fP(1), \fBcpp\fP(1), \fBld\fP(1), \fBframa-c\fP(1)

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

@@ -53,11 +53,6 @@ SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:"
 # Prefix for an error message due to wrong arguments
 ERROR="ERROR parsing arguments:"
 
-# Frama-C
-FRAMAC="`check_tool 'frama-c'`"
-FRAMAC_FLAGS=""
-FRAMAC_SHARE="`$FRAMAC -print-share-path`"
-
 # Architecture-dependent flags. Since by default Frama-C uses 32-bit
 # architecture we need to make sure that same architecture is used for
 # instrumentation and for compilation.
@@ -72,6 +67,13 @@ CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
 # GCC machine option
 GCCMACHDEP="-m$MACHDEPFLAGS"
 
+# Frama-C
+FRAMAC="`check_tool 'frama-c'`"
+FRAMAC_FLAGS=""
+FRAMAC_SHARE="`$FRAMAC -print-share-path`"
+EACSL_SHARE="$FRAMAC_SHARE/e-acsl"
+EACSL_MMODEL="bittree"
+
 # Macro that identifies E-ACSL compilation. Passed to Framac and GCC runs
 # but not to the original compilation
 EACSL_MACRO_ID="__E_ACSL__"
@@ -123,83 +125,21 @@ OPTION_BUILTINS="-DE_ACSL_BUILTINS"
 OPTION_EXTRA_CPP="-D$EACSL_MACRO_ID -I$FRAMAC_SHARE/libc $CPPMACHDEP"
 
 manpage() {
-  echo "NAME"
-  echo "  e-acsl-gcc -- convenience wrapper for instrumentation of C files with"
-  echo "   the E-ACSL Frama-C plugin and their subsequent compilation using"
-  echo "   GNU compiler collection (GCC)"
-  echo ""
-  echo "SYNOPSIS"
-  echo "  e-acsl-gcc <OPTIONS> <C-FILES>"
-  echo ""
-  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, defaults to a.out.frama.c"
-  echo "  -O, --oexec=<FILENAME>"
-  echo "      name of the executable generated from the un-instrumented code."
-  echo "      Executable compiled from the E-ACSL instrumented sources is"
-  echo "      appended .e.acsl suffix. Defaults to a.out and a.out.e-acsl"
-  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 "  -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)"
-  echo "  -q, --quiet"
-  echo "      suppress any output except for errors and warnings"
-  echo "  -s, --logfile=<FILE>"
-  echo "      redirect all output to a given log file"
-  echo "  -F, --frama-c-extra <OPTION>"
-  echo "      pass an extra option to frama-c invocation"
-  echo "  -m, --memory-model=<bittree|tree|list|splaytree>"
-  echo "      memory model (i.e., runtime library) to be used at compile time."
-  echo "      Valid arguments are:"
-  echo "        bittree     - memory modelling using a Patricie trie ADT"
-  echo "        splay_tree  - memory modelling using a splay tree ADT"
-  echo "        list        - memory modelling using a linked-list ADT"
-  echo "        tree        - memory modelling using a binary tree ADT"
-  echo "  -P, --production"
-  echo "      Compile optimized executatle without debug features"
-  echo "  -N, --no-stdlib"
-  echo "      If specified the E-ACSL run-time library uses custom  "
-  echo "      implementations of standard library functions (such as memset)."
-  echo "      By default GCC builtins are used (e.g., __builtin_memset)."
-  echo "  -D, --debug-log=<FILE>"
-  echo "      Specify the name of the file for logging of debugging output of"
-  echo "      modified modified executables. If '-' is specified then the"
-  echo "      output is redirected to the standard error stream. By default  "
-  echo "      /tmp/e-acsl.log file is used. Note that this option is meaningful"
-  echo "      in the absence of the -P flag, which diables debug logging for  "
-  echo "      performance reasons."
-  echo ""
-  echo "EXAMPLES:"
-  echo "  # Instrument foo.c and output the instrumented code to a.out.frama.c"
-  echo "      e-acsl-gcc.sh foo.c"
-  echo "  # Instrument foo.c, output the instrumented code to gen_foo.c and"
-  echo "  # compile foo.c into foo and gen_foo.c into foo.e-acsl"
-  echo "      e-acsl-gcc.sh -c -ogen_foo.c -Ofoo foo.c"
-  echo "  # Assume gen_foo.c has been instrumented by E-ACSL and compile it"
-  echo "  # into a.out.e-acsl"
-  echo "      e-acsl-gcc.sh -C gen_foo.c"
+  printf "e-acsl-gcc.sh - instrument and compile C files with E-ACSL
+Usage: e-acsl-gcc.sh [options] files
+Options:
+    -h         show this help page
+    -c         compile instrumented code
+    -p         output the generated code to STDOUT
+    -O <file>  output the generated executable to <file>
+    -M         maximise memory-related instrumentation
+    -q         suppress any output except for errors and warnings
+    -s <file>  redirect all output to <file>
+    -P         compile executatle without debug features
+
+Notes:
+  This manual page shows only basic options.
+  See man (1) e-acsl-gcc.sh for full up-to-date documentation.\n"
   exit 1
 }
 
@@ -357,9 +297,9 @@ do
     ;;
     -m|--memory-model)
       shift;
-      OPTION_MMODEL="$1"
-      echo $OPTION_MMODEL | grep "\(tree\|bittree\|splay_tree\|list\)"
-      error "no such memory model: $OPTION_MMODEL" $?
+      EACSL_MMODEL="$1"
+      echo $EACSL_MMODEL | grep "\(tree\|bittree\|splay_tree\|list\)"
+      error "no such memory model: $EACSL_MMODEL" $?
       shift;
     ;;
   esac
@@ -376,7 +316,7 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
   # Memory model sources
   RTL="$EACSL_SHARE/e_acsl.c \
     $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
-    $EACSL_SHARE/memory_model/e_acsl_$OPTION_MMODEL.c"
+    $EACSL_SHARE/memory_model/e_acsl_$EACSL_MMODEL.c"
 
   ($OPTION_ECHO; \
     $FRAMAC \