diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e41aa41b752a05253b6c5be77dad5048433f913a..65b6a0d9866d31a0f43bcb8186bfa545474f1cd8 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -138,6 +138,8 @@ install::
$(PRINT_INSTALL) E-ACSL scripts
$(MKDIR) $(BINDIR)
$(CP) $(E_ACSL_DIR)/scripts/e-acsl-gcc.sh $(BINDIR)/
+ $(PRINT_INSTALL) man pages
+ $(CP) $(E_ACSL_DIR)/man/e-acsl-gcc.sh.1 $(MANDIR)/man1/
uninstall::
$(PRINT_RM) E-ACSL share files
@@ -148,6 +150,8 @@ uninstall::
$(FRAMAC_SHARE)/manuals/e-acsl-manual.pdf
$(PRINT_RM) E-ACSL scripts
$(RM) $(BINDIR)/e-acsl-gcc.sh
+ $(PRINT_RM) man pages
+ $(RM) $(MANDIR)/man1/e-acsl-gcc.sh.1
################################
# Building source distribution #
@@ -165,6 +169,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] \
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 2270f45d71c053cfdfaf30c41cf10632c77d04f4..945b09e32f12951089902bcfec0c3d192ad7bcc7 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,10 +15,13 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
+- E-ACSL [2016/02/03] Added scripts/testrun.sh - a convenience wrapper
+ around e-acsl-gcc.sh for use with testing.
+-* E-ACSL [2016/01/15] Fix installation with custom --prefix.
-* E-ACSL [2016/01/05] Fix bug in the memory model that caused the
tracked size of heap memory be computed incorrectly.
-- E-ACSL [2015/12/15] Added a convenience script for small runs of the
- E-ACSL plugin.
+- E-ACSL [2015/12/15] Added a convenience script e-acsl-gcc.sh for
+ small runs of the E-ACSL plugin.
-* E-ACSL [2015/12/08] Fix bug #1817 about incorrect initialization of
literal strings in global arrays with compound initializers.
-* E-ACSL [2015/11/06] Fix a crash occuring when using a recent libc
diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
new file mode 100644
index 0000000000000000000000000000000000000000..225328400351a88367c80bf433100e4a7e82b4aa
--- /dev/null
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -0,0 +1,179 @@
+.\"
+.\"
+.\" 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 a convenience wrapper for instrumentation of C programs using the
+\fBE-ACSL\fP \fBFrama-C\fP plugin and their subsequent compilation using
+the GNU compiler collection (\fBGCC\fP).
+.SH OPTIONS
+.TP
+.B -h, --help
+show a help page.
+.TP
+.B -c, --compile
+compile the generated and the original (supplied) sources.
+By default no compilation is performed.
+.TP
+.B -C, --compile-only
+compile the input files as if they were generated by \fBE-ACSL\fP.
+.TP
+.B -p, --print
+output the code generated by E-ACSL to \fISTDOUT\fP using rich formatting
+features enabled via \fBpygmentize\fP. If no \fBpygmentize\fP
+executable is found in the system path, the generated sources are
+printed as is using the \fBcat\fP command.
+.TP \fI \fP
+.B -d, --debug=\fI<N>
+pass a value to the \fBFrama-C\fP -\fIdebug\fP option.
+By default the -\fIdebug\fP flag is unused.
+.TP
+.B -v, --verbose=\fI<N>
+pass a value to the \fBFrama-C\fP -\fIverbose\fP option.
+By default the -\fIverbose\fP flag is unused.
+.TP
+.B -o, --ocode=\fI<FILE>
+output the \fBE-ACSL\fP instrumented code to \fI<FILE>\fP.
+Defaults to \fIa.out.frama.c\fP.
+.TP
+.B -O, --oexec=\fI<FILE>
+output the code compiled from the uninstrumented sources to \fI<FILE>\fP.
+The executable compiled from the files generated by \fBE-ACSL\fP is
+appended the \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 -f, --frama-c-only
+run input source files through \fBFrama-C\fP without \fBE-ACSL\fP instrumentations.
+.TP
+.B -E, --extra-cpp-args=\fI<FLAGS>
+pass additional arguments to the \fBFrama-C\fP pre-processor.
+.TP
+.B -L, --frama-c-stdlib
+use the \fBFrama-C\fP standard library instead of a system-wide one.
+.TP
+.B -M, --full-mmodel
+maximize memory-related instrumentation.
+.TP
+.B -g, --gmp
+always use GMP integers instead of C integral types.
+By default the GMP integers are used on as-needed basis.
+.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 pre-processor flags see \fB--extra-cpp-args\fP option.
+.TP
+.B -q, --quiet
+suppress any output except for errors and warnings.
+.TP
+.B -s, --logfile=\fI<FILE>
+redirect all output to a given file.
+.TP
+.B -F, --frama-c-extra=\fI<FLAGS>
+pass an extra option to a \fBFrama-C\fP invocation.
+.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.
+
+Valid arguments are:
+ \fIbittree\fP \- memory modelling using a Patricia trie ADT.
+ \fIsplay_tree\fP \- memory modelling using a splay tree ADT.
+ \fIlist\fP \- memory modelling using a linked-list ADT.
+ \fItree\fP \- memory modelling using a binary tree ADT.
+
+By default the Patricia trie memory model is used.
+.TP
+.B -P, --production
+generate an optimized executable with all debug features disabled.
+Unoptimized executables (default) may lead to a significant
+performance slowdown.
+.TP
+.B -N, --no-stdlib
+if specified the \fBE-ACSL\fP runtime library uses custom
+implementations of standard library functions (such as \fBmemset\fP).
+By default \fBGCC\fP builtins are used (e.g., \fB__builtin_memset\fP).
+.TP
+.B -D, --debug-log=\fI<FILE>
+the name of the file for logging of the debugging output of
+modified executables. If '-' is specified then the
+output is redirected to \fISTDERR\fP. By default
+the debug output is redirected to
+\fI/tmp/e-acsl.log\fP. This option is only meaningful
+in the absence of the \fB-P\fP flag that disables debug logging for
+performance reasons.
+.TP
+.B -I, --frama-c=\fI<FILE>
+the name of the \fBFrama-C\fP executable. By default the
+first \fIframa-c\fP executable found in the system path is used.
+.TP
+.B -G, --gcc=\fI<FILE>
+the name of the \fBGCC\fP executable. By default the first \fIgcc\fP
+executable found in the system path is used.
+
+.SH EXIT STATUS
+.TP
+.B 0
+Successful execution
+.TP
+.B 1
+Invalid user input
+.TP
+.B \fBFrama-C\fP or \fBGCC\fP error code
+Instrumentation- or compile-time error
+
+.SH EXAMPLES
+
+.B e-acsl-gcc.sh foo.c
+
+Instrument foo.c and output the instrumented code to \fIa.out.frama.c\fP.
+
+.B e-acsl-gcc.sh -P -c -ogen_foo.c -Ofoo 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 --memory-model=splay_tree -C gen_foo.c
+
+Assume \fIgen_foo.c\fP has been instrumented by \fBE-ACSL\fP and compile it into
+\fIa.out.e-acsl\fP using \fBsplay_tree\fP memory model.
+
+.SH SEE ALSO
+\fBgcc\fP(1), \fBcpp\fP(1), \fBld\fP(1), \fBframa-c\fP(1)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index dae2bc058f46bdb1c0fd7a49dc1fdf08737adbc0..f1b8bee53f38e1b9f61c94befbe33df772a028a7 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -33,149 +33,76 @@ error () {
fi
}
-# Check if an executable can be found by in the PATH
+# Check if a given executable name 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 if a given executable name is indeed an executable or can be found
+# in the $PATH. Abort the execution if not.
check_tool() {
- has_tool "$1" && echo "$1" \
- || error "Cannot find '$1' executable in the \$PATH"
+ { has_tool "$1" || test -e "$1"; } || error "No executable $1 found";
}
# 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,quiet,logfile:,
- ld-flags:,cpp-flags:,frama-c-extra:"
-SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g,q,s:,F:"
+ 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:"
+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:"
# Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:"
-# 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.
-MACHDEPFLAGS="`getconf LONG_BIT`"
-# Check if getconf gives out the value accepted by Frama-C/GCC
-echo "$MACHDEPFLAGS" | grep '16\|32\|64' \
- || error "$MACHDEPFLAGS-bit architecture not supported"
-# -machdep option sent to frama-c
-MACHDEP="-machdep gcc_x86_$MACHDEPFLAGS"
-# Macro for correct preprocessing of Frama-C generated code
-CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
-# GCC machine option
-GCCMACHDEP="-m$MACHDEPFLAGS"
-
-# Gcc
-CC="`check_tool 'gcc'`"
-CFLAGS="-std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin -Wall \
- -Wno-long-long \
- -Wno-attributes \
- -Wno-unused-result \
- -Wno-unused-value \
- -Wno-unused-function \
- -Wno-unused-variable \
- -Wno-unused-but-set-variable \
- -Wno-implicit-function-declaration \
- -Wno-attributes"
-CPPFLAGS=""
-LDFLAGS=""
-# Frama-C
-FRAMAC="`check_tool 'frama-c'`"
-FRAMAC_CONGIG="`check_tool 'frama-c-config'`"
-FRAMAC_FLAGS="-implicit-function-declaration ignore"
-
-# E-ACSL source that needed for compilation
-FRAMA_C_SHARE="`$FRAMAC_CONGIG -print-share-path`"
-EACSL_SHARE="$FRAMA_C_SHARE/e-acsl"
-RTL="$EACSL_SHARE/e_acsl.c \
- $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
- $EACSL_SHARE/memory_model/e_acsl_bittree.c \
-"
-
-# 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_FRAMAC_EXTRA= # Extra Frama-C options
+OPTION_CFLAGS= # Compiler flags
+OPTION_CPPFLAGS= # Preprocessor flags
+OPTION_LDFLAGS= # Linker flags
+OPTION_FRAMAC="frama-c" # Frama-C executable name
+OPTION_CC="gcc" # GCC executable name
OPTION_ECHO="set -x" # Echo executed commands to STDOUT
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_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_OUTPUT_CODE="a.out.frama.c" # Name of the translated file
+OPTION_OUTPUT_EXEC="a.out" # Generated executable name
OPTION_EACSL="-e-acsl -then-last" # 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
+OPTION_DEBUG_MACRO="-DE_ACSL_DEBUG" # Debug macro
+OPTION_DEBUG_LOG_MACRO="" # Specification of debug log file
+OPTION_FRAMAC_CPP_EXTRA="" # Extra CPP flags for Frama-C
+OPTION_EACSL_MMODEL="bittree" # Memory model used
+# The following option controls whether to use gcc builtins
+# (e.g., __builtin_strlen) in RTL or fall back to custom implementations
+# of standard functions.
+OPTION_BUILTINS="-DE_ACSL_BUILTINS"
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 " -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)"
- 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 ""
- 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
+ -l pass additional options to the linker
+ -e pass additional options to the pre-preprocessor
+ -E pass additional arguments to the Frama-C pre-processor
+ -p output the generated code with rich formatting to STDOUT
+ -o <file> output the generated code to <file> [a.out.frama.c]
+ -O <file> output the generated executables to <file> [a.out, a.out.e-acsl]
+ -M maximise memory-related instrumentation
+ -g always use GMP integers instead of C integral types
+ -q suppress any output except for errors and warnings
+ -s <file> redirect all output to <file>
+ -P compile executable without debug features
+ -I <file> specify Frama-C executable [frama-c]
+ -G <file> specify C compiler executable [gcc]
+
+Notes:
+ This help page shows only basic options.
+ See man (1) e-acsl-gcc.sh for full up-to-date documentation.\n"
exit 1
}
@@ -217,16 +144,16 @@ do
;;
# Redirect all output to a given file
--logfile|-s)
- shift;
- exec > $1
- exec 2> $1
- shift;
+ shift;
+ exec > $1
+ exec 2> $1
+ shift;
;;
- # Pass an option to a frama-c invocation
+ # Pass an option to a Frama-C invocation
--frama-c-extra|-F)
- shift;
- OPTION_FRAMAC_EXTRA="$OPTION_FRAMAC_EXTRA $1"
- shift;
+ shift;
+ FRAMAC_FLAGS="$FRAMAC_FLAGS $1"
+ shift;
;;
# Do compile instrumented code
--compile|-c)
@@ -262,32 +189,32 @@ do
# code is to be written
--ocode|-o)
shift;
- OPTION_OCODE="$1"
+ OPTION_OUTPUT_CODE="$1"
shift
;;
# Specify the base name of the executable generated from the
# instrumented and non-instrumented sources.
--oexec|-O)
shift;
- OPTION_OEXEC="$1"
+ OPTION_OUTPUT_EXEC="$1"
shift
;;
# Additional CPP arguments
--extra-cpp-args|-E)
shift;
- OPTION_EXTRA_CPP="$OPTION_EXTRA_CPP$1"
+ OPTION_FRAMAC_CPP_EXTRA="$OPTION_FRAMAC_CPP_EXTRA $1"
shift;
;;
# Additional flags passed to the linker
--ld-flags|-l)
shift;
- LDFLAGS="$LDFLAGS $1"
+ OPTION_LDFLAGS="$OPTION_LDFLAGS $1"
shift;
;;
# Additional flags passed to the pre-processor (compile-time)
--cpp-flags|-e)
shift;
- CPPFLAGS="$CPPFLAGS $1"
+ OPTION_CPPFLAGS="$OPTION_CPPFLAGS $1"
shift;
;;
# Do not perform the instrumentation, only compile the provided sources
@@ -298,16 +225,11 @@ do
OPTION_INSTRUMENT=
OPTION_COMPILE="1"
;;
- # Run only frama-c related instrumentation
+ # 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;
@@ -323,23 +245,131 @@ do
shift;
OPTION_GMP="-e-acsl-gmp-only"
;;
+ -P|--production)
+ shift;
+ OPTION_DEBUG_MACRO=""
+ ;;
+ -N|--no-stdlib)
+ shift;
+ OPTION_BUILTINS=""
+ ;;
+ -D|--debug-log)
+ shift;
+ OPTION_DEBUG_LOG_MACRO="-DE_ACSL_DEBUG_LOG=$1"
+ shift;
+ ;;
+ # Supply Frama-C executable name
+ -I|--frama-c)
+ shift;
+ OPTION_FRAMAC="$1"
+ shift;
+ ;;
+ # Supply GCC executable name
+ -G|--gcc)
+ shift;
+ OPTION_CC="$1"
+ shift;
+ ;;
+ # A memory model to link against
+ -m|--memory-model)
+ shift;
+ echo $1 | grep "\(tree\|bittree\|splay_tree\|list\)"
+ error "no such memory model: $1" $?
+ OPTION_EACSL_MMODEL="$1"
+ shift;
+ ;;
esac
done
shift;
# Bail if no files to translate are given
-if test -z "$1"; then
+if [ -z "$1" ]; then
error "no input files";
fi
+# 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.
+MACHDEPFLAGS="`getconf LONG_BIT`"
+# Check if getconf gives out the value accepted by Frama-C/GCC
+echo "$MACHDEPFLAGS" | grep '16\|32\|64' 2>&1 >/dev/null \
+ || error "$MACHDEPFLAGS-bit architecture not supported"
+# -machdep option sent to Frama-C
+MACHDEP="-machdep gcc_x86_$MACHDEPFLAGS"
+# Macro for correct preprocessing of Frama-C generated code
+CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
+# GCC machine option
+GCCMACHDEP="-m$MACHDEPFLAGS"
+
+# Check if Frama-C and GCC executable names
+check_tool "$OPTION_FRAMAC"
+check_tool "$OPTION_CC"
+
+# Frama-C and related flags
+FRAMAC="$OPTION_FRAMAC"
+FRAMAC_FLAGS=""
+FRAMAC_SHARE="`$FRAMAC -print-share-path`"
+FRAMAC_CPP_EXTRA="
+ $OPTION_FRAMAC_CPP_EXTRA
+ -D$EACSL_MACRO_ID
+ -I$FRAMAC_SHARE/libc
+ $CPPMACHDEP"
+EACSL_SHARE="$FRAMAC_SHARE/e-acsl"
+EACSL_MMODEL="$OPTION_EACSL_MMODEL"
+
+# 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
+ -std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin
+ -Wall \
+ -Wno-long-long \
+ -Wno-attributes \
+ -Wno-unused \
+ -Wno-unused-function \
+ -Wno-unused-result \
+ -Wno-unused-value \
+ -Wno-unused-function \
+ -Wno-unused-variable \
+ -Wno-unused-but-set-variable \
+ -Wno-implicit-function-declaration \
+ -Wno-unknown-warning-option \
+ -Wno-extra-semi \
+ -Wno-tautological-compare \
+ -Wno-gnu-empty-struct \
+ -Wno-incompatible-pointer-types-discards-qualifiers \
+ -Wno-empty-body"
+CPPFLAGS="$OPTION_CPPFLAGS"
+LDFLAGS="$OPTION_LDFLAGS"
+
+# C, CPP and LD flags for compilation of E-ACSL-generated sources
+EACSL_CFLAGS=""
+EACSL_CPPFLAGS="
+ -I$EACSL_SHARE
+ -D$EACSL_MACRO_ID
+ -D__FC_errno=(*__errno_location())"
+EACSL_LDFLAGS="-lgmp -lm"
+# Memory model sources
+EACSL_RTL="$EACSL_SHARE/e_acsl.c \
+ $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
+ $EACSL_SHARE/memory_model/e_acsl_$OPTION_EACSL_MMODEL.c"
+
+# Output file names
+OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source
+OUTPUT_EXEC="$OPTION_OUTPUT_EXEC" # Output name of the original executable
+# Output name of E-ACSL-modified executable
+EACSL_OUTPUT_EXEC="$OPTION_OUTPUT_EXEC.e-acsl"
+
# Instrument
if [ -n "$OPTION_INSTRUMENT" ]; then
($OPTION_ECHO; \
$FRAMAC \
$FRAMAC_FLAGS \
$MACHDEP \
- $OPTION_FRAMAC_EXTRA \
- -cpp-extra-args="$OPTION_EXTRA_CPP" \
+ -cpp-extra-args="$OPTION_FRAMAC_CPP_EXTRA" \
-e-acsl-share $EACSL_SHARE \
$OPTION_VERBOSE \
$OPTION_DEBUG \
@@ -349,27 +379,36 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
"$@" \
$OPTION_EACSL \
-print \
- -ocode "$OPTION_OCODE");
- error "aborted by frama-c" $?;
+ -ocode "$OPTION_OUTPUT_CODE");
+ error "aborted by Frama-C" $?;
# Print translated code
if [ -n "$OPTION_PRINT" ]; then
- $CAT $OPTION_OCODE
+ $CAT $OPTION_OUTPUT_CODE
fi
fi
# Compile
-if test -n "$OPTION_COMPILE" ; then
+if [ -n "$OPTION_COMPILE" ]; then
# Compile the 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
- ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS "$@" -o "$OPTION_OEXEC" $LDFLAGS);
+ ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS "$@" -o "$OUTPUT_EXEC" $LDFLAGS);
error "fail to compile/link un-instrumented code: $@" $?;
else
- OPTION_OCODE="$@"
+ OUTPUT_CODE="$@"
fi
# Compile and link E-ACSL-instrumented file
- ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS $EACSL_CPP_FLAGS $RTL \
- "$OPTION_OCODE" -o "$OPTION_OEXEC.e-acsl" $LDFLAGS $EACSL_LD_FLAGS)
+ ($OPTION_ECHO;
+ $CC \
+ $CFLAGS $CPPFLAGS \
+ $EACSL_CFLAGS $EACSL_CPPFLAGS \
+ $EACSL_RTL \
+ $OPTION_DEBUG_MACRO \
+ $OPTION_DEBUG_LOG_MACRO \
+ $OPTION_BUILTINS \
+ -o "$EACSL_OUTPUT_EXEC" \
+ "$OUTPUT_CODE" \
+ $LDFLAGS $EACSL_LDFLAGS)
error "fail to compile/link instrumented code: $@" $?;
fi
exit 0;
diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
new file mode 100755
index 0000000000000000000000000000000000000000..ab14bb1b24a55a437732edfe490df57dff0a475a
--- /dev/null
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -0,0 +1,110 @@
+##########################################################################
+# #
+# This file is part of the Frama-C's E-ACSL plug-in. #
+# #
+# Copyright (C) 2012-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 license/LGPLv2.1). #
+# #
+##########################################################################
+
+#!/bin/sh -e
+
+# Convenience script for running tests with E-ACSL. Given a source file the
+# sequence is as follows:
+# 1. Perform E-ACSL instrumentation
+# 2. Compile instrumented and original files
+# 3. Compare outputs of the above
+
+# Arguments:
+# $1 - base name of the source file to use excluding an
+# extension (e.g., addrOf)
+# $2 - base name of the test suite directory the test file is located in.
+# (for instance e-acsl-runtime). Provided that ROOT is the directory
+# holding the E-ACSL repository there should be either:
+# $ROOT/test/e-acsl-runtime/addrOf.i or
+# $ROOT/test/e-acsl-runtime/addrOf.c
+# $3 - if specified this script re-runs test sequence generating using
+# -e-acsl-gmp-only option
+# $4 - debug flag
+
+set -e
+
+TEST="$1" # Based name of the test file with extension stripped
+PREFIX="$2" # Prefix (test suite) directory, e.g., bts, e-acsl-runtime
+GMP="$3" # Whether to use a subsequent run with -e-acsl-gmp-only
+DEBUG="$4" # Debug flag
+
+ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository
+TESTDIR="$ROOTDIR/tests/$PREFIX"
+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 output
+RUNS=1
+
+# Error reporting
+error() {
+ echo "Error: $1" 1>&2
+ echo "See $2 for details" 1>&2
+ exit 1
+}
+
+# Clean up log/output files unless the DEBUG flag is set
+clean() {
+ if [ -z "$DEBUG" ]; then
+ rm -f $LOG.* $OUT.*
+ fi
+}
+
+ # Do clean up on exit
+trap "clean" EXIT HUP INT QUIT TERM
+
+# Instrument the given test using e-acsl-gcc.sh and compare outputs of the
+# executables generated from instrumented and non-instrumented sources
+run_test() {
+ local ocode=$OUT.$RUNS.c # Generated source file
+ 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
+
+ # Command for instrumenting the source file and compiling the original
+ # and the instrumented code
+ EACSL_GCC="e-acsl-gcc.sh
+ --compile $TESTFILE --ocode=$ocode --logfile=$logfile
+ --memory-model=$MODEL --oexec=$oexec $extra"
+
+ $EACSL_GCC || error "Command $EACSL_GCC failed" "$logfile"
+
+ # Log outputs of the generated executables
+ $oexec 2>&1 > $oexeclog.native
+ $oexec.e-acsl 2>&1 > $oexeclog.e-acsl
+
+ ## Make sure that instrumented and uninstrumented programs have same outputs
+ diff $oexeclog.native $oexeclog.e-acsl ||
+ error "Output of programs before and after instrumentation differ" \
+ "output of $oexec and $oexec.e-acsl"
+
+ RUNS=$((RUNS+1))
+}
+
+run_test
+if test -n "$GMP"; then
+ run_test "--gmp"
+fi
+exit 0