Skip to content
Snippets Groups Projects
Commit 3fd6a1eb authored by Julien Signoles's avatar Julien Signoles
Browse files

Merge branch 'feature/andre/remove-sedcmd' into 'master'

[E-ACSL] remove SEDCMD and .in test configs

See merge request frama-c/frama-c!3637
parents b35eb8a0 0409d798
No related branches found
No related tags found
No related merge requests found
......@@ -233,26 +233,12 @@ E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
tests:: $(TEST_DEPENDENCIES)
endif
$(EACSL_PLUGIN_DIR)/tests/test_config: \
$(EACSL_PLUGIN_DIR)/tests/test_config.in \
$(EACSL_PLUGIN_DIR)/Makefile
$(PRINT_MAKING) $@
$(SED) -e "s|@SEDCMD@|`command -v sed`|g" $< > $@
$(EACSL_PLUGIN_DIR)/tests/test_config_dev: \
$(EACSL_PLUGIN_DIR)/tests/test_config_dev.in \
$(EACSL_PLUGIN_DIR)/Makefile
$(PRINT_MAKING) $@
$(SED) -e "s|@SEDCMD@|`command -v sed`|g" $< > $@
clean::
for d in $(E_ACSL_EXTRA_DIRS); do \
$(RM) $$d/*~; \
done
$(PRINT_RM) cleaning generated test files
$(RM) $(E_ACSL_DIR)/tests/*.cm* $(E_ACSL_DIR)/tests/*.o
$(RM) $(E_ACSL_DIR)/tests/test_config \
$(E_ACSL_DIR)/tests/test_config_dev
$(RM) $(foreach dir, $(PLUGIN_TESTS_DIRS), tests/$(dir)/result/*)
endif
......@@ -353,8 +339,8 @@ EACSL_DOC_FILES = \
$(EACSL_MANPAGES)
EACSL_TEST_FILES = \
tests/test_config_dev.in \
tests/test_config.in \
tests/test_config_dev \
tests/test_config \
tests/wrapper.sh \
tests/gmp-only/test_config \
tests/gmp-only/test_config_dev \
......
......@@ -186,8 +186,8 @@ 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/test_config: .ignore
tests/test_config_dev: .ignore
tests/builtin/test_config: .ignore
tests/builtin/test_config_dev: .ignore
tests/concurrency/test_config: .ignore
......
......@@ -4,7 +4,7 @@
MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose --concurrency
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:\s[0-9-]*_Offset:xxxxx_g | @SEDCMD@ -e s/[0-9]*\skB/xxxkB/g | @SEDCMD@ -e s/Leaked.*bytes/Leakedxxxbytes/g
MACRO: ROOT_EACSL_EXEC_FILTER sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g | sed -e s/Leaked.*bytes/Leakedxxxbytes/g
*/
// Include existing test
......
......@@ -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 sed -e s/0x[0-9a-f]*$/0x000000/g
*/
#include <float.h>
......
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 sed -e s+/.*/share/e-acsl+FRAMAC_SHARE/e-acsl+
......@@ -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:\s[0-9-]*_Offset:xxxxx_g | @SEDCMD@ -e s/[0-9]*\skB/xxxkB/g
MACRO: ROOT_EACSL_EXEC_FILTER sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g
*/
int main() {
return 0;
......
NOFRAMAC: only the EXEC command below is useful in this config
MACRO: SEDCMD @SEDCMD@
MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.err.log
COMMENT: Default options for `e-acsl-gcc.sh`
......
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