diff --git a/bin/test.sh b/bin/test.sh index 4192edf44b67e3543adec4bf0cf413d13a0d02fe..305e39abd99688146118b42c52feb627ce18db47 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -29,6 +29,7 @@ LOGS= TESTS= SAVE= +DUNE_ALIAS= DUNE_OPT= DUNE_LOG=./.test-errors.log CACHEDIR=$(pwd -P)/.wp-cache @@ -169,9 +170,10 @@ function PullCache # -------------------------------------------------------------------------- [ "$DUNE_LOG" = "" ] || rm -rf $DUNE_LOG -function TestAlias +function RunAlias { + Head "Running tests..." if [ "$DUNE_LOG" = "" ]; then Run dune build $DUNE_OPT $@ elif [ "$SAVE" != "yes" ] && [ "$VERBOSE" != "yes" ]; then @@ -204,8 +206,8 @@ function TestDir CFG="(config $CONFIG)" ;; esac - Head "Running test on directory $1 $CFG" - TestAlias @$ALIAS + Head "Register test on directory $1 $CFG" + DUNE_ALIAS="${DUNE_ALIAS} @$ALIAS" } # -------------------------------------------------------------------------- @@ -231,17 +233,17 @@ function TestFile if [ "$LOGS" = "yes" ]; then ALIAS=$DIR/$RESULT/$FILE else - ALIAS=$DIR/$RESULT/${FILE%.*}.wtests + ALIAS=$DIR/$RESULT/${FILE%.*}.diff fi - Head "Running test on file $1 $CFG" - TestAlias @$ALIAS + Head "Register test on file $1 $CFG" + DUNE_ALIAS="${DUNE_ALIAS} @$ALIAS" } # -------------------------------------------------------------------------- # --- Tests Processing # -------------------------------------------------------------------------- -function RunTests +function Register { while [ "$1" != "" ] do @@ -251,7 +253,7 @@ function RunTests TestFile $1 else case $1 in - @*) Head "Running test on alias $1"; TestAlias $1;; + @*) Head "Register test on alias $1"; DUNE_ALIAS="${DUNE_ALIAS} $1";; *) ErrorUsage "ERROR: don't known what to do with '$1'";; esac fi @@ -349,5 +351,6 @@ do esac shift done -RunTests $TESTS +Register $TESTS +RunAlias ${DUNE_ALIAS} Status $DUNE_LOG diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md index f1d1bc29cf9349d365c4b13aaddce54f531d584d..d3988a13649a5f8fb5fb6f7ce3680b4781073ec8 100644 --- a/src/plugins/wp/tests/README.md +++ b/src/plugins/wp/tests/README.md @@ -48,7 +48,7 @@ The `./bin/test.sh` uses, in order of proprity: - `FRAMAC_WP_CACHEDIR` environement variable, - local `./.wp-cache` directory. -Of course, these environment variables must be set to an absolute path to prevent from different execution locations of Frama-C. +Of course, these environment variables must be set to an absolute path since test executions are done from different directories. It is _not_ recommended to use the `FRAMAC_WP_CACHEDIR` variable in your default shell setup, unless is it a temporary directory (eg. `/tmp/wp-sandbox`) since diff --git a/tests/misc/global_decl_loc.i b/tests/misc/global_decl_loc.i index c9acc56f5dd0c18bcd267c57d5fe311ab0708f90..8e72244e97d9bff0821d7f3e0d0d1a1583eb2dc0 100644 --- a/tests/misc/global_decl_loc.i +++ b/tests/misc/global_decl_loc.i @@ -1,5 +1,5 @@ /* run.config - COMMENT: with dune, the LIBS directive must be replaced by a MODULE directive (see also ./test_config file) + COMMENT: note: the module global_decl_loc is also used by another test file (global_decl_loc2.i) MODULE: global_decl_loc OPT: %{dep:./global_decl_loc2.i} */ diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i index 07967d5c3d7873c33ac86dac295018a2058e335c..f148b3592cf0038d4e7153f1117196609670c3af 100644 --- a/tests/misc/global_decl_loc2.i +++ b/tests/misc/global_decl_loc2.i @@ -1,5 +1,5 @@ /* run.config* - COMMENT: with dune, the LIBS directive must be replaced by a MODULE directive (see also ./test_config file) + COMMENT: note: the module global_decl_loc is also used by another test file (global_decl_loc.i) MODULE: global_decl_loc OPT: %{dep:./global_decl_loc.i}