diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index 76af3b546dc557401a59d546874cca65a347db5b..a284c18a55469e190c3a1f9eb59e248689b775e2 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -21,10 +21,12 @@ # configure configure ############################################################################### -############################# -Plugin E-ACSL 24.0 (Chromium) -############################# +############################ +Plugin E-ACSL <next-release> +############################ +-* e-acsl-gcc [2021-11-22] Fix e-acsl-gcc.sh detection of failures in + subcommands. - E-ACSL [2021-11-03] Improve runtime debug logs: the %a modifier now outputs in hexadecimal, the debug logs now all end in new lines, the trace now outputs to stderr. @@ -33,6 +35,11 @@ Plugin E-ACSL 24.0 (Chromium) have been adjusted to what was effectively used. -* E-ACSL [2021-11-03] Now the same Frama-C options are used when parsing the user sources and the E-ACSL's RTL. + +############################# +Plugin E-ACSL 24.0 (Chromium) +############################# + - E-ACSL [2021-10-20] Add option -e-acsl-assert-print-data (--assert-print-data in e-acsl-gcc.sh) to print data contributing to a failed assertion along with the error message. diff --git a/src/plugins/e-acsl/doc/refman/changes_modern.tex b/src/plugins/e-acsl/doc/refman/changes_modern.tex index 770c70c1af1d699ba3e671e938cc1e6939414b90..3e7e104758318f6448f261ddcb560e5ecab516f9 100644 --- a/src/plugins/e-acsl/doc/refman/changes_modern.tex +++ b/src/plugins/e-acsl/doc/refman/changes_modern.tex @@ -1,8 +1,9 @@ \section{Changes} % Next version -\subsection*{Version \version} +%\subsection*{Version \version} +\subsection*{Version 1.17} \begin{itemize} \item \changeinsection{expressions}{xor \lstinline|\^\^| is not lazy} \item \changeinsection{expressions}{new extended syntax for quantifications} @@ -179,7 +180,7 @@ in \lstinline|\\at|} \item \changeinsection{higherorder}{support for \lstinline|\\sum|, \lstinline|\\prod|, and \lstinline|\\numof|} \end{itemize} - + \subsection*{Version Vanadium-23} \begin{itemize} \item \changeinsection{expressions}{mark logic function and predicate diff --git a/src/plugins/e-acsl/doc/userman/changes.tex b/src/plugins/e-acsl/doc/userman/changes.tex index cbdddcd2a4d79e312b40c913ba71a700538bcf8a..23a76db94725e69c99f6ea9376463c01b72fbcc2 100644 --- a/src/plugins/e-acsl/doc/userman/changes.tex +++ b/src/plugins/e-acsl/doc/userman/changes.tex @@ -6,7 +6,7 @@ release. First we list changes of the last release. % Next version %\section*{E-ACSL \eacslpluginversion \eacslplugincodename} -\section*{E-ACSL \eacslpluginversion \eacslplugincodename} +\section*{E-ACSL 24.0 Chromium} \begin{itemize} \item \textbf{Runtime Monitor Behavior}: Document new options diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index 8547ac9d2e1d37fcc2b8c66c7fd6dc1131c99821..6f14f96c8043d9906eb9884c1ff58e7570dbb0cd 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -1,4 +1,4 @@ -#!/bin/sh -e +#!/bin/sh ########################################################################## # # # This file is part of the Frama-C's E-ACSL plug-in. # @@ -23,11 +23,30 @@ # Convenience wrapper for small runs of E-ACSL Frama-C plugin -# Base dir of this script -BASEDIR="$(realpath `dirname $0`)" +# The -e option is not present in the sha-bang on purpose, the error() function +# should be used after each command that may fail. + +# Portable realpath using pwd +realpath() { + if [ -e "$1" ]; then + if [ -d "$1" ]; then + (cd "$1" && pwd) + else + local name=$(basename "$1") + local dir=$(cd $(dirname "$1") && pwd) + echo $dir/$name + fi + return 0 + else + echo "realpath: no such file or directory: '$1'" 1>&2 + return 1 + fi +} # Print a message to STDERR and exit. If the second argument (exit code) # is provided and it is '0' then do nothing. +# /!\ Use this function after each command that may fail with the second +# argument set to $? error () { if [ -z "$2" ] || ! [ "$2" = 0 ]; then echo "e-acsl-gcc: fatal error: $1" 1>&2 @@ -40,6 +59,10 @@ warning () { echo "e-acsl-gcc: warning: $1" 1>&2 } +# Base dir of this script +BASEDIR="$(realpath `dirname $0`)" +error "unable to find base dir of script" $? + # True if the script is launched from the E-ACSL sources, false otherwise is_development_version() { test -f "$BASEDIR/../E_ACSL.mli" @@ -47,13 +70,13 @@ is_development_version() { # Check if a given executable name can be found by in the PATH has_tool() { - which "$@" >/dev/null 2>&1 && return 0 || return 1 + command -v "$@" >/dev/null 2>&1 && return 0 || return 1 } # Check if a given executable name is indeed an executable or can be found # in the $PATH. Abort the execution if not. check_tool() { - { has_tool "$1" || test -e "$1"; } || error "No executable $1 found"; + { has_tool "$1" || test -e "$1"; } || error "No executable '$1' found"; } # Check if a given Frama-C executable name is indeed an executable, can be found @@ -61,7 +84,7 @@ check_tool() { # in the binary folder of the development version. Abort the execution if not. retrieve_framac_path() { if has_tool "$1"; then - echo $(which "$1") + echo $(command -v "$1") elif [ -e "$1" ]; then echo "$1" elif [ -e "$BASEDIR/$1" ]; then @@ -69,7 +92,8 @@ retrieve_framac_path() { elif is_development_version && [ -e "$BASEDIR/../../../../bin/$1" ]; then echo "$BASEDIR/../../../../bin/$1" else - error "No executable $1 or $BASEDIR/$1 found" + echo "No executable '$1' or '$BASEDIR/$1' found" + return 1 fi } @@ -103,23 +127,6 @@ is_number() { fi } -# Portable realpath using pwd -realpath() { - if [ -e "$1" ]; then - if [ -d "$1" ]; then - (cd "$1" && pwd) - else - local name=$(basename "$1") - local dir=$(cd $(dirname "$1") && pwd) - echo $dir/$name - fi - return 0 - else - echo "realpath: no such file or directory: '$1'" 1>&2 - return 1 - fi -} - # Split a comma-separated string into a space-separated string, remove # all duplicates and trailing, leading or multiple spaces tokenize() { @@ -229,7 +236,10 @@ mmodel_features() { case $model in bittree) flags="-DE_ACSL_BITTREE_MMODEL" ;; segment) flags="-DE_ACSL_SEGMENT_MMODEL" ;; - *) error "Memory model '$model' is not available in this distribution" ;; + *) + echo "Memory model '$model' is not available in this distribution" + return 1 + ;; esac # Temporal analysis @@ -546,13 +556,13 @@ do # Supply Frama-C executable name -I|--frama-c) shift; - OPTION_FRAMAC="$(which $1)" + OPTION_FRAMAC="$(command -v $1 || echo $1)" shift; ;; # Supply GCC executable name -G|--gcc) shift; - OPTION_CC="$(which $1)" + OPTION_CC="$(command -v $1 || echo $1)" shift; ;; # Specify EACSL_SHARE directory (where C runtime library lives) by hand @@ -590,6 +600,7 @@ do shift; # Convert comma-separated string into white-space separated string OPTION_EACSL_MMODELS="`echo $1 | sed -s 's/,/ /g'`" + error "unable to parse '$1' with sed" $? shift; ;; # Print names of the supported memody models. @@ -696,12 +707,12 @@ do ;; --ar) shift; - OPTION_AR="$(which $1)" + OPTION_AR="$(command -v $1 || echo $1)" shift; ;; --ranlib) shift; - OPTION_RANLIB="$(which $1)" + OPTION_RANLIB="$(command -v $1 || echo $1)" shift; ;; --with-dlmalloc) @@ -746,6 +757,7 @@ fi # Check Frama-C and GCC executable names OPTION_FRAMAC="$(retrieve_framac_path "$OPTION_FRAMAC")" +error "$OPTION_FRAMAC" $? check_tool "$OPTION_CC" # Frama-C directories @@ -757,6 +769,7 @@ FRAMAC="$OPTION_FRAMAC" if is_development_version; then # Development version DEVELOPMENT="$(realpath "$BASEDIR/..")" + error "unable to find parent dir of base dir" $? # Check if the project has been built, as if this is a non-installed # version that has not been built Frama-C will fallback to an installed one # for instrumentation but still use local RTL @@ -799,7 +812,7 @@ GCCMACHDEP="-m$MACHDEPFLAGS" # RTE flags RTE_FLAGS="$(rte_options "$OPTION_RTE" "$OPTION_RTE_SELECT")" -error "Invalid argument $1 to --rte|-a option" $? +error "Invalid argument '$RTE_FLAGS' to --rte|-a option" $? # Frama-C and related flags # Additional flags passed to Frama-C preprocessor via `-cpp-extra-args` @@ -1027,6 +1040,7 @@ if [ -n "$OPTION_COMPILE" ]; then # RTL sources EACSL_RTL="$EACSL_SHARE/e_acsl_rtl.c" EACSL_MMODEL_FEATURES="$(mmodel_features $model)" + error "$EACSL_MMODEL_FEATURES" $? ($OPTION_ECHO; $CC \ $EACSL_MMODEL_FEATURES \