diff --git a/bin/test.sh b/bin/test.sh index 1b8254771f14a9ad4b570c171df3f3b4a73a5e23..4192edf44b67e3543adec4bf0cf413d13a0d02fe 100755 --- a/bin/test.sh +++ b/bin/test.sh @@ -31,7 +31,7 @@ SAVE= DUNE_OPT= DUNE_LOG=./.test-errors.log -CACHEDIR=./.wp-cache +CACHEDIR=$(pwd -P)/.wp-cache FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git # -------------------------------------------------------------------------- @@ -73,7 +73,7 @@ function Usage echo "" echo " FRAMAC_WP_QUALIF" echo " FRAMAC_WP_CACHEDIR" - echo " Location of wp-cache ($FRAMAC_WP_CACHEDIR)" + echo " Absolute path to wp-cache directory ($FRAMAC_WP_CACHEDIR)" if [ ! -d $FRAMAC_WP_CACHEDIR ]; then echo " About to clone from $FRAMAC_WP_CACHE_GIT" fi @@ -142,6 +142,11 @@ function SetEnv [ ! -f "$FRAMAC_WP_CACHEDIR" ] || [ -d "$FRAMAC_WP_CACHEDIR" ] \ || Error "$FRAMAC_WP_CACHEDIR is not a directory" + case "$FRAMAC_WP_CACHEDIR" in + /*);; + *) Error "Requires an absolute path to $FRAMAC_WP_CACHEDIR";; + esac + } function CloneCache diff --git a/src/plugins/wp/tests/README.md b/src/plugins/wp/tests/README.md index 3d90fddfa98c31cc044c5f1bbcd7e4df7775e89a..f1d1bc29cf9349d365c4b13aaddce54f531d584d 100644 --- a/src/plugins/wp/tests/README.md +++ b/src/plugins/wp/tests/README.md @@ -48,6 +48,8 @@ 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. + 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 _every_ run of `frama-c -wp` might then use it by default. Be carefull if you do so.