Merge branch 'fix/test/promotion-when-using-test-script' into 'master'

[test] Fixes promoting when using test script

Closes #1153

See merge request frama-c/frama-c!3898

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

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

tests/misc/global_decl_loc.i

 /* 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}
  */

tests/misc/global_decl_loc2.i

 /* 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}