Merge branch 'fix/andre/creduce-script' into 'master'

[analysis-scripts] fixes for creduce script

See merge request frama-c/frama-c!4689

share/analysis-scripts/creduce.sh

-#!/bin/bash -e
+#!/bin/bash -eu
 ##########################################################################
 #                                                                        #
 #  This file is part of Frama-C.                                         #
@@ -110,17 +110,17 @@ dir_for_reduction="creducing"
 
 script_for_creduce="./script_for_creduce.sh"
 
-if [ -z "$CREDUCE" ]; then
+if [ -z "${CREDUCE+x}" ]; then
     # Now some distributions have 'cvise' instead of 'creduce', so try it
     # if found in PATH
-    if command -v cvise 2>&1 >/dev/null; then
+    if command -v cvise >/dev/null 2>&1; then
         CREDUCE="cvise"
     else
         CREDUCE="creduce"
     fi
 fi
 
-if ! command -v "$CREDUCE" 2>&1 >/dev/null; then
+if ! command -v "$CREDUCE" >/dev/null 2>&1; then
     echo "cvise/creduce not found; install it in the PATH or"
     echo "put it in environment variable CREDUCE."
     exit 1
@@ -137,7 +137,7 @@ for f in "$@"; do
         too_many_sources+=" $f"
     fi
 done
-if [ ! -z "$too_many_sources" ]; then
+if [ -n "$too_many_sources" ]; then
     echo "error: too many sources; only the first argument must be a file: $file"
     echo "       remove these from the command-line:$too_many_sources"
     exit 1
@@ -149,7 +149,7 @@ if [[ $(dirname "$file") = "$dir_for_reduction" ]]; then
     exit 1
 fi
 
-if [ -z "$FRAMAC_BIN" ]; then
+if [ -z "${FRAMAC_BIN+x}" ]; then
     if ! command -v "frama-c" >/dev/null; then
         echo "error: frama-c must be in the PATH, or FRAMAC_BIN must point to"
         echo "       the directory containing the frama-c binary"
@@ -161,7 +161,7 @@ else
 fi
 echo "[info] using FRAMAC: $FRAMAC"
 
-if [ -z "$FRAMAC_LIB" ]; then
+if [ -z "${FRAMAC_LIB+x}" ]; then
     FRAMAC_LIB="$("$FRAMAC" -print-lib-path)"
 fi
 
@@ -182,7 +182,7 @@ fi
 #
 #### End of command-line and environment validation
 
-if [[ ! "$options" =~ no-autoload-plugins ]]; then
+if [[ ! "$*" =~ no-autoload-plugins ]]; then
     echo "********************************************************************"
     echo "Hint: consider using -no-autoload-plugins -load-module [modules]"
     echo "      for faster reduction"
@@ -208,7 +208,7 @@ else
     cpp_retcode=$?
     set -e
     if [ $cpp_retcode -ne 0 ]; then
-        echo "error trying to get preprocessing flags (exit code: $cpp_retcode): $FRAMAC -print-cpp-commands $@ $file"
+        echo "error trying to get preprocessing flags (exit code: $cpp_retcode): $FRAMAC -print-cpp-commands $* $file"
         exit $cpp_retcode
     fi
     CPP=$(echo "$cpp_output" | \
@@ -237,9 +237,11 @@ if [ ! -e "$script_for_creduce" ]; then
     case $errorkind in
         1)
             cp "$FRAMAC_LIB/analysis-scripts/script_for_creduce_fatal.sh" "$script_for_creduce"
+            chmod +w "$script_for_creduce"
             ;;
         2)
             cp "$FRAMAC_LIB/analysis-scripts/script_for_creduce_non_fatal.sh" "$script_for_creduce"
+            chmod +w "$script_for_creduce"
             echo "Script copied. Please edit $script_for_creduce and re-run this script."
             exit 0
             ;;
@@ -267,7 +269,7 @@ else
 fi
 "$SED" -i "s|@FRAMAC@|$FRAMAC|g" "$script_for_creduce"
 "$SED" -i "s|@BASE@|$base|g" "$script_for_creduce"
-"$SED" -i "s|@FCFLAGS@|$(echo $@ | tr "'" "\\'")|g" "$script_for_creduce"
+"$SED" -i "s|@FCFLAGS@|$(echo "$@" | tr "'" "\\'")|g" "$script_for_creduce"
 chmod u+x "$script_for_creduce"
 
 trap '{ echo "Creduce interrupted!"; echo ""; echo "(partially) reduced file: $dir_for_reduction/$base"; exit 0; }' SIGINT
@@ -286,7 +288,7 @@ if [ $? -ne 0 ]; then
     echo "       check the options given to Frama-C."
     echo "       If you edited '$script_for_creduce', check it as well."
     echo ""
-    if [ $(wc -l /tmp/script_for_creduce.out | cut -d' ' -f1) -gt 20 ]; then
+    if [ "$(wc -l /tmp/script_for_creduce.out | cut -d' ' -f1)" -gt 20 ]; then
         echo "# Script output (first 20 lines):"
         head -n 20 /tmp/script_for_creduce.out
         echo "(...) [truncated; full output in /tmp/script_for_creduce.out]"
@@ -298,6 +300,10 @@ if [ $? -ne 0 ]; then
 fi
 set -e
 
+# CREDUCE_OPTIONS may not have been defined
+# Note: the absence of double quotes around $CREDUCE_OPTIONS below is
+# intentional, to allow passing multiple options
+CREDUCE_OPTIONS=${CREDUCE_OPTIONS:-}
 "$CREDUCE" $CREDUCE_OPTIONS script_for_creduce.sh "$base"
 
 echo "Finished reducing file: $dir_for_reduction/$base"

share/analysis-scripts/script_for_creduce_fatal.sh

@@ -29,10 +29,11 @@
 set +e
 "@FRAMAC@" "@BASE@" @FCFLAGS@
 retcode=$?
+set -e
+
 # see cmdline.ml for the different exit codes returned by Frama-C
-if [ $retcode -eq 125 -o $retcode -eq 4 ]; then
+if [ $retcode -eq 125 ] || [ $retcode -eq 4 ]; then
     exit 0
 else
     exit 1
 fi
-set -e

share/analysis-scripts/script_for_creduce_non_fatal.sh

@@ -32,7 +32,7 @@ fc_out=$(mktemp creduce_fc_XXXXXX.log)
 
 # We always check that the reduced file remains valid C code.
 set -o pipefail
-@CPP@ "@BASE@" 2>&1 | tee $cc_out
+@CPP@ "@BASE@" 2>&1 | tee "$cc_out"
 set +o pipefail
 
 ### Examples of conditions to be maintained by C-Reduce; copy and adapt
@@ -49,10 +49,12 @@ set +o pipefail
 
 ##########
 
+set +e # allow Frama-C to fail so we can retrieve its exit code
 set -o pipefail
-"@FRAMAC@" "@BASE@" @FCFLAGS@ 2>&1 | tee $fc_out
-fc_retcode=$(echo ${PIPESTATUS[0]})
+"@FRAMAC@" "@BASE@" @FCFLAGS@ 2>&1 | tee "$fc_out"
+fc_retcode=${PIPESTATUS[0]}
 set +o pipefail
+set -e
 
 ### Examples of conditions to be maintained by C-Reduce; copy and adapt
 #
@@ -69,4 +71,4 @@ set +o pipefail
 ##########
 
 ### Cleanup
-rm -f $cc_out $fc_out
+rm -f "$cc_out" "$fc_out"