From 16d511f3bb0da60dff1a7117fa19eec8e2fc0547 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Thu, 4 Feb 2016 09:39:39 +0100
Subject: [PATCH] e-acscl wrapper: - Added man page - Fixed memory
model option
---
src/plugins/e-acsl/Makefile.in | 4 +
src/plugins/e-acsl/man/e-acsl-gcc.sh.1 | 162 +++++++++++++++++++++++
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 112 ++++------------
3 files changed, 192 insertions(+), 86 deletions(-)
create mode 100644 src/plugins/e-acsl/man/e-acsl-gcc.sh.1
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index e41aa41b752..8874c6b9bb5 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/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] \
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 00000000000..67d45782fcd
--- /dev/null
+++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1
@@ -0,0 +1,162 @@
+.\"
+.\"
+.\" 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)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index c481794321d..5b4db819505 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/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 \
--
GitLab