diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 93fe3e1be9eef035a663acb0c1366e666c03b693..c80d95a5803c50c459cd1baa910bac15266d2862 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -204,7 +204,8 @@ TEST_DEPENDENCIES:= \
$(EACSL_PLUGIN_DIR)/tests/ptests_config \
$(EACSL_PLUGIN_DIR)/tests/test_config \
$(EACSL_PLUGIN_DIR)/tests/test_config_dev \
- $(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmo
+ $(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmo \
+ $(EACSL_PLUGIN_DIR)/tests/wrapper.sh
ifeq ($(OCAMLBEST),opt)
TEST_DEPENDENCIES += \
@@ -332,6 +333,7 @@ EACSL_DOC_FILES = \
EACSL_TEST_FILES = \
tests/test_config_dev.in \
tests/test_config.in \
+ tests/wrapper.sh \
tests/gmp-only/test_config \
tests/gmp-only/test_config_dev \
tests/full-mtracking/test_config \
@@ -453,6 +455,7 @@ EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
Makefile.in configure.ac tab-in-changelog.sh \
scripts/*.sh \
tests/E_ACSL_test.ml \
+ tests/wrapper.sh \
man/e-acsl-gcc.sh.1
EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
$(EACSL_CEA_SHARE)
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 77c47d3113ad4339362f25fbe8573ea54adb43ef..c260e31129e5aa2fc6de80d76f5bc89248cc42b1 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -164,6 +164,7 @@ src/project_initializer/rtl.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/project_initializer/prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/project_initializer/prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
tests/E_ACSL_test.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+tests/wrapper.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL
tests/test_config.in: .ignore
tests/test_config_dev.in: .ignore
tests/builtin/test_config: .ignore
diff --git a/src/plugins/e-acsl/tests/constructs/printed_data.c b/src/plugins/e-acsl/tests/constructs/printed_data.c
index 8da27ae88f84d87e23005dc89776b8605ef0fd98..9ae229447051a2d1d3bb4fd15705f995f52f1193 100644
--- a/src/plugins/e-acsl/tests/constructs/printed_data.c
+++ b/src/plugins/e-acsl/tests/constructs/printed_data.c
@@ -4,7 +4,7 @@
/* run.config_dev
COMMENT: Print the data and filter the addresses of the output so that the test is deterministic.
MACRO: ROOT_EACSL_GCC_OPTS_EXT --assert-print-data -e -DE_ACSL_DEBUG_ASSERT -F -no-unicode
- MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|0x[0-9a-f]*$|0x000000|g"
+ MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e s/0x[0-9a-f]*$/0x000000/g
*/
#include <float.h>
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
index dd9937641ad9afdd509b8fa4fcad02299d072049..e561c38846bd832eb584a4cf4af91a6bd7cc8c3e 100644
--- a/src/plugins/e-acsl/tests/format/test_config_dev
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -1,3 +1,3 @@
COMMENT: Remove --full-mtracking once e-acsl#118 is fixed
MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking -F -variadic-no-translation
-MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
+MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e s+/.*/share/e-acsl+FRAMAC_SHARE/e-acsl+
diff --git a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
index 1f58f5e6b965c2af807ca2ea7605fd1343253dba..ea22c000ba0e6f13e2f8f5a71375617d1c76221e 100644
--- a/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
+++ b/src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c
@@ -5,7 +5,7 @@
/* run.config_dev
MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose --full-mtracking
COMMENT: Filter the addresses of the output so that the test is deterministic.
- MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|0x[0-9a-f-]*|0x0000-0000-0000|g" | @SEDCMD@ -e "s|Offset: [0-9-]*|Offset: xxxx|g"
+ MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | @SEDCMD@ -e s_Offset:\s[0-9-]*_Offset:xxxxx_g
*/
int main() {
return 0;
diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
index 30d0abab894eea95a8bf6781909e678cf384f022..78b9d1588bcd821a058727741193dbbc009fd5bb 100644
--- a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
+++ b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log
@@ -1,17 +1,17 @@
>>> HEAP ---------------------
Application: 128 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Primary : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> STACK --------------------
Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
- Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Primary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> GLOBAL -------------------
Application: 0 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
- Secondary : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Primary : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> TLS ----------------------
Application: 64 MB [0x0000-0000-0000, 0x0000-0000-0000]
- Primary : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
- Secondary : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+ Primary : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+ Secondary : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
>>> --------------------------
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index a4b467001b82cdbff1ed5c3204c016343d9d3245..eefa60c7fb94b292a05dcf9d11fc8ace5e8f7706 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -1,12 +1,7 @@
NOFRAMAC: only the EXEC command below is useful in this config
MACRO: SEDCMD @SEDCMD@
-MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
-MACRO: OUT @PTEST_NAME@.res.log
-MACRO: ERR @PTEST_NAME@.err.log
MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.err.log
-COMMENT: Define the following macro to "no" in a test to stop the execution of `e-acsl-gcc.sh`
-MACRO: ROOT_EACSL_GCC_ENABLE yes
COMMENT: Default options for `e-acsl-gcc.sh`
MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X --no-assert-print-data
COMMENT: Default options for the frama-c invocation
@@ -14,7 +9,7 @@ MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
PLUGIN: E_ACSL eva,scope,variadic rtegen
-EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c-exe@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
+EXEC: LOG @EACSL_ERR@ ./tests/wrapper.sh "@frama-c-exe@" "@PTEST_RESULT@" "@PTEST_NAME@" "@PTEST_FILE@" "@EACSL_ERR@" "@ROOT_EACSL_GCC_MISC_OPTS@ @ROOT_EACSL_GCC_OPTS_EXT@" "@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" "@ROOT_EACSL_EXEC_FILTER@"
COMMENT: These next macros can be redefined in a test file
COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
@@ -22,4 +17,6 @@ MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT
COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh`
MACRO: ROOT_EACSL_GCC_OPTS_EXT
COMMENT: Define the following macro in a test to filter the output of the test execution
+COMMENT: You can chain several filters by separating commands with |. However sed cannot
+COMMENT: use | as a delimiter, please use / or another character instead.
MACRO: ROOT_EACSL_EXEC_FILTER cat
diff --git a/src/plugins/e-acsl/tests/wrapper.sh b/src/plugins/e-acsl/tests/wrapper.sh
new file mode 100755
index 0000000000000000000000000000000000000000..a2862ed67aaf28271b544ebd8488287b1a5600d0
--- /dev/null
+++ b/src/plugins/e-acsl/tests/wrapper.sh
@@ -0,0 +1,132 @@
+#!/bin/bash
+##########################################################################
+# #
+# This file is part of the Frama-C's E-ACSL plug-in. #
+# #
+# Copyright (C) 2012-2020 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Wrapper script to compile a test file and execute the resulting binary
+
+# Base dir of this script
+BASEDIR="$(realpath `dirname $0`)"
+
+help() {
+ printf "wrapper.sh - run e-acsl-gcc.sh and the resulting binary to test E-ACSL
+Usage: $0 framac_exe result_dir test_name test_file output_name opts fc_opts filter_cmd
+Args:
+ framac_exe @frama-c-exe@ in test_config
+ result_dir @PTEST_RESULT@ in test_config
+ test_name @PTEST_NAME@ in test_config
+ test_file @PTEST_FILE@ in test_config
+ output_name Output file given to LOG in test_config
+ opts Options for e-acsl-gcc.sh
+ fc_opts Options for Frama-C
+ filter_cmd Command to filter the output of the resulting binary
+" >&2
+ exit 1
+}
+
+if [[ $# -ne 8 ]]; then
+ printf "Error: wrong number of arguments: 8 expected, got $#\n\n" >&2
+ help
+fi
+
+# Name the arguments of the script
+framac_exe=$1
+result_dir=$2
+test_name=$3
+test_file=$4
+output_name=$5
+opts=$6
+fc_opts=$7
+filter_cmd=$8
+
+# Derive output logs from the arguments
+out_log=$result_dir/$test_name.res.log
+err_log=$result_dir/$test_name.err.log
+exec_out_log=$result_dir/$test_name.exec_out.log
+exec_err_log=$result_dir/$test_name.exec_err.log
+output_log=$result_dir/$output_name
+
+# Compile the test file
+$BASEDIR/../scripts/e-acsl-gcc.sh -I $framac_exe \
+ -c $opts \
+ --frama-c-extra="$fc_opts" \
+ -o $result_dir/$test_name.gcc.c \
+ -O $result_dir/$test_name \
+ $test_file \
+ 1>$out_log \
+ 2>$err_log
+
+# Check compilation return code and exit script in case of error
+if [[ $? -ne 0 ]]; then
+ error_code=$?
+ printf "Error while executing e-acsl-gcc.sh\n" > $output_log
+ printf "\nSTDOUT:\n" >> $output_log
+ cat $out_log >> $output_log
+ printf "\nSTDERR:\n" >> $output_log
+ cat $err_log >> $output_log
+ exit $error_code
+fi
+
+# Execute the compiled test file
+$result_dir/$test_name.e-acsl 1>$exec_out_log 2>$exec_err_log
+
+# Check execution return code and exit script in case of error
+if [[ $? -ne 0 ]]; then
+ error_code=$?
+ printf "Error while executing $result_dir/$test_name.e-acsl\n" > $output_log
+ printf "\nSTDOUT:\n" >> $output_log
+ cat $exec_out_log >> $output_log
+ printf "\nSTDERR:\n" >> $output_log
+ cat $exec_err_log >> $output_log
+ exit $error_code
+fi
+
+# No error while executing the script, filter stderr before saving it to the
+# output log
+
+## Create temporary files
+tmp_filter_input=$(mktemp) || (printf "unable to create temp file\n" > $output_log && exit 1)
+tmp_filter_output=$(mktemp) || (printf "unable to create temp file\n" > $output_log && exit 1)
+cp $exec_err_log $tmp_filter_input
+
+## Split the filter command on character | to extract the subcommands and apply
+## the filters one at a time
+IFS='|' read -ra filters <<< "$filter_cmd"
+for filter in "${filters[@]}"; do
+ cat $tmp_filter_input | $filter > $tmp_filter_output
+ if [[ $? -ne 0 ]]; then
+ error_code=$?
+ printf "Error while filtering output with command '$filter'\n" > $output_log
+ printf "\nFILTER INPUT:\n" >> $output_log
+ cat $tmp_filter_input >> $output_log
+ printf "\nFILTER OUTPUT:\n" >> $output_log
+ cat $tmp_filter_output >> $output_log
+ exit $error_code
+ fi
+ cp $tmp_filter_output $tmp_filter_input
+done
+
+## Filtering done, copy output to the output log and remove temporary files
+cp $tmp_filter_output $output_log
+rm $tmp_filter_input
+rm $tmp_filter_output
+
+exit 0