From 1b24c0fd7ab3f4ee4df665f30a3906c0ffceec09 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 14 Oct 2021 17:59:44 +0200
Subject: [PATCH] [eacsl] Update test config to use LIBS directive
---
src/plugins/e-acsl/Makefile.in | 10 +++++-----
src/plugins/e-acsl/headers/header_spec.txt | 2 +-
src/plugins/e-acsl/tests/{print.ml => E_ACSL_test.ml} | 0
src/plugins/e-acsl/tests/test_config.in | 3 ++-
4 files changed, 8 insertions(+), 7 deletions(-)
rename src/plugins/e-acsl/tests/{print.ml => E_ACSL_test.ml} (100%)
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 5127ac2254f..c3e5537eff5 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -185,7 +185,7 @@ PLUGIN_TESTS_DIRS := \
builtin \
libc
-PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
+PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.ml
DEV?=
ifeq ("$(DEV)","yes")
@@ -203,11 +203,11 @@ 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/print.cmo
+ $(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmo
ifeq ($(OCAMLBEST),opt)
TEST_DEPENDENCIES += \
- $(EACSL_PLUGIN_DIR)/tests/print.cmxs
+ $(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmxs
endif
# Add the test dependencies to the test targets, but also to
@@ -341,7 +341,7 @@ EACSL_TEST_FILES = \
tests/temporal/test_config_dev \
tests/format/test_config \
tests/format/test_config_dev \
- tests/print.ml \
+ tests/E_ACSL_test.ml \
EACSL_TESTS_C_FILES = \
$(foreach dir, $(addprefix tests/,$(PLUGIN_TESTS_DIRS)), \
@@ -451,7 +451,7 @@ EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
E_ACSL.mli \
Makefile.in configure.ac tab-in-changelog.sh \
scripts/*.sh \
- tests/print.ml \
+ tests/E_ACSL_test.ml \
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 3daf5993839..1583aff49c0 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -158,7 +158,7 @@ src/project_initializer/rtl.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
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/print.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+tests/E_ACSL_test.ml: 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/print.ml b/src/plugins/e-acsl/tests/E_ACSL_test.ml
similarity index 100%
rename from src/plugins/e-acsl/tests/print.ml
rename to src/plugins/e-acsl/tests/E_ACSL_test.ml
diff --git a/src/plugins/e-acsl/tests/test_config.in b/src/plugins/e-acsl/tests/test_config.in
index 6b01b795f88..ce7dca752b1 100644
--- a/src/plugins/e-acsl/tests/test_config.in
+++ b/src/plugins/e-acsl/tests/test_config.in
@@ -5,10 +5,11 @@ MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0
MACRO: EACSL -e-acsl -e-acsl-share ./share/e-acsl -e-acsl-verbose 1 -e-acsl-assert-print-data
MACRO: EVA -eva -eva-no-alloc-returns-null -eva-no-results -eva-no-print -eva-warn-key libc:unsupported-spec=inactive -eva-warn-key loop-unroll:auto=inactive
-MACRO: EVENTUALLY -print -ocode @DEST@.c -load-script ./tests/print.cmxs
+MACRO: EVENTUALLY -print -ocode @DEST@.c
PLUGIN: E_ACSL eva,scope,variadic rtegen
+LIBS: ../E_ACSL_test
LOG: gen_@PTEST_NAME@.c
OPT: @GLOBAL@ @EACSL@ -then-last @EVA@ @EVENTUALLY@
FILTER:@SEDCMD@ -e "s|[a-zA-Z/\\]\+frama_c_project_e-acsl_[a-z0-9]*|PROJECT_FILE|" -e "s|$FRAMAC_SHARE|FRAMAC_SHARE|g" -e "s|../../share|FRAMAC_SHARE|g" -e "s|./share/e-acsl|FRAMAC_SHARE/e-acsl|g" -e "s|share/e-acsl|FRAMAC_SHARE/e-acsl|g"
--
GitLab