diff --git a/src/plugins/e-acsl/.gitignore b/src/plugins/e-acsl/.gitignore index 5a408ad7fca1a997233c61acae61ad3863abc9b5..6f12194ddbc0198d72df30192cb7f036339c617c 100644 --- a/src/plugins/e-acsl/.gitignore +++ b/src/plugins/e-acsl/.gitignore @@ -49,8 +49,6 @@ /doc/userman/*.log /doc/userman/*.lof /doc/userman/eacslversion.tex -/tests/test_config -/tests/test_config_dev /tests/*/result*/* .frama-c META.frama-c-e_acsl diff --git a/src/plugins/e-acsl/tests/builtin/dune b/src/plugins/e-acsl/tests/builtin/dune new file mode 100644 index 0000000000000000000000000000000000000000..9dbf4e24533a7de7d1e1946bcef58497e1507f23 --- /dev/null +++ b/src/plugins/e-acsl/tests/builtin/dune @@ -0,0 +1,7 @@ +(subdir + result/utils + (copy_files ../../utils/*)) + +(subdir + result_dev/utils + (copy_files ../../utils/*)) diff --git a/src/plugins/e-acsl/tests/builtin/strcat.c b/src/plugins/e-acsl/tests/builtin/strcat.c index ae47c89f2928c950ef25095e7f4bc2dd8fc3710b..4f5097eee1c4430a6cfb44d66163f75bdc0be32d 100644 --- a/src/plugins/e-acsl/tests/builtin/strcat.c +++ b/src/plugins/e-acsl/tests/builtin/strcat.c @@ -2,10 +2,10 @@ COMMENT: Test `strcat` and `strncat` E-ACSL built-ins DEPS: @PTEST_DEPS@ utils/signalled.h STDOPT: +"-eva-precision=1" - COMMENT: This part is blank on purpose (test stability + Dune) - - - +*/ +/* run.config_dev + MACRO: INCLUDED_HEADERS utils/signalled.h + COMMENT: This part is blank on purpose (test stability + Dune) */ diff --git a/src/plugins/e-acsl/tests/builtin/strcmp.c b/src/plugins/e-acsl/tests/builtin/strcmp.c index 10c86c02e0aa57f3d845574008a91f39bb4eec26..37f43a402148b2f222d2e30d726b418c6c83e13c 100644 --- a/src/plugins/e-acsl/tests/builtin/strcmp.c +++ b/src/plugins/e-acsl/tests/builtin/strcmp.c @@ -2,10 +2,10 @@ COMMENT: Test `strcmp` and `strncmp` E-ACSL built-ins DEPS: @PTEST_DEPS@ utils/signalled.h STDOPT: - COMMENT: This part is blank on purpose (test stability + Dune) - - - +*/ +/* run.config_dev + MACRO: INCLUDED_HEADERS utils/signalled.h + COMMENT: This part is blank on purpose (test stability + Dune) */ diff --git a/src/plugins/e-acsl/tests/builtin/strcpy.c b/src/plugins/e-acsl/tests/builtin/strcpy.c index 51987a4299dbfbe0d75279a0e566dea7ec4274d5..fcf30f6cd2560230f568405e69b3590eff6a7beb 100644 --- a/src/plugins/e-acsl/tests/builtin/strcpy.c +++ b/src/plugins/e-acsl/tests/builtin/strcpy.c @@ -2,10 +2,10 @@ COMMENT: Test `strcpy` and `strncpy` E-ACSL built-ins DEPS: @PTEST_DEPS@ utils/signalled.h STDOPT: - COMMENT: This part is blank on purpose (test stability + Dune) - - - +*/ +/* run.config_dev + MACRO: INCLUDED_HEADERS utils/signalled.h + COMMENT: This part is blank on purpose (test stability + Dune) */ diff --git a/src/plugins/e-acsl/tests/builtin/strlen.c b/src/plugins/e-acsl/tests/builtin/strlen.c index b570dfe679ef08540fc73c48292d915df29d460a..5ec3ad2191479f2bcca75821388e9fb3e54f646a 100644 --- a/src/plugins/e-acsl/tests/builtin/strlen.c +++ b/src/plugins/e-acsl/tests/builtin/strlen.c @@ -2,10 +2,10 @@ COMMENT: Test `strlen` E-ACSL built-ins DEPS: @PTEST_DEPS@ utils/signalled.h STDOPT: - COMMENT: This part is blank on purpose (test stability + Dune) - - - +*/ +/* run.config_dev + MACRO: INCLUDED_HEADERS utils/signalled.h + COMMENT: This part is blank on purpose (test stability + Dune) */ diff --git a/src/plugins/e-acsl/tests/dune b/src/plugins/e-acsl/tests/dune index 30ba5050fcdccc4b72aa84e325a6248a547a0269..5a43bd223a0bae216544fe3eb2c7dfb50657484e 100644 --- a/src/plugins/e-acsl/tests/dune +++ b/src/plugins/e-acsl/tests/dune @@ -1,7 +1,6 @@ -; Used by the ptests directive `LIBS: ../../print` in `tests_config` files. -; (library -; (name print) -; (modules print) -; (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-e-acsl.core) -; (flags -open Frama_c_kernel) -; ) +(library + (name E_ACSL_test) + (modules E_ACSL_test) + (libraries frama-c.init.cmdline frama-c.boot frama-c.kernel frama-c-e-acsl.core) + (flags -open Frama_c_kernel) +) diff --git a/src/plugins/e-acsl/tests/format/dune b/src/plugins/e-acsl/tests/format/dune new file mode 100644 index 0000000000000000000000000000000000000000..9dbf4e24533a7de7d1e1946bcef58497e1507f23 --- /dev/null +++ b/src/plugins/e-acsl/tests/format/dune @@ -0,0 +1,7 @@ +(subdir + result/utils + (copy_files ../../utils/*)) + +(subdir + result_dev/utils + (copy_files ../../utils/*)) diff --git a/src/plugins/e-acsl/tests/format/fprintf.c b/src/plugins/e-acsl/tests/format/fprintf.c index d882296dc46353433056f0b1c97a646606364f58..71cbd78f9a6e17ef1b7d4b436a5a5ac7bb47db42 100644 --- a/src/plugins/e-acsl/tests/format/fprintf.c +++ b/src/plugins/e-acsl/tests/format/fprintf.c @@ -2,11 +2,11 @@ COMMENT: Check behaviours of format functions DEPS: @PTEST_DEPS@ utils/signalled.h STDOPT: +"-eva-precision=1" +*/ +/* run.config_dev + MACRO: INCLUDED_HEADERS utils/signalled.h COMMENT: This part is blank on purpose (test stability + Dune) - - - */ #include "utils/signalled.h" diff --git a/src/plugins/e-acsl/tests/format/printf.c b/src/plugins/e-acsl/tests/format/printf.c index a70af11be0159a5a338a4f1990f37d513d48481e..321fca54b3083aa5f40eb69d5fd878728cd4df16 100644 --- a/src/plugins/e-acsl/tests/format/printf.c +++ b/src/plugins/e-acsl/tests/format/printf.c @@ -5,11 +5,11 @@ */ /* run.config_dev MACRO: ROOT_EACSL_GCC_OPTS_EXT @ROOT_EACSL_GCC_OPTS_EXT@ -e "-Wno-maybe-uninitialized" + MACRO: INCLUDED_HEADERS utils/signalled.h COMMENT: This part is blank on purpose (test stability + Dune) - */ #include "utils/signalled.h" diff --git a/src/plugins/e-acsl/tests/ptests_config b/src/plugins/e-acsl/tests/ptests_config index 824139152c3c0908ae0c33824c7fdf222d5eaad5..0c0f44a5c36506af7ae9a955ce3701188d87fff2 100644 --- a/src/plugins/e-acsl/tests/ptests_config +++ b/src/plugins/e-acsl/tests/ptests_config @@ -1 +1,2 @@ -IGNORE= DEFAULT_SUITES = arith bts builtin constructs examples format full-mtracking gmp-only memory special temporal +DEFAULT_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory special temporal +dev_SUITES = arith bts builtin concurrency constructs examples format full-mtracking gmp-only memory special temporal diff --git a/src/plugins/e-acsl/tests/test_config b/src/plugins/e-acsl/tests/test_config index 32bdb4f86a1625cc53ce62d68ca8ce0b3b159cda..a729d3877fc2389a3b8497ade9c3f68750616abd 100644 --- a/src/plugins/e-acsl/tests/test_config +++ b/src/plugins/e-acsl/tests/test_config @@ -2,12 +2,13 @@ MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@ MACRO: MACHDEP -machdep gcc_x86_64 MACRO: GLOBAL @MACHDEP@ -remove-unused-specified-functions -verbose 0 -no-unicode -MACRO: EACSL -e-acsl -e-acsl-share @PTEST_SHARE_DIR@/e-acsl -e-acsl-verbose 1 +COMMENT: no more share to set with Dune +MACRO: EACSL -e-acsl -e-acsl-verbose 1 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 -PLUGIN: E_ACSL eva,scope,variadic rtegen +PLUGIN: e-acsl eva,scope,inout,variadic rtegen LIBS: @PTEST_SUITE_DIR@/../E_ACSL_test LOG: gen_@PTEST_NAME@.c diff --git a/src/plugins/e-acsl/tests/test_config_dev b/src/plugins/e-acsl/tests/test_config_dev index 0ce872fd8895a63e08ee03b78a2810b1d85955cf..4f999011228f6439d8868c9b337ea490dc7baf9f 100644 --- a/src/plugins/e-acsl/tests/test_config_dev +++ b/src/plugins/e-acsl/tests/test_config_dev @@ -7,10 +7,10 @@ MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X --no-assert-print-data COMMENT: Default options for the frama-c invocation MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0 -PLUGIN: E_ACSL eva,scope,variadic rtegen +PLUGIN: e-acsl eva,scope,variadic rtegen COMMENT: The dependency to the plugin share directory has not to be explicited -DEPS: @PTEST_SUITE_DIR@/../wrapper.sh +DEPS: @PTEST_SUITE_DIR@/../wrapper.sh @INCLUDED_HEADERS@ EXEC: LOG @EACSL_ERR@ @PTEST_SUITE_DIR@/../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@" @@ -26,3 +26,5 @@ COMMENT: Define the following macro in a test to filter the output of the test e 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 + +MACRO: INCLUDED_HEADERS