From 8f663dc750aaf08de5e39c74f20a710b63d95f11 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 16 Dec 2015 13:05:46 +0100
Subject: [PATCH] Added Examples section for the help page of
e-acsl-gcc.sh
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 26 +++++++++++++++++-------
1 file changed, 19 insertions(+), 7 deletions(-)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 44e3e1ec2a1..76074ab1fc8 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -112,7 +112,7 @@ 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_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
@@ -123,8 +123,10 @@ manpage() {
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 ""
echo "SYNOPSIS"
echo " e-acsl-gcc <OPTIONS> <C-FILES>"
+ echo ""
echo "OPTIONS"
echo " -h, --help"
echo " show this help page"
@@ -137,9 +139,11 @@ manpage() {
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 " name of the output source file, defaults to a.out.frama.c"
echo " -O, --oexec <FILENAME>"
- echo " name of the compiled executable"
+ 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"
@@ -158,6 +162,16 @@ manpage() {
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 ""
+ 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"
exit 1
}
@@ -310,7 +324,6 @@ if [ -n "$OPTION_INSTRUMENT" ]; then
$OPTION_EACSL \
-print \
-ocode "$OPTION_OCODE");
- # Hard abort based on the return code as the above runs in a subshell
error "aborted by frama-c" $?;
# Print translated code
if [ -n "$OPTION_PRINT" ]; then
@@ -320,9 +333,8 @@ 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
+ # 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
(set -x; $CC $CPPFLAGS $CFLAGS "$@" -o "$OPTION_OEXEC" $LDFLAGS);
error "fail to compile/link un-instrumented code" $?;
--
GitLab