From 466e88a60f5690c063d98e27fa8d61046aeacde6 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 16 Dec 2015 11:00:09 +0100
Subject: [PATCH] Adjustment of the executable script for e-acsl runs: -
Renamed to e-acsl-gcc.sh - BUGFIX: Clean abort on frama-c/gcc failures
- Use an explicit list of disabled warnings instead of plain '-w' for
gcc runs
---
.../scripts/{e-acsl-gcc => e-acsl-gcc.sh} | 25 +++++++++++++++----
1 file changed, 20 insertions(+), 5 deletions(-)
rename src/plugins/e-acsl/scripts/{e-acsl-gcc => e-acsl-gcc.sh} (93%)
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
similarity index 93%
rename from src/plugins/e-acsl/scripts/e-acsl-gcc
rename to src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index 3f99ceb4b8f..d8f6ea47380 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -24,10 +24,13 @@
# Convenience wrapper for small runs of E-ACSL Frama-C plugin
-# Print a message to STDERR and exit
+# Print a message to STDERR and exit. If the second argument (exit code)
+# if provided and it is '0' then do nothing.
error () {
- echo "e-acsl-gcc: fatal error: $1" 1>&2
- exit 1;
+ if [ -z "$2" ] || ! [ "$2" = 0 ]; then
+ echo "e-acsl-gcc: fatal error: $1" 1>&2
+ exit 1;
+ fi
}
# Check if an executable can be found by in the PATH
@@ -51,7 +54,15 @@ ERROR="ERROR parsing arguments:"
# Gcc
CC="`check_tool 'gcc'`"
-CFLAGS="-std=c99 -w -g3 -O2 -fno-builtin"
+CFLAGS="-std=c99 -g3 -O2 -fno-builtin -Wall \
+ -Wno-long-long \
+ -Wno-attributes \
+ -Wno-unused-result \
+ -Wno-unused-value \
+ -Wno-unused-variable \
+ -Wno-unused-but-set-variable \
+ -Wno-implicit-function-declaration \
+ -Wno-attributes"
CPPFLAGS=""
LDFLAGS=""
# Frama-C
@@ -298,6 +309,8 @@ 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
$CAT $OPTION_OCODE
@@ -310,12 +323,14 @@ if test -n "$OPTION_COMPILE" ; then
# 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)
+ (set -x; $CC $CPPFLAGS $CFLAGS "$@" -o "$OPTION_OEXEC" $LDFLAGS);
+ error "fail to compile/link un-instrumented code" $?;
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)
+ error "fail to compile/link instrumented code" $?;
fi
exit 0;
--
GitLab