Skip to content
Snippets Groups Projects
Commit 30ff4e8b authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Added -q|--quiet option to e-acsl for quiet executions that output only

errors or warnings
parent 8f663dc7
No related branches found
No related tags found
No related merge requests found
...@@ -46,9 +46,9 @@ check_tool() { ...@@ -46,9 +46,9 @@ check_tool() {
# Getopt options # Getopt options
LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:, \ LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:, \
frama-c-only,extra-cpp-args,rtl,frama-c-stdlib,full-mmodel,gmp, frama-c-only,extra-cpp-args,rtl,frama-c-stdlib,full-mmodel,gmp,quiet,
ld-flags:,cpp-flags:" ld-flags:,cpp-flags:"
SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g" SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g,q"
# Prefix for an error message due to wrong arguments # Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:" ERROR="ERROR parsing arguments:"
...@@ -105,6 +105,7 @@ EACSL_CPP_FLAGS=" ...@@ -105,6 +105,7 @@ EACSL_CPP_FLAGS="
EACSL_LD_FLAGS="-lgmp -lm" EACSL_LD_FLAGS="-lgmp -lm"
# Variables holding getopt options # Variables holding getopt options
OPTION_ECHO="set -x" # Echo executed commands to STDOUT
OPTION_INSTRUMENT=1 # Perform E-ACSL instrumentation OPTION_INSTRUMENT=1 # Perform E-ACSL instrumentation
OPTION_PRINT= # Output instrumented code OPTION_PRINT= # Output instrumented code
OPTION_DEBUG= # Set frama-c debug flag OPTION_DEBUG= # Set frama-c debug flag
...@@ -162,6 +163,8 @@ manpage() { ...@@ -162,6 +163,8 @@ manpage() {
echo " pass the specified flags to the linker" echo " pass the specified flags to the linker"
echo " -e, --cpp-flags <FLAGS>" echo " -e, --cpp-flags <FLAGS>"
echo " pass the specified flags to the pre-processor (compile-time)" echo " pass the specified flags to the pre-processor (compile-time)"
echo " -q, --quiet"
echo " suppress any output except for errors and warnings"
echo "" echo ""
echo "EXAMPLES:" echo "EXAMPLES:"
echo " # Instrument foo.c and output the instrumented code to a.out.frama.c" echo " # Instrument foo.c and output the instrumented code to a.out.frama.c"
...@@ -203,6 +206,13 @@ do ...@@ -203,6 +206,13 @@ do
shift; shift;
manpage; manpage;
;; ;;
# Do not echo commands to STDOUT
--quiet|-q)
shift;
OPTION_ECHO=
OPTION_DEBUG="-debug 0"
OPTION_VERBOSE="-verbose 0"
;;
# Do compile instrumented code # Do compile instrumented code
--compile|-c) --compile|-c)
shift; shift;
...@@ -309,7 +319,7 @@ fi ...@@ -309,7 +319,7 @@ fi
# Instrument # Instrument
if [ -n "$OPTION_INSTRUMENT" ]; then if [ -n "$OPTION_INSTRUMENT" ]; then
(set -x; \ ($OPTION_ECHO; \
$FRAMAC \ $FRAMAC \
$FRAMAC_FLAGS \ $FRAMAC_FLAGS \
$MACHDEP \ $MACHDEP \
...@@ -336,14 +346,14 @@ if test -n "$OPTION_COMPILE" ; then ...@@ -336,14 +346,14 @@ if test -n "$OPTION_COMPILE" ; then
# Compile the original files only if the instrumentation option is given, # Compile the original files only if the instrumentation option is given,
# otherwise the provided sources are assumed to be E-ACSL instrumented files # otherwise the provided sources are assumed to be E-ACSL instrumented files
if [ -n "$OPTION_INSTRUMENT" ]; then if [ -n "$OPTION_INSTRUMENT" ]; then
(set -x; $CC $CPPFLAGS $CFLAGS "$@" -o "$OPTION_OEXEC" $LDFLAGS); ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS "$@" -o "$OPTION_OEXEC" $LDFLAGS);
error "fail to compile/link un-instrumented code" $?; error "fail to compile/link un-instrumented code: $@" $?;
else else
OPTION_OCODE="$@" OPTION_OCODE="$@"
fi fi
# Compile and link E-ACSL-instrumented file # Compile and link E-ACSL-instrumented file
(set -x; $CC $CPPFLAGS $CFLAGS $EACSL_CPP_FLAGS $RTL \ ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS $EACSL_CPP_FLAGS $RTL \
"$OPTION_OCODE" -o "$OPTION_OEXEC.e-acsl" $LDFLAGS $EACSL_LD_FLAGS) "$OPTION_OCODE" -o "$OPTION_OEXEC.e-acsl" $LDFLAGS $EACSL_LD_FLAGS)
error "fail to compile/link instrumented code" $?; error "fail to compile/link instrumented code: $@" $?;
fi fi
exit 0; exit 0;
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment